Bend: The Language That Blocks AI Errors with Mathematical Proofs

The Bend project offers an unusual answer to a question that comes up ever more often in the age of “vibe coding”: how can you trust code you've never read? The authors' answer is simple — demand a proof.

The Idea

The authors start from a bold assumption: in a “post-AGI economy” people will stop writing and reading code, but they'll still need a way to explain unambiguously to an AI exactly what is required. Natural language is too vague for that, so Bend proposes describing intent in the form of laws and confirming the correctness of the implementation with proofs. The syntax, meanwhile, is close to Python.

How It Works

The central element is the LAWS.bend file, where the developer writes down rules that must never be broken. From that moment on, as the authors envision it, no AI will be able to submit a line of code that breaks a law. Type checking in Bend is at the same time proof checking — as in Lean or Rocq. The difference, according to the creators, is speed: whereas full-fledged proof checkers spend minutes on an average project, Bend fits within a second, which lets the agent check the code after every change.

As a vivid demonstration, they present a game with the law “winning is impossible.” When the AI is asked to add a feature — “make the board wrap around at the edges” — the bug sails calmly into production without LAWS.bend. With the law in place, however, the agent has to rewrite the code until it proves the rule still holds. Merging a bug becomes, as the authors put it, mathematically impossible — it's a theorem.

Speed and Parallelism

Bend compiles to native code and runs on a single core almost like C. The same binary runs on sixteen cores or on a GPU, speeding up, by their claims, up to a hundredfold relative to a single core. Parallelism is presented as a free bonus: no threads, no locks, no kernel functions need to be written — the task is split in two, distributed across all available cores, and assembled back together. In the demonstration, the pow2 function runs on 4096 GPU cores.

How to Try It

Installation comes down to running a script via curl, after which an instruction for the agent is added to AGENTS.md: learn the language with the bend guide command, keep the rules in LAWS.bend, and run bend PROOF.bend before committing. In essence, LAWS.bend is an “AGENTS.md backed by a proof”: the phrase “don't make mistakes” finally becomes checkable by types.

The authors themselves honestly warn that the project is young: it works best on the backend under Linux and macOS, and bugs are to be expected and reported. The language is built on two works — BendTT (an affine dependent type theory) and BendRT (a parallel runtime for CPU and GPU).

Source: Hacker News