Bend 2 goes public: a LAWS.bend file the compiler proves, so an AI cannot merge an edit that breaks it

Bend (Higher Order Co)·high signalXBlueskyLinkedInCopy link

Bend 2 from Higher Order Co went public on 2026-09-17 and hit 502 points on Hacker News. Humans write theorem statements in LAWS.bend (for example `law add_zero: for x: Nat {Nat.add(x, 0n) == x : Nat}`) and the AI writes the discharging proofs in PROOF.bend; `bend PROOF.bend` fails until every law is proved, making it a commit gate rather than a linter. The core is BendTT, an affine dependent type theory in the family of Lean and Rocq, but the authors claim type checking finishes in about a second where comparable systems take minutes. Python-shaped syntax, compiles to C, Metal, CUDA and JavaScript with automatic parallelization across cores or GPU, Apache 2.0.