3 ms·
SPARK is a formal proving system for Ada. Formal correctness is what they focus on, that Ada can safely prove mathematically how a function will behave, and how
by shakna 6y ago
SPARK is a formal proving system for Ada. Formal correctness is what they focus on, that Ada can safely prove mathematically how a function will behave, and how a body of functions will behave.
If you're using Ada without SPARK, it will try and enforce these same guarantees, but generally with a runtime contract system, rather than compile time.
- OnlyOneCannolo 6y agoI've always wondered this - Does the compiler actually use all that contract information, or is it just the prover?
- shakna 6y agoAs of Ada 2012, the redesign means that the compiler can make use of the contract information, and was one of the main reasons for a lot of the changes.
- OnlyOneCannolo 6y agoThat makes sense. Otherwise why bother conflating the programing language with the verification language.
- agumonkey 6y agopretty nice, is the SPARK market lively ? I'd love to see how work is done there
- shakna 6y agoLively, but proprietary. A lot of SPARK stuff tends to be automotive, factory designs, fabrication and the sort of stuff where people working there are buried under dozens of NDAs preventing them from discussing their work in any way. But projects tend to have a longer shelf-life. Contracts expected to take a decade to complete aren't unusual, and the product can be expected to be in use for twice that, or longer.