[Haskell-cafe] Heart Bleed bug in OpenSSL
chriswarbo at googlemail.com
Wed Apr 9 09:29:50 UTC 2014
Andrew Butterfield <Andrew.Butterfield at scss.tcd.ie> writes:
> 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?
More information about the Haskell-Cafe