What is SPARK about?

[Claude <claude.defour@orange.fr>]

Ada is a formal language to software engineering.

What is SPARK about?

I means since SPARK is restricted to the best of Ada, is SPARK better
than Ada to resolving complex engineering applications, or SPARK a
better choice than C/C++ to address leaner systems?  (in terms of
compliance to early drafts of DO-178C - certification levels C to A).

Indeed, the successful applications of SPARK bring to results that are
rather difficult to compare.

“The formal design of Tokeneer ID Station (TIS) shows the TIS system
to be a purely sequential system.” -  (INFORMED design, at section
2.2, Identification of the SPARK boundary)

“We believe part of the success of proof on SHOLIS is due to the
simple system architecture. …
Some large-scale SPARK reasoning are also needed, including support
for abstract proof, before the technology can be extensively used at
the highest level of large systems.” - (Is Proof More Cost Effective
Than Testing – Section 8, Summary).

Beyond any theory or academic project, 10 years later, from all the
past SPARK projects’ experiences, does it happen that SPARK can
address “purely sequential systems” or that SPARK “can be extensively
used at the highest level of large systems”?

Claude