> if your processes ... are good enough
I would say that it's possible to write complex safety-critical software in any language, provided it's completely specified beforehand in, well, military detail. This program was likely done when that spec hit the programmers' desks--the project from that point on basically consisted of transforming pseudocode to language-of-choice-X without mucking anything up in the process.
And while the specification process is obviously extremely extensive, it's only a part of the total process and not a guarantee of bug-free code. Many of these projects have gone pear-shaped during the implementation phase despite having good specifications.
So that's why having good programmers, a good development process, solid libraries and great tooling is so important for the implementation phase. Especially because the requirements always change during development, even for mission-critical military avionics software.
One of the main problems with the F-35 program is that the implementation phase for the development of the plane's software has gone badly wrong. It's already by far the most expensive avionics program ever.
Finally the testing phase is super-critical. ATE designed their own extremely thorough testing setup, ranging from software verifiers to full-scale test-benches to simulate on the ground the full range of software functionality in flight.
It's a difficult process that's very easy to get wrong as a result of the incredible complexity of modern avionics and weapons systems. I am in awe of those teams that get it right.
You could argue the one language which actually does lend itself to formal verification is the one which has been formally specified via operational semantics; namely, Standard ML.
However, any system that runs on top of a virtual machine is problematic because of how extensive their runtimes are. Developing an efficient and competitive DO-178b-certified JVM, for example, would be a huge undertaking, but so would modifying an existing JVM.
Further, anything garbage collected is a problem because you can't have any situations where a timing constraint is violated because of your garbage collector. The best way to prevent this would be to schedule, say, 50 milliseconds every second for garbage collection. But there's still a limit there where the GC can no longer keep up with the rate of garbage production, which could lead to your application running out of memory and failing. Proving that your application will never reach said limit would be hard either by static or dynamic analysis.
We switched because we wanted to reduce the risks of bugs, but you must remember that in most mission critical applications, one must consider failure not only in the software. You use redundancy - in the software, in the hardware, and in the network. We even used several separate power systems and several redundant generators.
EDIT: see http://goedel.cs.uiowa.edu/MVD/talks/Vitek.pdf presentation slides from 9/2012 on realtime and safety-critical Java.
There are a few interesting developments regarding Java for safety-critical and mission-critical applications. One is JSR-302, which is defining a safety-critical subset of Java which will not have garbage collection and will use of a run-time stack rather than a heap for temporary object allocation, the removal of dynamic class-loading, changes to task scheduling and a smaller standard library. These should make it possible to certify JSR-302-compatible Java runtimes and applications for safety-critical and mission-critical tasks.
The second is DO-178C, the follow-on to DO-178B, which will incorporate additional work on the certification of object-oriented languages such as Java.
http://cpptruths.blogspot.com/2005/11/c-templates-are-turing...
Most likely no one will write such a template in a mission critical system. However, from a formal verification standpoint the only way to verify the code is to check the binaries.