|
|
|
|
|
|
by mehrdada
4443 days ago
|
|
|
> 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. |
|
|