GoKawiilBend 2 and the Vibe-Coding Trap
September 18, 2026
[Bend just serves as a useful example of my general point regarding vibe-coding as it is recent, high-profile, and has aspects that make it easy to use as an example. I don’t know anything about the author’s history with designing languages or if they actually did consider the tradeoffs below and made what I think is a poor choice. Feel free to replace “the author” below with “a hypothetical author who could have created the same thing”.]
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
I won’t reproduce it here because the code isn’t too important. What is important for this article is that it’s quite a bit of code. It’s 58 lines of code just to state that the player can never touch the flag or win the game. There’s also other problems in that the LLM can redefine the Game subprograms to do anything; however, that’s once again not the point of the article.
Next up lets look at what the LLM writing the code for this program needs to write in order to prove the “laws”:
https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend
That’s a lot. 442 lines of code to prove those simple properties.
... continue reading