At 3 a.m., a coding agent finishes an eight-hour task. Tests are green, the diff is clean, CI smiles at you. But a team rule that was never written into tests—user balances must never go negative—got bypassed. Nobody lied, nobody was negligent, and the bad thing still happened.
On September 17, a Hacker News post with over 260 upvotes presented a remedy for exactly this scenario. The language is Bend, whose site tagline translates roughly as: *a fast language that blocks AI mistakes with proofs*. The author is Victor Taelin, a familiar figure in this space—his May 2024 "language that runs on GPUs" drew over a thousand upvotes on HN. This Bend 2 is a ground-up rewrite: the README states plainly that Bend 1 programs do not carry over, and the HVM runtime was rewritten too.
How It Works
Three files:
LAWS.bend— write your team's invariants, e.g., "no move may pass through a wall."PROOF.bend— the AI writes code *plus* a proof that it satisfies those laws.- Run the checker before merging; it renders a verdict in under a second. If the proof fails, the AI retries until the proof holds or it gives up.
Under the hood is BendTT, an affine dependent type theory. The type checker is a proof checker, in the same family as Lean and Rocq. Linear types ban runtime closures outright, and paradoxes that can blow up type systems (Russell's, Girard's) have no entry point at the language level. The cost is on the label: no tactics, no proof search, no type inference—all traded away for checking speed. Lean and Rocq core-check a proof in minutes; Bend does it in about a second. For humans that gap is trivia; for AI it is a workflow: every change can be re-verified on the spot, shifting verification from "grade after submission" to "judge while writing."
A single file is simultaneously a CPU program and a GPU kernel, compiled to C, then dispatched to Metal and CUDA via macros. Official figures: near-C single-core performance, GPU over 100x faster than a single core. Recursion must be bounded, programs must terminate, infinite paths must be closed by induction—and if you want to switch that protection off, there's a door: attach an explicit unsafe marker and sign for it yourself. The author's demo claim on HN was bolder still: with laws properly covering the domain, merging a bug is *mathematically impossible*.
The Fine Print
1. The demo itself showed cracks. Someone removed a wall in front of the checker—the AI turned a straight path into a diagonal, stepping over the removed wall in one move. The law was literally unviolated, but the intent had escaped. The original poster's line is worth quoting: writing the laws becomes a bigger problem than writing the code. Taelin's response was honest: laws only protect the parts you remember to write; this is not a silver bullet. He offered one serious use case—a single law like "the sum of all account balances is zero" would block The DAO-style reentrancy bugs.
2. Who audits the laws themselves? A commenter asked directly: if laws are also vibecoded, what happens when they're wrong? The author's one-word reply: "true." One practitioner ported a small tool with Claude Opus 5; it ran, but the standard library is painfully thin—of 163 lines of proofs, 60 were hand-rolled basic lemmas. On the author's wishlist: a mathlib.
3. The repo is a piece of performance art. The entire git history was squashed into one commit, signed Bend 2.0.5, with co-author listed as "Claude Fable 5.1." The stated reason: removing personal information, AI-generated residue, and a snippet of proprietary code. The community pushed back—force-pushing erases nothing; the history lives in forks and caches, and what was destroyed is trust itself. The author relented, saying a redacted history could be restored. Performance charts are all animated GIFs with no data tables, so the 100x speedup remains a slogan for now. The current-state list is almost excessively honest: no Windows, no 64-bit floats, strings are linked lists, no HTTP library, no JSON, no debugger, no LSP. The README also admits the compiler is 99% AI-written and has never been fully audited. The business model is clear: open-source compiler, paid "Bender" proof agent—already with a crowdfunding page.
Verdict
Layering the fine print back onto the main story: is this still worth watching? Yes. Once coding agents have solved about seventy percent of the productivity problem, the bottleneck is relocating—into "how to state intent precisely." AI can already write proofs, write code, even wrote this compiler itself. What remains for humans is deciding which rules deserve to become law. Machines can't do that for you, because at its core it answers: what do you actually want?
How many unwritten rules like "user balances must not go negative" are still lurking in your project?
---
Sources: bend-lang.com; github.com/bendlang/bend; the BendTT paper (repo paper directory); HN discussion 49746163 (2026-09-17).