Bend 2 launches, a language that blocks AI mistakes by proof

Bend 2 launched today, from the Higher Order Company. The project's landing page describes it as a fast language that blocks AI mistakes by proof, and the top comment thread on Hacker News reached 198 points in about two hours. The bendlang/bend repository has 20,222 stars and its Apache-2.0 code was last pushed today.

Bend 2 is not compatible with Bend 1. The project says out loud that "Bend 2 is a new language. Bend 1 programs and HVM do not carry over."

What the language actually adds

The mechanism the project leads with is a file called LAWS.bend. A team writes rules there: things about the program that must always hold, whether the AI is writing the code or a person is. A companion PROOF.bend file, which the project says the AI is expected to write, has to convince Bend's type checker that every law still holds after the change. If it does not, the code will not compile, so a change that breaks a stated rule cannot reach the main branch.

The site gives a small game as the example. The stated law is that no sequence of moves can lead to a win. Asked to make the board wrap around, without LAWS.bend, the AI's code merges and wins are now possible. With LAWS.bend, the AI has to keep trying until it produces a version that both satisfies the request and can prove the law still holds. The project's phrasing: "Merging a bug is mathematically impossible: it is a theorem."

The performance numbers, and their caveat

Bend claims to run near the speed of C on one core and roughly a hundred times faster on a GPU, and to check proofs in about a second on files that other systems (Lean, Rocq) take minutes on. Every chart on the landing page carries the caption "Apple M4 Max, lower is better," so those are the project's own numbers on one machine, not an independent benchmark.

The project is open source (Apache-2.0), so a team can install it and test the claims. It says Bend "works best on the back-end, on Linux and on macOS" and asks for issues on anything that goes wrong.

The project points to two papers on the site for the parts a reader would want to inspect: BendTT, an affine dependent type theory that is Bend's core, and BendRT, the parallel runtime that targets CPUs and GPUs. The proof language is documented in a GUIDE.md file in the repository, which the bend guide command prints locally.

Bend 2's ambition is bigger than shipping one more programming language. The wording on the landing page frames it as a language for the case where people stop writing code themselves and start telling AI what to do. Whether that framing lands or not, the practical thing it offers a team today is a compile-time refusal for the rules a team wrote down and cares most about, checked in about a second on ordinary hardware.

Source

• Bend, the project's own site
• bendlang/bend on GitHub
• Hacker News thread