> SPARK builds on the strengths of Ada to provide even more guarantees statically rather than dynamically. As summarized in the following table, Ada provides strict syntax and strong typing at compile time plus dynamic checking of run-time errors and program contracts. SPARK allows such checking to be performed statically. In addition, it enforces the use of a safer language subset and detects data flow errors statically.
Contract programming:
- Ada: dynamic
- SPARK: dynamic / static
Run-time errors:
- Ada: dynamic
- SPARK: dynamic / static
Data flow errors:
- Ada: -
- SPARK: static
Strong typing:
- Ada: static
- SPARK: static
Safer language subset:
- Ada: -
- SPARK: static
Strict clear syntax:
- Ada: static
- SPARK: static
---
Additionally, safe pointers in SPARK: https://blog.adacore.com/using-pointers-in-spark and https://arxiv.org/abs/1710.07047.
---
Cryptographic library in SPARK 2014: https://github.com/Componolit/libsparkcrypto.
> libsparkcrypto is a formally verified implementation of several widely used cryptographic algorithms using the SPARK 2014 programming language and toolset. For the complete library proofs of the absence of run-time errors like type range violations, division by zero and numerical overflows are available. Some of its subprograms include proofs of partial correctness.
---
Ada/SPARK is excellent for real-time and safety-critical software: https://www.rcs.ei.tum.de/fileadmin/tueircs/www/becker/spark... to give you some ideas. It may be a bit outdated in some regards, though, for example: "Next version of SPARK 2014 under development (pointers!).". It is already done! :)