Bend 2 and the Vibe-Coding Trap

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 and I can see why someone would want a language that does that. There are actually a few major problems with this idea; however, that's not what this article about. Instead I want to talk about how the Bend itself seems to have fallen in to a common trap with vibe-coding that I don't see mentioned much.

Let's start with a baseline of what Bend requires the developer to write for its demo on the home page:

https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend