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.