I'm a big fan of high-assurance code and feel that we should write software as if people's lives depend on it, because they do! But your response is a bit hype

I'm a big fan of high-assurance code and feel that we should write software as if people's lives depend on it, because they do! But your response is a bit hyperbolic and calling someone a zealot or a snake-oil salesman is in poor taste. CompCert and seL4 represent the upper limit of what can be formally verified, and they are relatively small programs. CompCert targets a subset of C99, which is fairly small. Certainly much smaller than C++ and most other production programming languages. seL4 weighs in at 10K LoC and only provides memory protection and process scheduling. The implementation cost ~2.2 py but the proof cost was ~20 py (although they estimate new tooling would reduce this to ~6 py)[1]. Even Gernot (the head of the seL4 project) stipulates that formal verification is suitable only for software that doesn't change much over time, because it's difficult to add new features without breaking the proof. seL4 benefits from decades of iterations on the L3/L4 design. Now imagine trying to sell formal verification of a product like Gmail, which IIRC has a code base churn of ~20%/year. Even using formal methods to create a markup sanitizer would be a huge research project, probably larger than that of Everest's formally verified implementation of the HTTPS stack[2]. Economies of scale have made commodity programming languages designed for low-assurance code ubiquitous. If we ever want to see investment in high-assurance tooling, we have to prove it's value within the existing marketplace. And we can only do that if we are honest about what is possible and what is profitable. So no, we can't just choose to verify any program. We are getting to the point where it is profitable to formally verify small components, like DNS or the WASM bytecode. That's exciting! But it's not as feasible as you or I want it to be. [1]: https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-... [2]: https://project-everest.github.io/ https://project-everest.github.io/