Hacker News Reader

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

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.

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