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 ).


Andras Slemmer wrote:
Heartbleed is caused by an unchecked memcpy. In particular the size of the memory chunk to be copied is retrieved from a client request and and is not checked



after Noon Silk <noonslists@gmail.com> wrote:

it's a "why is anyone still using c!" issue.

http://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=96db9023b881d7cd9f379b0c154650d6c108e9a3


--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@TCD, Head of Foundations & Methods Research Group
Director of Teaching and Learning - Undergraduate,
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                          http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------