Hacker News new | past | comments | ask | show | jobs | submit login

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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: