|
|
|
|
|
|
by touisteur
339 days 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. |
|
|