Andrew Butterfield
No, it's a "why does anyone use open-source software for critical applications" issue.
The safety critical industries use C and Ada by and large, but restrict the language to safe subsets, - in particular operations like memcpy, or dynamic memory allocation are ruled out (google MISRA-C or SParkAda).
'though I'm sure the nice folks at Galois might have some interesting insights here…
Andrew Butterfield
PS - interestinglly, the first down-to-code formal verification of a O/S kernel (google seL4) used Haskell as a prototype language and then derived a formal Isabelle/HOL specification from that - the code verified was hand-written in C ( a safe subset ).
I don't see what any of those points have to do with open-source software. Does the proprietary nature of MISRA-C and seL4 somehow make them better at their job, or is it (as I suspect) irrelevant to their job? Likewise (implementations of) SPARK ADA, Haskell and Isabelle are open source; does this make them untrustworthy? Regards, Chris