The Bend 2 critique names a specific vibe-coding failure mode: shipping a large solution before learning the problem already has one
Liam Powell's 18 September post argues Bend was built around formal verification without its author apparently knowing the field exists, and backs it with a side-by-side: Bend needs 58 lines to specify simple game laws plus a 442-line AI-generated proof, while the equivalent SPARK program is far shorter and discharges automatically with GNATprove reporting "Success: all checks proved (12 checks)". His generalizable claim is the useful part, that LLMs compress implementation time enough to let you finish a substantial system before the research that would have told you not to build it. The counter-argument worth holding is that SPARK's automation only covers the proof obligations it can discharge, so the comparison favors SPARK on the chosen example.
↳ Follow the thread