Bend · a new programming language · Sept 2026
What if code could do many jobs at once, and prove it still follows your rules?
That's Bend, a programming language made for a world where AI writes much of the code. See its two big ideas in about a minute. No programming knowledge needed.
- Many jobs at once, spread over every core of your computer, or a graphics card
- Rules written down by people, precisely enough for a computer to check
- Every change checked against them, mathematically, even changes an AI wrote
1Side by side
A bank's AI support inbox just got 100 messages.
An AI has already guessed what each one is about, and how sure it is. For every message, the program decides who answers: the bot, or a person. That's 100 small jobs. Let's get through them.
A GPU has thousands of small cores. 100 of them are enough here.
Simplified on purpose: in each round, every busy core handles one message. Real GPU cores are individually slower than CPU cores, and splitting and joining the work costs a little time, so real speed-ups are smaller than these rounds suggest.
Doing independent jobs at the same time, on many workers.
- It works here because no message needs another message's answer. Jobs that depend on each other still have to wait their turn.
- More workers help only up to a point. Eight cores can't beat 13 rounds, and the work has to be shared out evenly.
1Where Bend comes in
Bend makes splitting the work the easy part.
Use one core unless told otherwise. Using all of them means extra coordination code (threads and locks), where small mistakes cause rare, hard-to-find bugs. Using a GPU usually means writing a second program in a special GPU language.
You say “split this in two”. Bend spreads the halves over every core, or over the GPU, and adds the answers back up. No threads, no locks, no GPU code.
Press the button to watch how Bend shares out the same 100 messages.
You, or the AI writing the code, still decide where to split, and the halves should be about the same size. What Bend guarantees is that the halves can't get in each other's way: a Bend function can't secretly change data that another one is using.
2Laws and proofs
But what happens when an AI changes the code?
Here's the part of the inbox that decides who answers. It checks its rules from top to bottom, and the first rule that fits decides. The bank has one thing it will never accept going wrong:
A fraud report always goes to a person.
See the real Bend code
The rules, as the program has them now
The law, and the AI's proof of it
- The change
- The agent's test
- Bend's proof check
What Bend printed
A rule that must always be true, written precisely enough for a computer to check.
People write the laws. In Bend they live in a file called LAWS.bend, which the AI isn't allowed to change.
An argument that the code obeys the law in every possible case, not just the ones someone tried.
The AI writes the proof. Bend checks it, in about 0.2 seconds here. How can it cover every score without trying them one by one? Like algebra: it works through the rules with the score left unknown. If there's no valid proof, the change doesn't go in.
A test tries examples. A proof covers every case.
3With an AI agent
Now let an AI agent make changes all day.
Agents write code faster than people can review it. Pick a change the agent might make, then send it down both roads.
Without Bend
tests + reviewWith Bend
law + proofThe agent's messages, tests and review on this page are illustrations. The Bend checks are real: every version of the rules shown here was run through the Bend checker, and each result is what it printed.
4The whole picture
Who does what, when an AI writes the code.
Write the laws
What must always be true. Short, precise, and owned by humans.
LAWS.bend
Writes the code and the proofs
As fast as it likes, as often as it likes.
PROOF.bend
Checks every proof
In about a second or less, so it can run after every edit.
acceptedback to the AIRuns it side by side
Accepted code runs split across every core, or on a GPU.
a b = f(x) g(y)
If the AI could edit the laws, it could weaken a law until its change passed. Keeping the laws file in human hands is up to your team, for example with required review on that file, as for any critical file.
Bend runs independent jobs side by side, on every core or a GPU. You say where the work splits; Bend shares it out.
People write laws: rules that must always be true, stated precisely. Like “a fraud report always goes to a person”.
Every change, even one written by an AI, needs a proof that the laws still hold. Bend checks it in about a second. No proof, no change.
Bend's own website calls it a fast language that blocks AI mistakes via proof
, and sums it up in four phrases. Here they are, translated:
It turns into fast machine code. On one core, close to C (a classic fast language) in its makers' own tests.
The same code can run on a graphics card's thousands of cores, which usually needs a special GPU language.
Its checks are real mathematical proofs, like those in Lean, a tool mathematicians use.
It reads a lot like Python, a language many people already know.
Keep in mind
What Bend does not promise.
Everything above is real, and narrower than it might sound.
It only checks the laws someone wrote.
A rule nobody wrote down isn't protected, and a law written too loosely passes too easily. In our own trial, a law that was too weak kept passing while the code was still wrong.
It doesn't make AI-written code bug-free.
It stops changes that break a law. Everything the laws don't cover still needs tests and review.
It checks the program, not the AI model.
If the AI labels a fraud report as a question, the law has nothing to say. Bend proves what the code does with a label, not whether the label is right.
Parallel isn't automatically faster.
It helps when work splits into even, independent pieces. GPUs shine on number-heavy work. In our business-rules trial, 8 cores were 3.1× faster than one, and plain Python was still faster than Bend.
A proof covers the source code.
The compiler that turns it into a running program is trusted, not proven, and it is young. A proof can't catch a compiler bug.
It's brand new.
Version 2 came out on 17 September 2026, and its own guide says to expect bugs. It runs on Linux and macOS. This page explains an idea; it isn't a recommendation to run production systems on Bend yet.
For the technically curious
The code behind this page is real.
The router, the law and the proofchecked with Bend 2.0.25
Three versions of one file: the original rules, the AI's fast lane, and the AI's fix. Each was run through bend, and the output below each is exactly what it printed (about 0.2 s each). A runtime spot-check confirms the failure is real: with the fast lane, route(Fraud{}, 99) returns Bot{}; after the fix it returns Person{}.
The other changes in chapter 3 were checked the same way: “billing from 80%” passes, and “skip unsure fraud” fails with expected : bot_if(Cmp.is_lt(U32.cmp(conf, 60))). Its spot-check, route(Fraud{}, 55), returns Bot{}.
The parallel programcompiled and run
The inbox from chapter 1 as a Bend type: either one message, or two smaller inboxes. triage uses Bend's parallel call, a b = f(x) g(y), to do both halves at once. The router above is in the same file.
We ran it on an inbox of 1,048,576 made-up messages (Docker, 8 CPU cores). It gave the same answer, 590,351 messages that need a person, on 1, 2, 4 and 8 threads: 44 ms on one thread, 26 ms on two, 19 ms on four and on eight. The work per message is tiny, so it stops scaling early. The GPU version, triage!(inbox), compiles; our test machine has no GPU, so we ran it with the GPU switched off, and it gave the same answer. We have not measured GPU speed ourselves.
What is simulated on this pageand what isn't
- The 100-message inbox, the rounds and the timings in chapter 1 are a simplified model of Bend's split-in-two scheduler, not a measurement.
- The AI agent's messages are scripted. The “agent's test”, the human review step and the outcomes in chapter 3 are illustrations of how teams usually ship code.
- Real: every version of the rules, the law, the proof, the checker's verdict and output, and the runtime spot-checks.
- The rules pane in chapter 2 shows the router as plain-English rules read top to bottom. That matches what the Bend code does: in the fast-lane version the confidence check runs before the topic is looked at; in the fixed version the topic is looked at first.
Sourceswhere the claims come from
- bend-lang.com: the pitch, the LAWS.bend and PROOF.bend convention, and the speed claims (theirs, measured on an Apple M4 Max).
- The Bend guide: the parallel call and the
!for the GPU, laws and{==}proofs, and “Bend is still evolving. Expect bugs.” - Our own ProofDesk trial (September 2026): four compliance laws proven, five out of five injected bugs rejected in about 0.2 s each, a law that turned out too weak, and the Bend versus Python timings.