4 ms·
Your point is wrong. C was /not/ intended for safety critical applications. Therefore, it makes sense that using it in that context will require adaptation. Fo
by crocal 5y ago
Your point is wrong. C was /not/ intended for safety critical applications. Therefore, it makes sense that using it in that context will require adaptation.
For Ada it does not. It’s tire patching.
- MaxBarraclough 5y agoAda 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
- pjmlp 5y agoOn the contrary my dear, Ada has been usable for 30 years before SPARK came to be, SPARK only makes it better by adding features that usually are only found in languages like Idris and Coq.