SPARK appears to be a restricted subset of ADA, with the addition of formal decorations in comments. The code is compiled by a regular ADA compiler, with the p

SPARK appears to be a restricted subset of ADA, with the addition of formal decorations in comments. The code is compiled by a regular ADA compiler, with the problem areas of ADA avoided by only using a specific subset. Then a separate verification/proving tool is used to read the decorations and use them to analyse the code in more depth than can be done from the code alone. I have experience with similar techniques, and while it sounds very ad hoc it can be made to work in suitable environments. The result is tool-enforced discipline regarding code derivation and development. As always, the system relies on + sufficiently detailed and accurate specifications + sufficient analysis of failure modes + correct compiler tools + correct hardware + sufficiently few transient hardware errors (such as cosmic ray bit flips) ... and other details. See also: http://en.wikipedia.org/wiki/SPARK_(programming_language) http://en.wikipedia.org/wiki/SPARK_(programming_language) http://www.praxis-his.com/spark.aspx http://www.praxis-his.com/spark.aspx