Hacker News Reader

Indeed, that was my point.

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.

On 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.

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

Reply on news.ycombinator.com