[Haskell-cafe] Heart Bleed bug in OpenSSL

[Chris Warburton]

Andrew Butterfield <Andrew.Butterfield at scss.tcd.ie> writes:

> 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