$cat ~/posts/bend2-manifesto

bilingual · en / pt

← /blog

the bend2 manifesto

2026-09-19·en·8 min read·bendlanguagesaiproofs

Bend2 shipped this week (two days ago, as I write this), and I want to defend the idea behind it before the discussion turns into a benchmark fight.

Scope warning: I have not run Bend2. I have not installed it, have not written a line of it, and have no opinion on its ergonomics. What I have is an opinion on the bet, and I think the bet is right.

what broke

Over the last two years the amount of code I read grew past the amount of code I write. That is not a complaint, it is just what the job looks like now.

And that is where a problem nobody has solved shows up: human review measures whether code looks right. That is literally the job. Read, understand the intent, look for the case the author forgot, and approve when nothing turns up.

Except "looking right" is exactly what a model trained on human code does better than anyone. It produces the most plausible code it can. Plausible is the metric it optimizes for, and plausible is the metric my review applies. Both point at the same target, and the bug lives in the blind spot they share.

I have already written here about four things I broke in production. None of them failed on bad math. They failed on seams: a constant that never reached the function, one scope keyword, a check run in the wrong order. All of them passed review. All of them looked right.

Tests do not fix this either, for a harder reason: a test shows a bug exists, never that it does not. You sample the space of inputs and hope you sampled the case that matters.

Scaling AI with a sampling guarantee is a bet that does not add up.

the inversion

What Bend2 proposes is to stop trying to fix review and change the artifact the human maintains instead.

Instead of you writing the code with the machine helping, you write the law, and the machine writes the code and the proof that the code obeys the law. The law lives in the repository, in a file called LAWS.bend, and it is the thing you read, version, and argue about in a pull request.

law you_cant_win:
  for moves: List<Game.Move>
  board = Game.replay(Game.start(), moves)
  {Game.is_won(board) == False{} : Bool}

That reads as: for any sequence of moves, replaying them from the starting state never results in a won board. It is not a test case. It is a claim about every possible sequence, including the ones you never thought of.

The implementation becomes output. The proof becomes output. What you keep is the claim.

the human writes the one part the machine cannot write for them: what counts as correct.

The project's slogan is that merging a bug becomes mathematically impossible, because it has become a theorem. That is strong, and it is literal, with an asterisk I think deserves to be in bold: within the scope of the law you declared. Nothing there protects you from declaring the wrong law. The responsibility did not disappear, it moved, and it moved somewhere much smaller and much more legible.

Trading ten thousand lines of implementation for twenty lines of law is the best deal this profession has seen in a while.

why proof and not more tests

The difference between the two is the difference between sampling and quantifying.

A test says: for these thirty inputs, it worked. A proof says: for every possible input, it works, and here is the argument you can check line by line.

This is not a new idea. Coq, Agda, Lean and Idris have done this for decades, and the reason it never caught on is well known: writing a proof is expensive, tedious, and demands training most programmers neither have nor want. The cost of the proof was always higher than the cost of the bug.

What changed is that there is now a machine willing to do the tedious part. The proof was the bottleneck because it was human labor. It no longer is.

That is why I think this is the first time formal verification has a real shot outside academia and safety-critical systems. Not because the math got better, but because its price fell through the floor.

the objection I take seriously

There is one, and it sits right in the project's own README, stated with an honesty I respect a lot: the Bend2 compiler is 99% AI-written and has not been fully audited yet.

Read that again and feel the size of the irony. The tool that exists to stop AI mistakes was itself written by AI and left unchecked.

That seems to sink the whole thesis. I don't think it does, and the reason is the most important thing in this post.

In a proof system, generating and checking are completely different jobs. Generating a proof is brutally hard and creative, and can be done by anything: you, an AI, a monkey with infinite luck. Checking a proof is mechanical, decidable, and the program that does it is small. It does not matter where the proof came from, because it arrives with the full argument attached, and the checker walks that argument step by step.

So the question is not "is the compiler trustworthy?". It is "is the checker trustworthy?". And the checker is the small part, the part that fits inside a real audit, done by people, once, valid forever.

This is old. A serious proof assistant has always been built this way, with a minimal core that everything else has to convince. That the generator around it is huge, opaque and suspect is the expected shape. It is the design, not the flaw.

I still want to see that checker audited. I want to see people outside the project trying to break it. But the structure of the argument is right, and it is the opposite of "trust the AI": it is "trust no one, demand the argument".

what still doesn't work

Being excited about the idea is not the same as pretending the release is ready, and it isn't.

No type classes, no traits, no macros beyond templates. No LSP, no debugger, no tactics. Type annotation is mandatory everywhere. The numbers are Nat, U32 and F32, and that's it. Strings are linked lists of characters, which means exactly what anyone who has written Haskell knows it means in practice. No TLS, HTTP, JSON or regex. No native Windows, only through WSL. One GPU per program.

This is a 2.0.5 release of a project that just shipped, and the list above is long enough that nobody should be putting this in production this week.

I am not saying use it. I am saying pay attention.

what I now expect

What I wrote about cryptography yesterday applies here, in reverse.

There, the argument was that cryptography treats a new algorithm with organized distrust: an open competition, years of people trying to break it, and only then does it become a standard. And that AI does the opposite, publishing the paper in two weeks and shipping to production in the third.

Bend2 is the first thing I have seen trying to bring that rigor inside the pipeline of machine-generated code. Not asking for trust: asking for proof, and offering a cheap way to produce the proof.

Bend2 might not make it. Most languages don't, and this one carries a list of limitations the length of an arm. But the question it asks does not go away, and it is the right question: if the machine writes the code, what exactly does the human remain responsible for?

Its answer is "for saying what counts as correct". I can't think of a better one.