curl -fsSL https://bend-lang.com/install.sh | shBuild this project with Bend-Lang:
- run `bend guide` to learn it
- write laws to avoid mistakes
- parallelize to make it fast!a fast language that blocks AI mistakes via proof
C speed · CUDA parallelism · Lean proofs
In the post-AGI economy, humans will eventually stop writing and reading code, but we still need an ambiguity-free way to tell the AIs building the world around us what we want done.
With laws, our intents can be much more precise than natural language. With proofs, we can verify that the AI implemented our prompts correctly. And a fast compiler runs it at speed.
That's Bend - and nothing else.
Bend compiles to native code. On one core, it runs nearly as fast as C. The same binary also runs on sixteen cores, or on the GPU, where it runs a hundred times faster than one core.
Bend's type checker is a proof checker, as in Lean and Rocq. Those can take minutes on a mid-sized codebase. Bend takes a second at most, so an AI agent can check after every change.
No threads, no locks, no kernels to write. Split the work in two, and Bend spreads the calls over every core it can find, then joins them back. Now watch pow2 run on 4,096 GPU cores:
How can you trust code you never read? By demanding a proof. LAWS.bend is where you declare laws. From then on, no AI can ship one line that breaks them, ever. Watch it guard a game:
Law: winning is impossible
New feature:
“Claude, make the board wrap around”
Without LAWS.bend:
With LAWS.bend:
Without LAWS.bend, the bug went live. With LAWS.bend, the AI had to retry until it built a wall and proved the law holds. Merging a bug is mathematically impossible: it is a theorem.
LAWS.bend
# LAW: no move sequence leads to victory.
law you_cant_win:
for moves: List<Move> # any sequence of moves
board = replay(start(), moves) # replayed from the start
is_won(board) == False # never leads to victoryPROOF.bend
# PROOF: you_cant_win holds.
def you_cant_win(moves):
# ... written by the AILAWS.bend is AGENTS.md backed by proof.
“Make no mistakes” is now type-checked.
curl -fsSL https://bend-lang.com/install.sh | shBend is made to be driven by an AI agent, so simply copy the prompt below, paste it into yours, and let it build for you:
Build this project with Bend-Lang:
- run `bend guide` to learn it
- write laws to avoid mistakes
- parallelize to make it fast!Hints: ask it for a law on whatever must never go wrong, and to parallelize whatever must be fast. Bend works best on the back-end, on Linux or macOS. On Windows, WSL works well too.
Guide: GUIDE.md is the whole language; bend guide prints it.
Paper: BendTT, an affine dependent type theory, Bend's core.
Paper: BendRT, a parallel runtime for CPUs and GPUs, the VM.
Bend is still evolving. Expect bugs, and please report them.