Comment by nilkn

Yes, this is a challenge, but I don't think it's as damning as it sounds.

First, the same kind of issue exists with any kind of testing. We all know that having unit tests and integration tests doesn't mean the software is correct and bug-free. Yet we still often believe it's worth investing in writing and maintaining a test suite. Formal methods is an additional level of assurance that I suspect we'd generally find worth it for critical software if it were easy enough to implement, even if it's not perfect.

Second, because formal verification has been so hard, nobody has really bothered making a serious attempt at solving the spec problem before (at least not to my knowledge). We've spent decades building frameworks that make writing tests really easy. We really have not come close to investing the same kind of effort into building frameworks and tools to make writing formal specs easy. I can imagine a world where we have sophisticated tools that help us create specs, plus real-time verification infrastructure that automatically reverifies code against the spec on each PR.

Third, and perhaps most importantly, there are many industries where this is actually low-hanging fruit: aerospace, medical devices, etc., actually already have formal specs that are verified manually by human engineers to satisfy certification requirements. I believe that's a more natural starting point vs. trying to scale formal methods for all software in general.