I’m the author of a tutorial on Rocq.

I’m surprised at the negativity on HN. We all want bug-free code and this is a way to not just reduce bugs, but eliminate whole classes of bugs.

Moreover, with proven code, we can have rock-solid libraries and code reuse.

Also, proven specifications allow LLMs to do divide-and-conquer when generating code. You can ask it to generate part A that does X, assuming part B will do Y. And then ask it to generate part B in parallel. And know that, when merged, the code will work.

And, provable code is good for LLMs because it will let LLM creators study hallucinations. The proof checker can identify what is a hallucination and what is not. This means LLMs may learn what they don’t know!

I’m not saying LLMs with proven code is nirvana. There are parts of systems where it doesn’t apply. Specifications are often complex and difficult to understand. Some important details are hard to write a spec for. And specs can miss things. But code proven correct by LLMs has potential to do real good.