Re:It’s time to kill the web app
by moosingin3space on Saturday September 23, 2017 @08:04PM
(#15322475)
I wouldn't consider seL4 to be a "C project". Yes, their github repository is mostly C, but the process of writing seL4 was extremely involved: write the kernel in Haskell, then write it again in C, then prove that the C is equivalent to the Haskell. seL4 is ~9000 lines of C, ~600 lines of asm, and ~200,000 lines of Isabelle (theorem prover).
I don't disagree with your use of OpenSSH as an example.
I'd say OpenSSH (since SSH2) has a better track record than most webapps, as unfair a comparison as that is. In terms of local robustness, there's SeL4, which is also a bit unfair (since it took about a decade for a team of geniuses to prove enough properties to make it probably not very buggy).