[bstx]

> I'm not saying writing secure software in C is inherently impossible, but I'm not aware of it having ever been accomplished

https://sel4.systems

Possibly one of the most trustworthy pieces of software there is.

[Intermernet]

The sneaky thing they did is write seL4 in Literate Haskell, and then translate it to C. That involves some serious understanding of both languages!

http://ssrg.nicta.com.au/projects/seL4/tech.pml

[prodigal_erik]

Man, I'd forgotten about that project. I wonder how much of the code could have been written differently and how much was effectively dictated by the theorem prover. Those are probably the very first people in the industry who deserve to be called engineers.

[Dewie]

So what did they do? Write the code in C and then proved it with Isabelle/HOL? Extracted C code from Isabelle/HOL?