I 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.
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.