Sadly, the DoD doesn't require Ada anymore and many software failures can be attributed to bugs that Ada would have caught at compile time. If I were doing flight control software it would probably be Ada checked with Agda.
My previous employer chose C over Ada for all their projects, and they paid for it when you looked at the overruns and additional moneys spent on testing and analysis tools that Ada provides as a language feature.
It would be interesting to have a version of SPIN [0] using this. This [1] looks really fresh. And I love the idea of creating new languages out of a subset. Almost all teams create an ad hoc language subset, formalizing it can be really powerful.
My previous employer chose C over Ada for all their projects, and they paid for it when you looked at the overruns and additional moneys spent on testing and analysis tools that Ada provides as a language feature.