4 ms·
> 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 https://sel4
by bstx 12y ago
> 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 https://sel4.systems
Possibly one of the most trustworthy pieces of software there is.
- prodigal_erik 12y agoMan, 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.
- Intermernet 12y agoThe 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 http://ssrg.nicta.com.au/projects/seL4/tech.pml
- Dewie 12y agoSo what did they do? Write the code in C and then proved it with Isabelle/HOL? Extracted C code from Isabelle/HOL?