Bend 2 and the vibe-coding trap: building a language without surveying the field

Bend 2 and the Vibe-Coding Trap

Liam Powell uses Bend 2 to show how vibe coding lets you ship a whole solution before you understand the problem. Bend 2's demo needs 442 lines of LLM-generated proof to guarantee the player can't win. Powell rewrites the same demo in SPARK—an existing formal verification language—and the compiler proves correctness with zero extra proof lines. The Bend 2 author appears to have missed that the formal verification field already solves this. LLMs won't stop you and say 'this already exists and works better.'