Hacker News new | ask | show | jobs
by pyjarrett 843 days ago
> 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).
2 comments
EuAndreh 835 days ago
That's very interesting!

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

link
EuAndreh 835 days ago
I found it on a past comment, for whoever might be interested:

https://github.com/pyjarrett/simple_regex

link
touisteur 843 days ago
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.

link
pyjarrett 843 days ago
> 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.

link