September 18, 2026 Bend 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”.

I obviously do not like the design decisions made in Bend and I wanted to present those, however that’s been overly conflated with the main point that I’m trying to make below. I don’t want to edit this now and make it seem like any existing comments are being overly harsh so I feel that the best solution is explaining what my mental model of the article looked like while writing it instead. Here is a comment by the author of Bend.

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.

So what’s the problem I have with this? Why am I calling it a vibe-coding 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.

It’s notable that 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. To clearly demonstrate why this is a problem, let’s recreate the same program that Bend uses as a demo in SPARK, an open source language and compiler for formal verification.

To be fair to Bend, I completely vibe-coded this, I just told a LLM to recreate the demo in SPARK with no further guidance:package Game with SPARK_Mode issubtype Column is Integer range 0 .. 11;subtype Row is Integer range 0 .. 7;type State is record X : Column; Y : Row; Won : Boolean;end record; Start : constant State := (8, 5, False);function Wall (X : Column; Y : Row) return Boolean is(((X = 3 or X = 11) and Y <= 3)or ((Y = 3 or Y = 7) and X <= 3));function Cell (X : Column; Y : Row) return Character is(if Wall (X, Y) then '#' elsif X = 1 and Y = 1 then 'F' else '.');-- Inductive invariant: outside the sealed room, off walls, not won.function Safe (G : State) return Boolean is((G. X > 2 or G. Y > 2) and not Wall (G.

X, G. Y) and not G. Won)with Ghost;procedure Step (G : in out State; Key : Character)with Post => (if Safe (G'Old) then Safe (G));-- Both Bend laws, including the actual cell drawn by the terminal.function Replay (Keys : St...