alt Hacker NewsI'm curious which software you have in mind. Ex: seL4 is technically C, but I'd say the theorem prover is doing most of the real work there.
I'm curious which software you have in mind. Ex: seL4 is technically C, but I'd say the theorem prover is doing most of the real work there.
Specifically? I'm thinking of qmail.
qmail was at one point the second most widely deployed email server, handling the majority of online mail. It wasn't a research project; it's not obscure. Yahoo used to use it.
And what I mean by track record: After more than a decade after the last published version, a theoretical attack was found requiring special setup uncommon for a sysadmin, and impossible ten years prior.
When anyone thinks about how to build reliable secure software, I think they should be thinking of qmail because it really has no public source-available equal, except maybe djbdns.
seL4 on the other hand makes some specious claims about some ten year old version of itself, and so few people have even heard about it you thought it important to remind it is "technically" C -- qmail isn't like that at all: There is no prover, no test suite, and almost no metaprogramming of any kind. It's just C.