alt Hacker NewsI agree with the core thesis that LLMs + theorem provers might make formal methods cheap enough to be practical in software development.
The biggest issue was always cost. But there's still an alignment problem. Without human supervision, things might drift away from the original specification and intent.
From my own experience, what works best is some kind of Hoare/separation logic (contracts), as these are quite easy to follow and decompose.
Even something as simple as a minimal Haskell subset, plus a bit of LiquidHaskell, can get you really far if you are pragmatic.
IMO the biggest issue was always not knowing what correct is in the first place. The vast majority of software we use, the stuff that's riddled with errors, has those errors largely because what it's supposed to do is vague and never, ever deals with edge cases. You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions.
Perhaps that's the same thing as what you're saying, though: we don't specify these things in detail because it's expensive to spend that much time thinking through it all, when users are largely trained to just accept crashes, glitches, inconsistencies, and the occasional sprinkle of data loss.