The program was written with Ada and failed in a most stupid
way. Is it not a proof enough that safety cannot be sensibly
enforced by mechanical tools? And this was the main rationale
for Ada from day one. If you check for possible commercial
compilers you will see that most of them remember the days of
Windows 95. Ada was forced on people by administrative means
and died when those means were removed. I wonder how much Ada
is in Curiosity on Mars. Let me guess, 0%?
The F35 runs on C++.
"Another difference with JSF is we have learned well the lesson
that Moore's Law can work against you if you don't pay
attention," Jeffreys continues. "So we have designed for
technology refresh, so at the appropriate time we can stop
putting in the 1 GHz processor board and swap out to the 2 GHz
board without having to go back and do any redesign. We were once
required to use a MIL-STD-1760 processor with Ada or other
military languages; now we use commercial PowerPC with C++."