4 ms·
Ada and SPARK are not aiming for the same thing. SPARK is intended for formal verification. Ada is not. You can write safety-critical code in the full Ada lang
by MaxBarraclough 5y ago
Ada and SPARK are not aiming for the same thing. SPARK is intended for formal verification. Ada is not.
You can write safety-critical code in the full Ada language, but you won't be able to use SPARK's verification tools.
An example: if I understand correctly, the Boeing 777's avionics software is written in Ada, and they did not use the SPARK subset. [0]
[0] http://archive.adaic.com/projects/atwork/boeing.html http://archive.adaic.com/projects/atwork/boeing.html