4 ms·
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
by touisteur 3y 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.
- pyjarrett 3y 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.