The seL4 microkernel was written by hand, in C by fallible humans [1]. However, the authors were careful to do so in such a way that it was feasible to subsequ

The seL4 microkernel was written by hand, in C by fallible humans [1]. However, the authors were careful to do so in such a way that it was feasible to subsequently prove its equivalence to a Haskell program that was proven consistent with the seL4 specifications. My point is, the degree to which you can expect "safety" from a program (whatever that word means to you) is predicated on the degree to which you can trust the competence and practices of the developers, and the degree to which your definition of "safety" applies to the program's specifications. Remember, all programming languages are Turing-complete, which means you can blow your foot off with any of them if you're not careful. [1] http://www.nicta.com.au/pub-download/full/7371 http://www.nicta.com.au/pub-download/full/7371