> you can use tools to automate the proof-work, as you said so yourself.

The language doesn't appear to be designed around supporting existing tools (either by exporting to Why3 or manually interfacing with existing tools). I'm not against shipping the whole proof or storing it on a cache server, I'm against the idea of having a LLM write it all. Even having the LLM only write proofs for subprograms that take a long time for ATPs to prove would work.

For the example in the article, the LLM had to write it exactly once without any iteration and it proved in a second, which I assume was mostly startup time. Having a LLM write 442 lines instead, which I assume also needed some iteration, is a tough sell in comparison.

I'm curious, have you actually tried Bend (for more than 5 minutes)? Or are you more of an expert on this topic than the author who has been deeply immersed in this for 10 years, after it's single day of release? From an outsiders perspective it feels like this is personal to you, and you're being unfairly critical.

It will, there is just too much to do! It is a programming language. With a consistent, non-standard proof system. That compiles to GPUs. We're a small team. Please be patient

You mean the SPARK example?

Because it's a toy problem and I would definitely not take much away from it. Most proofs are basically write-only and impossible to maintain -- you are better off throwing it away. And I mean human-written formal verification here, like Coq and Agda. Take a look at formalized mathematics, they are absolutely massive code bases.