Hacker News Reader

Comment by touisteur | Hacker News Reader

I wish rust had learned from that and also kept range/overflow checks on by default and not only in debug mode.

One of the key principles of Rust is zero-overhead abstractions. The more runtime code they insert the harder it would be to sell the language to C/C++ programmers.

They do keep runtime array indexing checks on. I'm pretty sure I remember reading a comment from Steve Klabnik on here that they only turned off overflow checks in release builds by default because array range checks stay on. With neither over/underflow checking nor array index checks, it's a lot more likely you'd accidentally use an out-of-bounds index.

For example, there was an iMessage vulnerability a while ago that relied on unsigned overflow to create an undersized buffer so that data would be written out of bounds later [0]. If it had been written in Rust (or Ada), with overflow checking on, it would have panicked upon overflow, and with it off, it would have panicked when using an out-of-bounds index. With both off, you get this vulnerability.

[0]: https://googleprojectzero.blogspot.com/2021/12/a-deep-dive-i...

And yet bounds checks were kept. Other compilers for other languages gave the option to disable some or all of the range checks, or to enable thorough validity checks. Not an all-or-nothing 'debug' toggle, but project- or file-level options for runtime checks.

On most code I worked on the bounds checks are really not having a large performance impact, especially on modern processors and it's been a very rare occasion I had to remove them, most recently converting the code to SPARK and proving the absence or runtime error. If people are OK pleasing the borrow-checker I'm sure they'll enjoy interaction with the prover (which farms most of the work to why3 and SMT solvers) to make sure their optimisation is actually safe.

> the code to SPARK and proving the absence or runtime error

I wrote Rob Pike's simple regex from the "Practice of Programming" in Ada/SPARK and it blew my mind that I actually managed to prove an absence of runtime error (guaranteed no overflow or out of bounds).

That's very interesting!

I have my copy of "Practice of Programming" about to be delivered. Is your regex implementation available somewhere?

I found it on a past comment, for whoever might be interested:

https://github.com/pyjarrett/simple_regex

What I really like about SPARK is the pragmatism. It's not all or nothing, you can call on non-SPARK code, and you don't have to go full functional verification to profit from the SPARK toolset.

edit: if you feel like sharing your code and experience there, I'm pretty sure some people would be interested.

> you don't have to go full functional verification

The amazing thing to me is that Ada code can call SPARK code just fine, and there's crates of SPARK code in Alire that you can use. It's a huge boost of confidence in the quality of a library that you're using when it has some form of verification.

You can also switch runtime checks off in Ada. The difference is that, in Ada, the default is to have them on, while in Rust, they are off by default.

BTW they've been on by default only since around 2010. IIRC Adacore checked the performance impact on most of their codebases and didn't really see an impact on performance (probably around the time branch prediction really improved on x86 and the Core architecture made branch misses far less painful).

They also pioneered validity checks injected by the compiler.

For the brave souls, shameless plug, I talk a bit about Ada's runtime checks, there https://blog.adacore.com/running-american-fuzzy-lop-on-your-...

Reply on news.ycombinator.com