3 ms·
The most interesting part of SPARK for me is how all the runtime checks are implicitly, automatically generated and need to be proved. A whole bunch of assumpt
by touisteur 1y ago
The most interesting part of SPARK for me is how all the runtime checks are implicitly, automatically generated and need to be proved.
A whole bunch of assumptions about the language are hidden and the verification conditions are generated automatically for the underlying automatic or semi-automatic proof tools (why3-intermediated) - the second best part of SPARK.
You have to trust that the SPARK FrontEnd makers got it right - or you can inspect/review all the discharged VC if you want - and you still have to actually prove or help prove them all, but I'm not losing sleep over a forgotten 'normal' check.