Bend 2 is being pitched as a language for the AI coding era: humans write "laws", AI writes implementations and proofs, and the compiler checks that the proofs are sound. That all sounds quite impressive. There are actually a few major problems with this idea; however, that's not what this article is about. Instead I want to talk about how Bend itself seems to have fallen into a common trap with vibe-coding that I don't see mentioned much.
The trap
The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists. A developer can produce an entire language and compiler while missing an approach that an introductory survey of the field would have put directly in front of them.
The field in question is formal verification. Those two words appear nowhere on Bend's webpage or in its codebase. The developer has built an entire language around a field seemingly without realising that said field exists.
Same demo in SPARK
To demonstrate, the author vibe-coded the same Bend demo laws in SPARK (Ada). The package states an inductive Safe invariant and a Replay postcondition that winning and flag contact are impossible—then GNATprove reports:
Success: all checks proved (12 checks).
What was supplied is everything required to prove correctness without having an LLM waste tokens building a 442-line proof from first principles.
Broader lesson
The author of Bend has completely missed that this is the current standard in formal verification. A little research before vibe-coding an entire language and compiler could have substantially improved the result.
This example matters beyond Bend: vibe-coding makes it far too easy to implement a design that's horribly broken or decades behind the state of the art, because you can immediately get a result without research. Ask an LLM for a language where you prove correctness by building proofs from basic principles and it will happily do so—it will never stop to suggest that existing tools already eliminate most of that work.
Originally published on Liam Powell's Blog.