Bend · two interactive demos

No programming knowledge needed

See what Bend does

Bend is a new programming language, released in September 2026. Its makers pitch it for a world where AI writes much of the code, and it makes two promises. Each demo below shows one of them. You press the buttons.


Demo 1 of 2 · Speed

A pile of documents

Here is a pile of 64 documents: contracts, tickets, emails, it doesn't matter. An AI model reads each one and decides whether it is risky. We want one number back: how many are risky? As you play, watch two things: how long it takes, and whether the answer changes.

Your laptop · 8 coresidle

Nothing has run yet. Press Run and watch the documents get read.

Time taken
not run yet
Risky documents found
not run yet
The pile is cut into
1 piece
1 · What am I looking at?

Each small square is one document. Grey means nobody has read it yet. The eight bars above the pile are your computer's eight processor cores: eight workers that can each read a document at the same time. Press Run.

The usual way

One document after another. One core works, seven wait. 64 ticks.

With Bend's parallel call

Independent pieces at the same time. 8 ticks on eight cores, 1 on a graphics card. Same answer.

That's one reason people noticed Bend: the speed-up came from writing one line, not from managing threads. But speed is only half of what it offers. The other half is about trust.


Demo 2 of 2 · Checked rules

A rule the code must never break

Some things a program does must never go wrong, however often the code changes and whoever changes it. Bend lets you write such a rule down and have the computer check it. Here is a small, real example in four steps.

Step 1

The situation

A bank's help desk gets thousands of messages a day. Before anyone replies, a small program called the router decides who should answer each one: the chatbot, or a person. To help it, an AI classifier reads each message first, labels what kind it is, and says how sure it is.

A customer writes"My card was just used in another country. It wasn't me."
The AI classifierLabels it Fraud · 99% sure
The routerPicks who answers
Answered byFraud specialist

How the router decides today

  • QuestionThe bot answers if it is at least 70% sure. Otherwise, a person.
  • BillingThe bot answers if it is at least 85% sure. Otherwise, a person.
  • FraudAlways the fraud specialist, a person.
Step 2

The rule the bank cares about

A fraud report must always reach a person. Never the bot, however sure it is.

Fraud report→a person✓ always
Fraud report→the bot✗ never, not even at 99% sure

Why? Someone whose money is being stolen needs a human who can freeze the card now, not an automatic "Thanks for your message!" Right now this rule is just a sentence in a document. Nothing in the code enforces it. The router happens to follow it today.

Step 3

The programmer writes the rule down in Bend

Bend knows nothing about banks or fraud. The rule only exists because a person turns the sentence into something exact, using the program's own names. In Bend, that is called a law.

The requirement"A fraud report must always reach a person."Decided by: the bank
The lawlaw fraud_goes_to_a_person, three lines of BendWritten by: a programmer, before any change
What Bend checksFor every possible score, the router hands a fraud report to a person.Done by: Bend, on every change

Three words the law uses

Handler: who can answer

Bot Agent Specialist

This is a type: a list of what a value is allowed to be. A handler is always one of these three, never anything else.

is_human: the bank's meaning of "a person"

Bot→False Agent→True Specialist→True

A tiny function the bank writes once, separately from the router.

U32: the classifier's score

012…4,294,967,295

Any whole number in that range. Real scores stay between 0 and 100, but nothing in the code promises that, so a rule about "every score" must cover them all.

The law, line by line

law fraud_goes_to_a_person:
A law, with a name. law is Bend's word for "this must always be true". It's a claim about the program, not a piece of the program.
for conf: U32
For every possible score. conf is the classifier's confidence. Not a sample, not the scores someone thought to test: all 4,294,967,296 of them.
{is_human(route(Fraud{}, conf)) == True{} : Bool}
  • route(Fraud{}, conf): run the router on a fraud report with that score. This is the ordinary program.
  • is_human( … ): is whoever it picked a person?
  • == True{}: the answer must be yes.
  • : Bool: both sides are yes/no values.

The Bend syntax here is law, for, and the braces {a == b : T}, which mean "a equals b, and both are of type T". Everything else (route, is_human, Fraud) is a name from this program.

Step 4

Now try to break it

The router below is real Bend code. Change it however you like with the controls, then ship the change. Do it first with the law off, where the rule is only a sentence in a document. Then switch the law on and try exactly the same thing.

Your goal: get a fraud report answered by the bot.
The law

Your edits to the router

The lawOff

            

The router's codeOriginal

            

Highlighted lines are the ones your edits changed.

See the whole file Bend checks

            
  1. 1Code changed
  2. 2Bend checks the law
  3. 3Result
