> The fact that there are downsides doesn't make everything else false. When we say something can be done but mean that it can be done only by a select few, at

> The fact that there are downsides doesn't make everything else false. When we say something can be done but mean that it can be done only by a select few, at great effort, and at a scale that's orders of magnitude smaller than what that "thing" normally is, then the meaning of "can" is misleading. > ~100KSLOC (e.g., CompCert) The total proofs may come out to that, but it corresponds to a ~10KLOC program (without proofs). > A future might exist where computers are fast enough and where we've uncovered better algorithms in that space so that something else could take the place of Coq and lessen that workload to something manageable for a typical project The problem is that the gap between programs that can be verified end-to-end with the semi-manual deductive proof technique used by Coq and other proof assistant and the typical software has been gradually growing, as the scale of software has grown faster than the scale of effective deductive-proof techniques. Today we can verify smaller programs relative to the average program size using such techniques than we could twenty and thirty years ago (although that's not to say that our ability to use that particular technique for small but critical components hasn't improved, and that is where that technique is hoped to be more widely applied). Which is why many in the formal verification space are looking in other directions when it comes to verifying the actual code, mostly methods that forgo soundness, like concolic testing and its descendants.