> seL4 is 9000 lines of C and took 11 person-years to verify. How big is OpenSSL?
Total market cap of the top three tech companies is more than a trillion dollars. Even a hundred times more resources is affordable for them given the criticality of the project. The replacement does not have to be written in C, it can be written in ML-like languages and expose an external C interface.
> Also, verification isn't a magic bullet, you need a good spec.
True, but drawing from the CompCert anecdote, I suspect bugs in a verified implementation would be orders of magnitude less likely.
Total market cap of the top three tech companies is more than a trillion dollars. Even a hundred times more resources is affordable for them given the criticality of the project. The replacement does not have to be written in C, it can be written in ML-like languages and expose an external C interface.
> Also, verification isn't a magic bullet, you need a good spec.
True, but drawing from the CompCert anecdote, I suspect bugs in a verified implementation would be orders of magnitude less likely.