At the help desk

    Nothing here is mocked up. Every edit you can make was run through the real Bend checker (version 2.0.25), and the output shown is what it printed.

    In technical terms

    What Bend actually did

    Four pieces were involved. Only one of them is Bend doing anything clever; the rest were written by people or an AI.

    The rule law fraud_goes_to_a_person

    A property someone specified. Bend doesn't know what fraud is. It knows what route returns.

    Written by the bank's team
    The program def route(cat, conf)

    Ordinary code. It can change as often as anyone likes.

    Written by developers or an AI agent
    The proof def fraud_goes_to_a_person(conf): {==}

    Code whose only job is to show the law holds. Here it is one line.

    Written by whoever changes the code
    The check bend router.bend

    Accepts the file only if every proof in it holds. About 0.2 seconds here.

    Run by Bend, on every change

    How one line covers every score. {==} means "work out both sides and check that they match". Bend works out route(Fraud{}, conf) with conf left unknown, like algebra. The fraud branch never looks at the score, so it comes out as Specialist{}, and is_human(Specialist{}) comes out as True{}. That matches. No scores were tried one by one: the unknown stands for all of them at once.

    Why the speed-up failed. With the speed-up, working out route first meets the question "is conf at least 95?". With the score unknown, Bend can't pick a branch, and one of the branches leads to the bot. No proof can exist for that code because the law really is false there: a fraud report scored 99 goes to the bot, as the help desk showed.

    For harder laws the proof is longer: going case by case, or step by step through a list. Bend checks those the same way. Writing them is real work, which is where AI agents come in. A failed check can also mean the proof needs fixing rather than the code, which is why Bend points at the exact step that failed.

    How this differs from a test. A test runs the code on examples someone picked. This law covers every score, including the ones nobody thought to try. But it covers only this one property. It says nothing about whether the router is right in any other way.


    Why this matters for AI-written code

    Now put an AI agent in the loop

    AI coding agents can change code much faster than anyone can review it. A law gives the system something exact to check every time the relevant code changes. Here is the speed-up from the demo, with an agent making it.

    01 · YOU ASK

    "Make the help desk faster."

    02 · THE AGENT EDITS

    It adds the 95% speed-up

    It looks sensible: most messages the classifier is that sure about really are routine.

    03 · BEND CHECKS THE LAW

    The check fails

    In about 0.2 seconds. The error points at the exact spot: a fraud report scored 95 or more reaches the bot.

    ✗ Law broken: not merged
    04 · THE AGENT TRIES AGAIN

    It keeps the speed-up, except for fraud

    Questions and billing can take the shortcut. Fraud never does. The law holds.

    ✓ Law holds: merged

    Nobody had to spot the problem in review, and nobody had to think of testing a fraud report scored 95 or more. The rule was written once, by people, and it was checked again the moment the code changed. The check is quick enough for an agent to run after every single edit, not once a night. (We ran the agent's second attempt through the checker too: it passes.)

    This does not make the agent's code correct in general. It means this particular promise can't quietly break, however many times the code is rewritten, as long as the check runs and the law stays as written.

    Who owns the law matters

    If the agent could edit the law, it could weaken the law until its change passed. Bend's convention keeps laws in their own file, LAWS.bend, which people write and agents don't touch. The agent writes the code and the proofs, and bend PROOF.bend is the check. Keeping the laws file off-limits is up to your team, for example through required code review, just as for any other critical file.


    Keep in mind

    What Bend does not guarantee

    Everything above is real, and it is narrower than it might sound.

    1. 1

      It checks the rules you write, not the ones you meant.

      A rule nobody wrote down isn't protected, and a rule written too loosely passes too easily. You saw this in the demo: fraud going to a general agent passed, because the law only asks for "a person". In our own trial, a rule that was too weak kept passing while the code was still wrong.

    2. 2

      It doesn't make AI-written code bug-free.

      It catches changes that break a law someone has proven. Everything the laws don't cover still needs tests and review.

    3. 3

      It covers the program's own logic, not the outside world.

      The law trusts the label it is given. If the classifier tags a fraud report as a plain question, the router treats it as a question and the law has nothing to say. The classifier itself, and anything that talks to networks, databases or files, is outside what Bend proves.

    4. 4

      Parallel speed has limits.

      Your hardware sets a ceiling (you hit it at eight pieces in demo 1), and so does how evenly the work splits. Faster than one core is not the same as faster than other languages: in our trial, ordinary Python ran the same business rules faster than Bend did.

    5. 5

      Bend is young.

      Version 2 came out on 17 September 2026, and its own README says to expect bugs. A proof covers the source code; the compiler that turns it into a running program is trusted, not proven. This page explains the idea. It isn't a recommendation to run production systems on Bend yet.


    For the technically curious

    What Bend actually is

    Now that the pictures are in your head, the words are easy.

    Category
    A general-purpose programming language with Python-shaped syntax
    Parallelism
    The a b = f(x) g(y) parallel call. Fork-join across cores or GPU. No threads, no locks, no kernels
    Why that is safe
    The language is pure and affine (a value is used at most once), so two halves cannot interfere
    Laws and proofs
    The type checker is the proof checker, as in Lean or Rocq. A law is a type; a proof is a definition of that type. No tactics
    The gate
    bend PROOF.bend fails while any law is unproven and prints "All terms check." once they all hold
    Speed of the check
    About 0.2 s for demo 2 and for our small trial; the project claims a second at most. Lean and Rocq can take minutes
    Targets
    C, CUDA, Metal and JavaScript. The JS target runs sequentially
    Status
    Released 17 Sep 2026 by Victor Taelin / Higher Order Company. Early

    Every Bend snippet on this page was run through Bend 2.0.25. Demo 2's router, law and proof, each edit you can make, the checker output for each, and the agent's second attempt were all checked for real. The router is a trimmed version of the one in our ProofDesk trial. Demo 1's code compiles and runs on both the CPU and GPU paths, with risky and documents defined elsewhere in the file. The 64-document animation itself is a simulation in this page: its timings model Bend's fork-join scheduler on eight cores, ignoring join overhead, so real speed-ups land a little below the ideal shown.