This is what's going to happen:
- Formally verifiable specs improve the absolute garbage that is LLM generated code to an acceptable degree.
- Realization: Providing formally verifiable specifications is actually a lot of work
- Light bulb: Oh, let's have the LLM generate formal specifications.
- Realization: Oh, actually those autogenerated specifications aren't correct
- Conclusion: We're back to square one.
There is a reason why most code is not formally verified. It's actually really hard (and in many cases arguably not worth it) to express what one would call "standard business logic" in formally verifiable terms.
