Bend

~/bend
hubbenderget Bend

×
1.Install
curl -fsSL https://bend-lang.com/install.sh | sh
2.Add this to your AGENTS.md
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 possible
3.Enjoy bug-free, fast vibe-coded apps!

Bend
a fast language that blocks AI mistakes via proof
C speed · CUDA parallelism · Lean proofs

In the post-AGI economy, humans will eventually stop writing
and reading code, but we still need an ambiguity-free way to
tell the AIs building the world around us what we want done.
With laws, our intents can be much more precise than natural
language. With proofs, we can verify that the AI implemented
our prompts correctly. And a fast compiler runs it at speed.
That's Bend - and nothing else.

1.Bend runs FAST.
Bend compiles to native code. On one core, it runs nearly as
fast as C. The same binary also runs on sixteen cores, or on
the GPU, running up to a hundred times faster than one core.

Apple M4 Max · lower is better

2.Bend compiles FAST.
Bend's type checker is a proof checker, as in Lean and Rocq.
Those can take minutes on a mid-sized codebase. Bend takes a
second at most, so an AI agent can check after every change.

Apple M4 Max · lower is better

3.Bend is PARALLEL.
No threads, no locks, no kernels to write. Split the work in
two, and Bend spreads the calls over every core it can find,
then joins them back. Now watch pow2 run on 4,096 GPU cores:

pow2.bend running on the GPU

4.Bend BLOCKS mistakes - with proof
How can you trust code you never read? By demanding a proof.
LAWS.bend is where you declare laws. From then on, no AI can
ship one line that breaks them, ever. Watch it guard a game:

Law: winning is impossible

So far, it works!

New feature:
“Claude, make the board wrap around”

Without LAWS.bend:

Laws broken. AI mistake: merged.

With LAWS.bend:

Laws intact. AI mistake: blocked!

Without LAWS.bend, the bug went live. With LAWS.bend, the AI
had to retry until it built a wall and proved the law holds.
Merging a bug is mathematically impossible: it is a theorem.
LAWS.bend
# LAW: no move sequence leads to victory.
law you_cant_win:
for moves: List<Move> # any sequence of moves
board = replay(start(), moves) # replayed from the start
is_won(board) == False{} # never leads to victory
PROOF.bend
# PROOF: you_cant_win holds.
def Laws.you_cant_win(moves):
# ... written by the AI
LAWS.bend is AGENTS.md backed by proof.
“Make no mistakes” is now type-checked.
Skeptical? Try breaking the game.

5.Get started.
5.1.Install
curl -fsSL https://bend-lang.com/install.sh | sh
5.2.Tell your agent to use Bend
Add this to your AGENTS.md:
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 possible
Then, just say: "use Bend"!
5.3.Enjoy bug-free, fast vibe-coded apps!
Hints: ask it to write laws for whatever should never break,
and to parallelize everything you want running fast. Bend is
young: if anything goes wrong, ask it to open an issue. Bend
works best on the back-end, on Linux and on macOS. Enjoy! <3

6.References.
Guide: GUIDE.md is the whole language; bend guide prints it.
Paper: BendTT, an affine dependent type theory, Bend's core.
Paper: BendRT, a parallel runtime for CPUs and GPUs, the VM.
Bend is still evolving. Expect bugs, and please report them.

Bend is presented as a novel language designed to mitigate errors generated by artificial intelligence within the context of complex programming and system development, addressing the need for an unambiguous specification language in the post-AGI economy where human input must guide AI agents building the world. The core philosophy of Bend rests on the integration of formal laws, mathematical proofs, and high-speed execution to enforce correctness, speed, and parallelism simultaneously.

One of Bend's distinguishing features is its exceptional performance. Bend compiles directly to native code, enabling execution speeds comparable to C on a single core. Furthermore, the system is designed to leverage parallel architectures effectively; the same compiled binary can execute across sixteen cores or the GPU, potentially achieving speeds up to a hundred times faster than a single core. This speed is maintained even during compilation, as the time taken for the type checking process, which functions as a proof checker similar to systems like Lean or Rocq, is minimized to at most a second, allowing AI agents to verify code frequently with minimal latency after every modification.

The mechanism for error blocking is deeply embedded through the concept of laws. Bend introduces LAWS.bend, a system where developers can declare essential rules or constraints, such as asserting that a specific outcome is impossible. These laws are then used to mandate correctness. For instance, a law might state that winning is impossible. The system then utilizes PROOF.bend to formally verify that the AI-generated code adheres to these established laws. This process shifts the burden of error prevention from runtime debugging to compile-time mathematical proof, making it mathematically impossible for an AI agent to generate code that violates the declared constraints. This approach is demonstrated by preventing erroneous actions, such as merging a bug, because such an action would contradict the established laws, thereby forcing the AI to retry and prove adherence until the integrity of the law is maintained.

Bend also inherently supports parallelism. It achieves this by structuring computations to allow work to be naturally distributed across available processing units without the explicit need for complex thread management or locking mechanisms. The system allows tasks to be split and spread across all accessible cores, returning the results when complete, providing a natural path for highly parallel execution across CPUs and GPUs.

The overall usage involves establishing these constraints and directives through the language structure. Users are guided to utilize specific commands such as bend guide to learn the language structure, LAWS.bend to define rules, and PROOF.bend prior to committing code, along with enforcing parallelization whenever feasible. The ecosystem also includes foundational documents, such as GUIDE.md detailing the entirety of the language structure, and associated papers like BendTT, which defines the language's core as an affine dependent type theory, and BendRT, which describes the parallel runtime system for CPUs and GPUs. Bend is acknowledged as an evolving system, with the expectation that ongoing development will involve addressing emergent issues and reporting bugs.