Bend 2 is pitched as a language for the AI coding era: a human writes “laws” the program must obey, an AI writes the implementation and the proof, and the compiler checks that the proof holds. Liam Powell’s objection is not that the idea can’t work. It is that Bend looks like a clean example of a trap vibe coding sets — you can now build a substantial thing long before you know enough about the problem to see that a much better approach already exists.

His evidence is the project’s own home-page demo:

  • Stating the game’s laws takes 58 lines of code — that the player can never touch the flag or win.
  • The proof an LLM then has to write for those laws runs to 442 lines.
  • The term “formal verification” — the decades-old field of machine-checked proofs of program correctness — appears nowhere on Bend’s site or in its codebase.

Powell then rebuilds the same demo in SPARK, an existing open-source language and compiler for formal verification, by telling an LLM to do it with no further guidance. The specification comes out around thirty lines, the proof obligations are discharged by the tool rather than written out by hand, and GNATprove — the checker that ships with SPARK, which searches for the proof itself instead of requiring the AI to supply every step — reports “Success: all checks proved (12 checks).”

That is the whole argument, and it generalises past one language:

  • Vibe coding makes it easy to implement a design that is broken or decades behind the state of the art, because the model hands you a working result immediately and no research is ever forced.
  • Ask an LLM for a language where correctness can be proved from first principles and it will happily build one; it will not stop to mention that computers can already construct complex proofs and that most of the work can be eliminated.
  • The failure mode is not a bad model answer. It is that the model never tells you what you don’t know to ask — which is the same asymmetry some commenters push back on below.

Powell also notes in an edit at the top of the post that he knows nothing about the Bend author’s actual history with language design, and links to the author’s reply, which is worth knowing before reading the piece’s most contested claim.

The 214-comment thread on Hacker News corrected the essay on that claim, supplied the counter-practice, and disagreed about whether the SPARK comparison was fair at all.

What the thread adds

  • LightMachine — the Bend author, replying in the thread (commenters identify him as Victor Taelin). On the “without realising that said field exists” line: “Bend proofs being verbose has nothing to do with me not knowing that inference, unification, or program search exists.” He lists a DevCon talk on formal verification from seven years ago, his Cedille Core implementation of Aaron Stump’s self types from around eight years ago, and Kind-Lang from five years ago — “And I dropped out of Federal University of Rio de Janeiro to study this subject independently… I spent nearly 10 years doing so, daily, on weekends.” He calls it “misleading, if not just a bit malicious, to claim I ‘vibe-coded’ a language without knowing about a field I’ve spent a decade researching about.”
  • LiamPowell — the essay’s author, replying in the same thread: “Sorry. See the edit at the top if you haven’t already. I didn’t realise how much it came off as a critique of you rather than a particular approach to software engineering.”
  • z7, johnfn and simonw — three commenters who each checked the author independently and reached the same conclusion. z7: “I checked the developer’s X account, they have written numerous posts about formal verification, so this specific claim … seems to be false.” simonw supplies the receipts: a 2018 Ethereum formal verification project, Formality, and its repo. johnfn: “Pretty impressive to accuse the author of not knowing formal verification when even minutes of research would immediately prove the opposite.”
  • simonw — the counter-practice the essay says is missing: “I’ve got into the habit of starting any new project with a session where I ask a search-enabled LLM to help me figure out what the prior art for a problem is. It’s saved me quite a bit of time.” capitalatrisk reads the essay as implying the author “should have remembered to ask, as part of the prior research.”
  • bunderbunder — the sharpest counter to that remedy, and the most useful thing in the thread: “I have known using an LLM to do your prior research to itself be a trap. The searches it runs, and the summaries it provides, are all incredibly sensitive to your choice of words. Words you chose from a state of minimal knowledge. So it’s like a particularly perverse version of the anchoring bias: information that could have led you to a better solution is often actively filtered out of the agent’s response precisely because it leads down a different path from your first idea.” His example: “if you ask an agent what’s the best hammer for driving screws, it’s liable not to mention that screws exist.”
  • thomasahle — the technical dissent on the comparison: “GNATprove uses SMT solvers, meaning it’s basically a brute force proof system. Yes, brute-force proofs are easier than symbolic proofs (lean, bend, etc.) because you don’t have to supply a proof. It’s all automatic. But brute-force proofs don’t scale to nearly anything of interest, which is why formal verification has been a niche field for 30 years, until now where LLM can write actual proofs.” captainmuon makes the demand-side version of the same defence: they want to write C# or JavaScript and “tack on preconditions, checks and so on with the same syntax,” which bunderbunder notes is closer to code contracts than to verification.
  • rozap and lbrito — the part of the essay that survives the correction. rozap: “I used to write dumb little programs all the time that explored an idea which was probably bad, and in that exploration I often found that there was a better way to do it, or that I didn’t know as much as I thought I did… But there was learning that happened there, so the process was still valuable. Now you can get a working bad idea without learning anything.” lbrito frames it as the developers-versus-managers split: managers are “laser focused on the final product, the outcome,” while developers were invested in a process that shaped what the product could and should be.
  • wg0 — the project’s own README, quoted back: “The compiler (not kernel) is 99% AI-written and has not been fully audited yet.”
  • mrbluecoat — the line that deflates the whole exchange: on Powell’s admission that he “completely vibe-coded” the SPARK port, “A vibe-coded retort to a vibe-coding tool? Ugh.”
  • golol and time0ut — pushback on tone rather than substance. golol: “I find this to be a mean and misguided post… And he is transparent about his work, which he then gets hounded for. A shame.” time0ut: “it reads like the author is doing the thing they are accusing the Bend 2 guy of.”

The question the thread kept asking

Whether the trap Powell names is actually new. hmokiguess argues it is an old human failure — “We simply don’t know what we don’t know” — and mromanuk takes the counter-position that chasing the better solution is itself the danger: “As a software developer we should fear chasing ‘better’ solutions, that path always lead to procrastination… ‘Good enough’ should suffice in most cases.” ofjcihen lands the compromise that most of the thread seemed to accept: “what the OP describes is a real problem. Regardless of whether or not Bend2 is realistically usable or not, the author definitely does not fit the description of the type of people who are actually causing the issue.”

Handles on Hacker News are pseudonymous, the site publishes no per-comment scores, and the ordering above is HN’s own ranking — so this is a slice of the thread, not a vote on it. The claims commenters make about the Bend author’s history are quoted as their findings; the author’s own account is quoted as his.