what correctness does ADA focus on ?
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.
Re:Bare Metal Rust Generics
by OnlyOneCannolo on Sunday August 23, 2020 @06:59PM
(#24256007)
I've always wondered this - Does the compiler actually use all that contract information, or is it just the prover?
As 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.
Re:Bare Metal Rust Generics
by OnlyOneCannolo on Sunday August 23, 2020 @11:27PM
(#24257302)
That makes sense. Otherwise why bother conflating the programing language with the verification language.
pretty nice, is the SPARK market lively ? I'd love to see how work is done there
Lively, 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.
Ada and Rust don't have 1:1 comparison on their safety guarantees.
Rust makes a lot of guarantees around memory safety that Ada does not, whilst Ada is far more focused on correctness. Whilst related, these are very different.