|
|
|
|
|
|
by 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. |
|
|
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.