Hacker Newsnew | past | comments | ask | show | jobs | submitlogin
Prediction: AI will make formal verification go mainstream (kleppmann.com)
10 points by raphlinus 4 months ago | hide | past | favorite | 2 comments


What a grim future, just chat with a bot without ever seeing the code


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.




Consider applying for YC's Summer 2026 batch! Applications are open till May 4

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: