3 ms·

Yes, and those non-validated compilers, and even the validated ones, had lots of bugs. We had to get legal with a compiler vendor because of the number of bugs.

by RogerL 11y ago

Yes, and those non-validated compilers, and even the validated ones, had lots of bugs. We had to get legal with a compiler vendor because of the number of bugs. This took disassembling the compiler on our end to prove our points. "Ada is safe". Yes, if it outputs correct code. Otherwise, not so much. Lives were at stake here, and like you say, I'm not sure all the vendors were prepared for what that meant in terms of their product. I really enjoyed working with Ada, but don't think I would want to go back to it today.

nickpsecurity 11y ago
This is true to this day per IRONSIDES paper [1]. Made me consider using Ada as an executable specification language to be converted to equivalent C/C++ and compiled that way. They need to just do a functional implementation of the compiler in a language such as Ocaml with extensive testing. That's what Esterel did for SCADE generator. They said Ocaml compiler stages were easy to trace down to object code. So, that helps with the chicken and egg problem a bit. Alternatively, implement it in the VLISP, PreScheme, or VeriML that were formally verified for correctness. [1] http://ironsides.martincarlisle.com/globecom_2012.pdf http://ironsides.martincarlisle.com/globecom_2012.pdf