⏱️ Lectura: 11 min
A new programming language called Bend promises to run almost as fast as C on a single core and scale up to 100 times faster using the same binary on GPU, according to its official site. But that’s not the most striking part.
📑 En este artículo
What’s striking is its compiler: it works as a proof prover, in the style of Lean or Rocq, capable of blocking any code change (even one written by an AI agent) if it breaks a rule you declared in advance in a file called LAWS.bend.
TL;DR
- Bend is a new language that compiles to native code and runs almost as fast as C on a single core.
- The same binary scales to 16 cores or GPU without changing the code, up to 100 times faster than a single core.
- Its type checker works as a proof prover in the style of Lean or Rocq and takes at most one second.
- LAWS.bend declares invariant rules; PROOF.bend certifies that the code meets them before merging.
- Installation is a single script: curl -fsSL https://bend-lang.com/install.sh | sh.
- The project recommends specific instructions in AGENTS.md so agents like Claude Code can use Bend on their own.
- Bend relies on two of its own papers: BendTT, an affine dependent type theory, and BendRT, its parallel runtime.
- Bend’s own site warns that the language is young and users should expect bugs of its own.
Introduction
The Bend language was born from an uncomfortable premise: if more and more code is written by AI, humans stop reading it line by line. The question Bend answers isn’t how to write better prompts, but how to trust code that no one reviewed by hand. Its answer is mathematical, not editorial: declare a law once and let the compiler enforce it forever.
This connects to a tension already being discussed across the industry: mass code generation by agents is growing faster than the capacity to review it. Bend doesn’t try to solve that problem with more human review, but with formal proofs that run on every build.
What happened with the Bend language
Bend introduces itself with a direct tagline: the speed of C, the parallelism of CUDA, the proofs of Lean, and the syntax of Python. Installation is a single script built for macOS and Linux:
# macOS / Linux
curl -fsSL https://bend-lang.com/install.sh | shOn Windows there’s no documented native installer: the practical route is to run it inside WSL2, since the project itself clarifies that Bend works better on Linux and macOS.
# Windows (via WSL2)
wsl --install
wsl -d Ubuntu -- bash -c "curl -fsSL https://bend-lang.com/install.sh | sh"⚠️ Heads up: before running anycurl | sh, it’s better to download the script and read it (curl -fsSL https://bend-lang.com/install.sh -o install.sh) instead of running it blindly, especially on machines with access to production credentials.
The second part of the announcement is aimed directly at coding agents: the project suggests pasting instructions into the AGENTS.md file that tools like Claude Code, Cursor, and Codex already read.
When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possibleWith that, according to Bend, it’s enough to tell the agent “use Bend” for the entire flow (reading the guide, respecting the laws, testing before committing) to be delegated.
Context and history
The idea of a compiler verifying mathematical properties of code isn’t new. Theorem provers like Lean and Rocq (the successor to the historic Coq) have been used for more than a decade to formalize mathematics and verify critical software. The seL4 microkernel is the most cited example of code with mathematical proofs of correctness running in production for years.
What changes with Bend is the audience. Lean and Rocq are designed for mathematicians and formal verification teams with dedicated budgets; their checks can take minutes on a mid-sized codebase. Bend targets a developer (or an AI agent) who needs an answer in seconds, within the same cycle where a linter or a unit test runs today.
Technical details and performance
Bend compiles to native code. On a single core, the project claims it runs close to the speed of C. The same binary, without recompiling or rewriting the code, can run on 16 cores or on GPU, with a gain of up to 100 times over a single core, according to the measurements published on its site for an Apple M4 Max.
A minimal example, just to see the syntax:
def main():
return "Hello from Bend"The interesting case isn’t this one, but how Bend parallelizes without threads or locks. If a function splits into two independent calls, the runtime distributes them on its own:
def suma_rango(lo, hi):
if hi - lo <= 1:
return lo
else:
medio = (lo + hi) / 2
(izquierda, derecha) = (suma_rango(lo, medio), suma_rango(medio, hi))
return izquierda + derechaThe two recursive calls of suma_rango don’t depend on each other, so BendRT (the parallel runtime described in the project’s paper) can dispatch them to different cores, or to different GPU threads, without the developer writing a single thread or lock.
| Execution mode | When to use it | Advantage | Limitation |
|---|---|---|---|
| Single core (CPU) | Prototyping and debugging | Predictable behavior, easy to reason about | Doesn’t take advantage of available parallelism |
| Multiple cores (CPU) | Medium workloads without a GPU on hand | Same binary, no code rewrite needed | The ceiling is set by the number of physical cores |
| GPU | Massively parallel workloads, like the project’s pow2.bend example | Up to 100 times faster than a single core, according to bend-lang.com | Requires the algorithm to be splittable into independent tasks |
The other technical pillar is type checking, which in Bend is, literally, a proof check. The project itself compares the operation to Lean and Rocq, but highlights the difference in timing: while those provers can take minutes on a mid-sized codebase, Bend takes at most one second, which lets an AI agent run it after every change.
💭 Key point: a proof in LAWS.bend doesn’t detect bugs in general: it only blocks violations of the specific law someone wrote. If no one declared the law, Bend won’t invent it.
The example the project itself uses to show this is a tic-tac-toe game with a law: you_cant_win, meaning that no sequence of moves leads to winning the game.
# LAW: no move sequence leads to victory.
law you_cant_win:
for moves: List<move> # any sequence of moves
board = replay(start(), moves) # the resulting board
is_won(board) == False # never leads to winning</move># PROOF: you_cant_win holds.
def Laws.you_cant_win(moves):
# ... proof written by the AIWhen the agent is asked to add a new function (making the board “wrap” at the edges), without LAWS.bend the bug goes straight to production. With LAWS.bend, the compiler rejects the change until the AI rebuilds the function and proves again that the law still holds.
flowchart TD
A["AI agent modifies the code"] --> B["bend PROOF.bend"]
B --> C{"Does the law in LAWS.bend hold?"}
C -->|"yes"| D["Merge allowed"]
C -->|"no"| E["Blocked: the AI must retry"]
E --> AHow to get started with the Bend language
To try it today, the flow the project itself describes has three steps. First, install:
curl -fsSL https://bend-lang.com/install.sh | shSecond, paste the instruction block into the repository’s AGENTS.md (the same file that Claude Code, Cursor, and Codex already read):
When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possibleThird, verify the installation is active by running the language’s full guide:
bend guideTo confirm that a law truly holds (and not just that Bend found nothing to prove), the most direct way is to check the exit code of the proof check:
bend PROOF.bend; echo $?A 0 means the proof passed; any other value means the compiler rejected the change because it breaks a law declared in LAWS.bend.
Impact and analysis
The use case generating the most enthusiasm is codebases maintained almost entirely by AI agents. If a team already delegates 80% of its commits to an assistant, according to figures Google, Anthropic, and OpenAI have been repeating this year, the question of who reviews that code becomes central. Bend proposes that the compiler do the reviewing, not a person reading a diff.
But there’s a real cost the project itself doesn’t hide: writing a law in LAWS.bend requires understanding, even superficially, the affine dependent type theory Bend is built on (described in the BendTT paper). Writing a unit test isn’t the same as formalizing an invariant. In practice, the one drafting the proof is usually the AI itself, which pushes the trust problem down one level: now you have to trust that the agent didn’t write an empty or trivially true proof just to pass the check.
Another honest limitation: the proofs only cover what someone thought to declare as a law. A performance bug, a style regression, or an edge case no one anticipated aren’t blocked by LAWS.bend simply because they were never written as a law. Bend doesn’t replace testing, it complements it for the subset of invariants a team decides to make non-negotiable.
What’s next
Bend’s own site is explicit: the language is young, users should expect bugs of its own in the compiler and runtime, and the request is that they be reported as issues. The core documentation lives in GUIDE.md, also accessible from the terminal with bend guide, and the theoretical foundation rests on two papers: BendTT, on the underlying type theory, and BendRT, on the parallel runtime for CPU and GPU.
The convention of instructions in AGENTS.md is, perhaps, the easiest thing to adopt today: it doesn’t depend on rewriting an entire project in Bend, just on deciding to declare a handful of critical invariants as laws (for example, that a billing function never overcharges) and letting the AI agent itself keep them maintained.
📖 Summary on Telegram: View summary
Try it yourself: run curl -fsSL https://bend-lang.com/install.sh | sh and follow up with bend guide to see the full syntax in minutes.
Frequently Asked Questions
What is the Bend language?
It’s a programming language with Python-like syntax, a native code compiler, and a type checker that works as a proof prover, designed so AI agents can write code without breaking declared invariants.
Do I need to write the proofs by hand?
Not necessarily. In the flow the project proposes, the AI writes both the code and the proof in PROOF.bend; the person only declares the law in LAWS.bend.
Does Bend run on Windows?
There’s no documented native installer for Windows. The practical alternative is to use WSL2, since the project clarifies that it works better on Linux and macOS.
What are BendTT and BendRT?
BendTT is the paper describing the affine dependent type theory that underpins Bend’s proof system. BendRT describes the parallel runtime that distributes computation between CPU and GPU.
Does Bend replace unit tests?
No. It only blocks violations of laws someone explicitly declared in LAWS.bend; any behavior not covered by a law still needs traditional tests.
Is Bend production-ready today?
The project’s own site asks users to expect bugs and report them as issues, and recommends using it mainly on the backend, on Linux and macOS.
References
- bend-lang.com: Bend’s official site, with the proposal, examples, and installation script.
- lean-lang.org: site of the Lean theorem prover, a direct reference Bend uses to explain its type checker.
- rocq-prover.org: site of Rocq (the successor to Coq), the other theorem prover Bend cites as a comparison.
- sel4.systems: a formally verified microkernel, a historical precedent for code with mathematical proofs of correctness in production.
📱 Enjoy this content? Follow @programacion on Telegram for daily tech content in Spanish: quick summaries, fresh content every day.
0 Comments