# Bend 2: proof-checked, and no longer an interaction net > Satyajit Ghana — Head of Engineering @ Inkers Technology > canonical: https://ai.thesatyajit.com/articles/bend-2 > date: 2026-09-18 > tags: programming-languages, formal-methods, gpu, systems, explainer Victor Taelin's launch post for [Bend 2](https://bend-lang.com) packs three claims into two sentences: it's "a new programming language that blocks AI mistakes via *proof checking* — the same technique big AI labs used to solve open math problems, like Navier-Stokes," and it's "also very fast, and runs on GPUs." Each half of that is a different claim about a different system, and they deserve to be checked separately rather than accepted or dismissed as a bundle. So I cloned [bendlang/bend](https://github.com/bendlang/bend) — the project moved out of the [Higher Order Company](https://higherorderco.com) org it shares with [HVM](https://github.com/HigherOrderCO/HVM2) — read the checker, read the 20,000-line Lean mechanization of its core theory, read HVM2's own paper, and ran the numbers in `bench/`. The proof-checking claim holds up better than skeptics of "AI plus formal methods" hype might expect. The Navier-Stokes name-drop is honest about the mechanism and rhetorical about the connection. And the performance story turned out to have a twist nobody announced: the runtime that ships with Bend 2 is not the one that made HVM famous. ## A hundred words of syntax, so the rest of this makes sense Bend's syntax is Python-shaped; its semantics are closer to Haskell or Lean. It's a *pure* language — effects go through an IO monad — with dependent types, and it's *affine by default*: a bound name is used at most once, unless its type is marked reusable (`Data`) and the binder carries a `+`: ```python import Base type Shape is Data: Circle{r: U32} Square{s: U32} def area(x: Shape) -> U32: match x: case Circle{+r}: (3 * r * r : U32) case Square{+s}: (s * s : U32) ``` `is Data` is what lets `r` be read twice in `3 * r * r`; without it, and without the `+`, that would be a type error. That single mechanism — a value has exactly one owner unless its type says otherwise — is doing three jobs at once in Bend 2: it's why the type theory is consistent, it's why the compiler needs no garbage collector, and, as it turns out, it's why the runtime no longer looks anything like HVM. All three show up below. ## Claim one: the checker is real, and it is small on purpose "Proof checking" is not a metaphor here. Bend has `law` (a proposition) and `def` (a proof of it, an ordinary function — there is no separate proof language, no tactics, and the pattern match *is* the eliminator). A law you don't fill is an unfinished axiom; `bend PROOF.bend` either produces a checked term or it doesn't compile, and there is no third option. The interesting engineering question is what, exactly, is doing the checking, and how much of it you have to trust. **The type theory is genuinely unusual.** BendTT — the theory Bend's checker implements, described in Taelin's [companion paper](https://github.com/bendlang/bend/blob/main/paper/BendTT.pdf) — has one universe, `Type : Type`, no hierarchy above it, and datatypes with no positivity restriction. On its own that's the setup for Girard's paradox: a inconsistency that has sunk every naive `Type : Type` theory since Martin-Löf's original 1971 system. BendTT's move is to make paradox-building *illegal for a different reason*: every known encoding of Girard's or Curry's paradox needs to apply some value to a copy of itself, and Bend's affine discipline won't let you copy a function. A `+` binder — the only kind that can be used twice — is only legal over a type of kind `Data`, and no function type is ever `Data`. Try it directly and the checker just says so: ```python law dupf: for +f: Nat -> Nat Nat ``` ``` - expected : Data - observed : Type ``` Consistency-via-affinity instead of consistency-via-a-universe-hierarchy is a real, citable idea — the paper's own related-work section states plainly that, among the linear/graded dependent type theories it knows of, "none uses the absence of contraction *for* consistency." It buys back some of what a universe hierarchy usually forbids: `Type : Type` gives you impredicative, self-referential type-level code that predicative theories reject outright. **The kernel is one file, and it says so.** `bend2/bend.ts` — parser, elaborator and checker together — is 3,734 lines. Its own first comment is unambiguous about the trust boundary: ``` // NOTE: this file was 99% human-designed and audited. // It includes Bend's trusted kernel, including interpreter and checker. // It has a bit of AI slop, but it is the most robust file in the repo. ``` Every rule in the paper is also a comment beside its case in that file. Here's `check-lam`, verbatim: ```ts // T == @q x:A -> B // Γ , x : qA ⊢ f(x) : B(x) ~ u // where u[x] <= q // lhs steps by x while a parameter remains // ---------------------------------------------- check-lam // Γ ⊢ x => f : T ~ u - x case "Lam": { const t_wnf = term_wnf(book, ty); if (t_wnf.$ !== "All") { throw Err(book, ctx, ty, typeless_show(book, ctx, tm), tm.s, lhs.def); } // ... } ``` 3,734 lines for a checker that also parses is a real number to compare against something. Lean 4's own kernel — the analogous "the one thing you have to trust" boundary in a very different architecture — is about 6,000 lines of C++ for its base layer, plus a few hundred more for inductive families. The comparison isn't quite apples to apples: Lean cleanly separates a small re-checking kernel from a large, untrusted elaborator, while Bend's file elaborates and checks in one bidirectional pass, so it's carrying work Lean puts on the untrusted side of its own line. Even so, the whole trusted surface of Bend 2 — parsing included — is smaller than just Lean's checking core. That's a legitimate data point in favor of "small, auditable kernel," which is the entire premise of proof checking as a trust mechanism. **The metatheory is mechanized, not just asserted.** `bend2/bend.lean` is a de Bruijn model of the core calculus, about 21,000 lines, and — I grepped it myself — zero uses of `sorry`. It proves confluence, subject reduction, progress, weak normalization and consistency, the last by a Dershowitz–Manna measure over pending recursive calls: ```lean theorem consistency_holds : consistency := by intro β a r ps t π u hok hemp h obtain ⟨_, _, _, _, h', hd⟩ := norm_all hok h exact Check.deep_empty hok h' hd (Le.refl _) hemp ```
That speed gap is the payoff of doing less: no unification, no metavariables, no tactic engine, one bidirectional pass with a usage counter per binder. The head-to-head numbers on the largest checker benchmark in the repo are stark: Isabelle and Agda are drawn at the 40s cap because both actually timed out past 300 seconds on this file — the chart understates the gap, not overstates it. All five numbers come from the same machine, the same file translated by hand into each system, in [`bench/checker/`](https://github.com/bendlang/bend/tree/main/bench/checker). Now the caveats, because a checker is exactly the kind of thing you don't want to take on faith. First: the Lean mechanization "does not yet fully match the shipped checker," in the paper's own words — `bend.lean` models the core with `+`, kinds, `Data` and the meet, `bend.ts` has grown past it, and the file itself lists where the two differ. The repo's limitations list is blunter: "The Lean formalization and bend.ts mismatch. Early consistency bugs may occur." The 21,000 lines of zero-`sorry` Lean proof are real, but they're a proof about a *model* of the calculus, not a certified compilation of the actual 3,734-line file that ships. Second: the checker is not the whole toolchain. `bend2/comp.ts`, the compiler that turns a checked program into C, Metal, CUDA or JavaScript, is 6,251 lines, and the README says outright: "the compiler (not kernel) is 99% AI-written and has not been fully audited yet." A law that machine-checks tells you the *source term* satisfies it. Whether the binary the compiler emits still does is a second question, answered so far by a checksum-matching test suite, not a proof. This is the honest shape of the trust story: a small, human-audited kernel checks your proof against your laws, and that part is real proof checking, done the way LCF-style provers have always done it — trust one small thing, not the whole program. But the kernel is one link in a chain (spec → proof → compiler → binary), and only one of those links is proven. The others are engineered, tested, and — for now — taken on faith. ## Claim two: "blocks AI mistakes" is exactly as strong as the law you wrote The workflow is `LAWS.bend` (a human, or an AI under a human's review, states the rules) and `PROOF.bend` (an AI fills them in; `bend PROOF.bend` either accepts the whole file or it doesn't). The README's demo is a tiny game with one rule — *winning is impossible* — stated as a law over every possible sequence of moves: ```python # LAW: for any sequence of moves, replaying them # from the start can never lead to victory. law you_cant_win: for moves: List board = Game.replay(Game.start(), moves) {Game.is_won(board) == False{} : Bool} ``` Ask an AI to "make the board wrap around" without the law in place, and — in Taelin's demo — the fix that ships lets the player wrap into the flag's room and win. With the law in place, the same request can't land until the AI also proves `you_cant_win` still holds for whatever it changed; if it can't, the change doesn't merge. That's a real difference from code review: a reviewer can miss a wraparound edge case, a checker cannot look the other way. The actual demo proof, for a 12×8 grid, runs to roughly 300 lines of hand-written induction — Bend has no tactics or proof search, so every case split, every use of an induction hypothesis, is written out by hand: ```python def go_ok(+a: Game.Move, +x: Nat, +y: Nat, +hp: T(okpos(x, y)), ca: T(chk_all(a, 11n)), e: {False{} == Game.wall(tx(a, x, y), ty(a, x, y)) : Bool}) -> T(okpos(tx(a, x, y), ty(a, x, y))): and_split(Game.nat_le(x, 11n) && Game.nat_le(y, 7n), Bool.not(room(x, y)) && Bool.not(Game.wall(x, y)), hp, T(okpos(tx(a, x, y), ty(a, x, y))), wb => wnr => /* ... */) ``` That verbosity is the actual cost of "no tactics": it's a deliberate tradeoff for a checker fast enough to outrun Lean by two orders of magnitude, and it means writing (or generating) a nontrivial proof is real work, not a one-line annotation. Here's the distinction the brief for this piece asked me to hold onto, and it matters more than the marketing copy suggests: **a law that machine-checks tells you the implementation matches the law. It says nothing about whether the law matches what you actually wanted.** "Winning is impossible" is easy to state and hard to get subtly wrong. "The sum of all balances must be zero" (the README's other example law) is easy to state and *easy* to get subtly wrong — a law that's too weak (doesn't rule out the bug you care about) or too strong (rules out legitimate behavior, so the AI "fixes" it by weakening the law instead of the code) both machine-check just fine. "Merging a bug is mathematically impossible: it is a theorem" is a true sentence about bugs that violate a stated law, and a non-sequitur about bugs that don't — a spec gap, a missing law, or a law that's vacuously true (checks a property that was never at risk) all produce the exact same green checkmark as a correct one. To be fair to Taelin's own phrasing: the README never actually claims the laws themselves are correct, only that the implementation matches them — "anything you can spell can become a law" puts the burden of spelling it right squarely back on the human. The risk is less in what's claimed than in how it reads at a skim: "make no mistakes becomes enforceable" is true of the mistakes you formalized, and silent about every other kind. ## Claim three: "the same technique big AI labs used… like Navier-Stokes" This one is worth being precise about, because it's doing real rhetorical work and it's easy to wave away too fast. Roughly two weeks before Bend 2 shipped, OpenAI announced that an unreleased model, run as roughly 10,000 autonomous agents over about 88 hours (several million dollars of compute, per researcher Sébastien Bubeck), found a finite-time singularity in the 3D Navier-Stokes equations — one of the six unsolved Millennium Prize Problems — and produced both an analytic writeup and a [Lean](https://lean-lang.org) formalization of it. About twelve hours earlier, NYU's Tristan Buckmaster and Anthropic's Levent Alpöge had independently reached a related result for the Euler equations, also Lean-checked; both efforts built on analytic groundwork from Diego Córdoba and Luis Martínez-Zoroa, who get first credit for the mathematics either way. [Quanta's writeup](https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-million-millennium-prize-problems-20260908/) is careful to note what "Lean-checked" buys here: mathematicians still have to verify that the Lean statement says what they think it says, but once it does, the proof itself is settled by a machine, not by trusting either the AI or the 10,000-way distributed process that produced it. That's the actual technique, and it *is* the one Bend's pitch is invoking: don't read the proof and decide whether to trust it, run it through a small kernel that either accepts or rejects it, no matter who or what wrote it — a lone AI, a swarm of 10,000, or a human. That idea transfers cleanly, and it's the same idea behind `LAWS.bend`/`PROOF.bend`. What doesn't transfer is the system. Lean is a mature, independently-developed proof assistant with roughly a decade of production use in mathematics, and it has no relationship to Bend, HVM, interaction nets, or GPUs — Bend's checker did not touch the Navier-Stokes proof, could not have, and Taelin's post doesn't claim otherwise. "The same technique" is an honest description of the *mechanism* (a checked proof, not a trusted author). "Like Navier-Stokes" borrows the prestige of a headline result Bend had no part in, to make an analogy about method read like a claim about lineage. Both things are true at once: the analogy is fair, and it is doing more marketing work than the literal words commit to. ## Claim four: fast, and on GPUs — but not the way its own history says ### The genuinely clever part Bend's speed claims have a real lineage: [HVM](https://github.com/HigherOrderCO/HVM2), Taelin's earlier runtime, evaluates **interaction combinators** — a graph-rewriting model from Lafont (1997) with a property that's rare enough to be worth explaining properly, because most engineers have never had a reason to meet it: *reduction order never changes the result, and never changes what's safe to run in parallel.* An interaction net is agents (drawn as triangles) connected by wires. Each agent has one **principal port** (the tip) and, here, two **auxiliary ports** (the base). Two agents whose principal ports point at each other form a **redex** — literally, two things ready to interact — and exactly one of two rules fires, decided purely by whether the two agents are the same kind: **Annihilate** (same agent meets same agent) is how beta-reduction and pattern matching happen: the two agents vanish and their four leaves rewire directly to each other, in place, touching nothing else in the net. **Commute** (a constructor meets a duplicator) is how a shared value gets copied *without* walking the whole structure up front: each agent clones the other, one node at a time, and the copies keep propagating outward on their own. The property that makes this parallel-safe for free is called **strong confluence**: firing any one redex can never disable or change the outcome of any other redex elsewhere in the net, because firing one only ever touches the two nodes at its own principal ports. A redex is a purely local fact — "these two ports point at each other" — so a scheduler doesn't have to decide *anything*: any number of workers can each grab a different ready pair from a shared bag, with nothing to lock and nothing to coordinate, and the net converges to the identical normal form regardless of who ran what when. That's "automatic parallelism" with the scare quotes earned rather than assumed — it's a real theorem about the rewrite system, not a benchmark trick. ### The part nobody put in the launch thread Here is the finding this piece turned up that the brief for it didn't anticipate: **Bend 2's shipped runtime does not use interaction nets.** BendRT — the paper describing the actual runtime, one directory over from BendTT — says so in its own words, in a sentence clearly aimed at exactly the audience who'd assume otherwise: > "Readers of the author's earlier runtimes may expect interaction nets here; there are none." And, in its related-work section, spelled out as a deliberate trade rather than a quiet regression: > "BendRT keeps the goals and drops the mechanism: affinity gives unique ownership directly, so the graph > and its duplication machinery become unnecessary. Lost is optimal reduction of shared redexes; gained are > native-speed sequential code, flat memory and a cost model a programmer can read." What replaced it: the checker already knows, statically, that every value has exactly one owner (that's what affine typing *is*), so BendRT doesn't need a graph of duplicator nodes to work sharing out at runtime — a whole-program analysis marks only the types that are actually shared as "hot" and reference-counts *those alone*; everything else compiles to plain stores, loads and frees, freed the instant a `match` consumes it. There's no garbage collector, because there's nothing to collect that ownership didn't already account for. Parallelism is explicit, not automatic — a `let` of the shape `a b = f(x) g(y)` tells the compiler these two calls may run concurrently, and a `!` suffix marks a call for the GPU: ```python # Computes 2^d in parallel: a tree of d levels, one leaf per unit. def pow2(+d: Nat) -> U32: match d: case 0n: 1 case 1n+p: a b = pow2(p) pow2(p) (a + b : U32) def main() -> IO(Unit): result = pow2!(20n) # runs on the GPU IO.print(U32.show(result)) ``` Those forked tasks land on a fixed 128×128 grid of rings — no work-stealing, no shared queue, no lock — that forks along rows and drains along columns. The price, stated as plainly as the gain: "the runtime trusts the equal-parts promise absolutely." A `let` fork that splits its work unevenly doesn't error; it just silently gives up the parallelism it was supposed to buy, and BendRT's own limitations section calls this out as unverified. So the honest one-line summary of claim four's first half is: Bend 2 traded HVM's "no annotation needed, ever" story for "two extra characters, and a contract the runtime doesn't check" — a real downgrade in the magic, and, on the evidence below, a real upgrade in speed and predictability. ### Why the old numbers deserved the skepticism, and what changed HVM2's own paper is unusually candid about where this leaves single-core performance: "In single-thread CPU evaluation, HVM2 is, baseline, still about 5x slower than GHC, and this number can grow to 100x on programs that involve loops and mutable arrays." Outside reviewers were harsher. On the original Bend 1 / HVM2 launch thread, one Hacker News commenter ([anon291](https://news.ycombinator.com/item?id=40390287)) put the scaling-vs-absolute problem in one line: "Going from 1 core to 16k cores increases performance by 50x. That's not actually very good" — because the thing being scaled from was already slow. Another ([Twirrim](https://news.ycombinator.com/item?id=40390287)) reported the single-threaded build of a recursive-sum benchmark running 42 minutes and 6GB of memory on their laptop without finishing, against a few seconds for PyPy. That's the exact failure mode this piece was asked to check for: a relative-speedup chart that can't show what it's scaling *from*. BendRT's own results table is the direct answer to that complaint — a hand-written **C twin** of every benchmark, run on the same machine, next to Bend at 1 thread, 16 threads and on the GPU:
The paper's headline claim from this table: single-thread Bend lands within 0.8–1.5x of hand-written C across its twelve benchmarks, sixteen threads give 8.8–12.1x over one, and uniform workloads (game of life, n-body, mandelbrot, merkle) hit 52–67x on the integrated GPU — while it says plainly that divergent workloads (n-queens, symbolic regression) *lose* to sixteen CPU threads, and that "the design stance is to report the loss rather than tune the scheduler toward it." That line — publishing the case where your own hardware target loses — is exactly the kind of receipt the "meaningless baseline" critics were asking for, and it wasn't in the earlier material. I pulled the fuller, more current pin — sixteen benchmarks as of this writing, four more than the paper's table, against C, TypeScript *and* Lean twins — and built both charts side by side, because the gap between them is the whole point: The extra four benchmarks are where it gets interesting. Three sit inside the paper's claimed 0.8–1.5x band (bfs 1.09x, edit-distance 1.28x, lexer sits a bit over at roughly 2x). The fourth, `hashmap`, doesn't: Bend's single core runs **4.4x slower** than its C twin there — the one case in the newer data that breaks the paper's own headline number, plausibly because a hash map is exactly the kind of pointer-chasing, heavily-shared structure that has to pay Bend's reference-counting cost on every access, where the tree-recursive numeric kernels in the paper's original twelve mostly don't. None of this reverses the finding. Bend 2 ships absolute numbers against three independent, competently optimized baselines, on real (if small) programs, on hardware anyone can rent, and most of them hold up the claim. It also has at least one benchmark, in its own public data, that doesn't — and the honest thing to do with a chart like the one above is use it to find that benchmark, not to stop looking once the first four look good. ``` - We don't have as many benchmarks as we'd like yet, especially for the checker. - The compiler (not kernel) is 99% AI-written and has not been fully audited yet. - The Lean formalization and bend.ts mismatch. Early consistency bugs may occur. - Parallelism requires balanced calls. Flexible parallelism will be added later. ```

— `bendlang/bend`'s own README, "Limitations"

## The take Unbundle the three claims and they land at three different heights. The proof checker is the real thing: a genuinely novel consistency argument (affinity instead of a universe hierarchy), a 3,734-line human-audited kernel that's smaller than the trusted core of the systems it's benchmarked against, and a Lean mechanization with no `sorry` in it — undercut, honestly, by that mechanization not yet matching the shipped checker, and by an AI-written, unaudited compiler sitting between a checked proof and the binary that runs. "Blocks AI mistakes" is true of exactly the mistakes you wrote a law against, which the project's own words don't quite overclaim but its tagline invites you to over-read. "The same technique big AI labs used… like Navier-Stokes" is an honest analogy about machine-checked trust wearing a technical-sounding hat it hasn't earned — Bend and Lean share an idea, not a lineage. And the performance story is the one that actually surprised me: the runtime that shipped is not the one the marketing's own history would lead you to expect, it's a real architectural bet against Taelin's earlier work, and — mostly, not universally — it backs that bet with exactly the kind of baseline the old benchmarks were missing. Taelin has been unusually direct that none of this is finished — Bend 2's own limitations file runs to thirty-some bullet points, ending with "and more that escape me," and the README says, in caps, "BEND IS YOUNG. EXPECT BUGS." Coming from someone shipping a launch video, that's a reasonable place to leave it too: a small trusted kernel behind a genuinely new consistency argument, a runtime that changed its mind and mostly has the numbers to justify it, and a marketing page one rhetorical flourish ahead of what's actually been shown. --- *Built from [bendlang/bend](https://github.com/bendlang/bend) and [HigherOrderCO/HVM2](https://github.com/HigherOrderCO/HVM2) at the commits current as of 2026-09-18, the BendTT and BendRT papers in `paper/`, `bend2/bend.lean`, and `bench/checker/` and `bench/runtime/` (pin of 2026-09-17, commit `d0db7b3e`, one Apple M4 Max). Navier-Stokes details from [OpenAI](https://openai.com/index/navier-stokes-solution/) and [Quanta Magazine](https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-million-millennium-prize-problems-20260908/). Historical criticism from Hacker News [discussion #40390287](https://news.ycombinator.com/item?id=40390287) and HVM2's own paper. Figures are reproduced from bend-lang.com's own benchmark charts.*