StackMap
Subscribe
Explore / bend
bendlang

bend

Bend 2: a Python-like language with dependent types that compiles to fast CPU/GPU code; LAWS.bend declares invariants the compiler forces AI-written code to prove before it builds.

23,061 708 TypeScript Apache-2.0updated today
coding
View on GitHubDispute this mapping →
Curator's take

The most radical answer on the map to 'how do I trust code I did not read': write rules like 'balances sum to zero' in LAWS.bend, and the compiler rejects any agent edit it cannot prove keeps them, so the agent retries until it can. It is also built for speed, with implicit parallelism across CPU and GPU cores. The catch is total: it only protects code written in Bend, a young language (its README says so) that your agent learns via `bend guide`, best suited to back-end logic on Linux or macOS. Your existing TypeScript or Python gets nothing. For guarantees about a system you already run, specula's TLA+ model checking fits; for everyday agent code, tests and type checkers remain the pragmatic floor.

Mapped by ShipWithAI editors · links verified

Continue your stack

What teams reach for next — and why each earns a place beside bend. Ranked by curator confidence.

alternativeSpeculabend
pairs wellalternativebuilt withpick a node for the why · open it from the panel
Weekly digest
README.md2 min read

Bend: a fast language that blocks AI mistakes via proof

In the post-AGI economy, humans will eventually stop writing and reading code, but we still need an ambiguity-free language to communicate our intents to the AIs building the world around us. Bend is that language.

With laws, intents can be more precise than natural language. With proofs, we can mechanically verify the AI implemented our prompts correctly. And with a fast compiler, we can run that code at peak compute.

That's Bend - and nothing else.

Bend runs FAST

Target: be as fast as C on the CPU, as fast as CUDA on the GPU. Status:

Runtime benchmarks: Bend vs C, TypeScript, Lean, on 1 core, 16 cores and the GPU

Thanks to strong types, purity and linearity, Bend compiles to fast executables as fast as hand-written C (single-core), and even faster (on 10000s cores). The entire language runs on the GPU, with full memory unification.

Bend checks FAST

Target: outperform every proof assistant by several OOMs. Status:

Checker benchmarks: Bend vs Isabelle, Agda, Lean, Rocq

Bend's compiler is so powerful it can verify mathematical proofs. Usually, this is slow. Bend is not. It checks, in under a second, files that other projects would take minutes, making proofs way more practical.

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. Below, pow2(20) divides until one task sits on each of 4,096 GPU cores:

pow2 splitting over 4,096 GPU cores, then folding back

Bend BLOCKS mistakes - with proof

PROBLEM: How can you trust AI code, without reading it?

SOLUTION: By forcing your AI to write a correctness proof.

Bend introduces LAWS.bend, a file where you declare rules that your app must not break. Bend's compiler then guarantees that these laws always hold, by demanding mathematical proof whenever your code is edited. For example, consider a game with one law: winning is impossible. Here's how it plays out:

Law: winning is impossible
The player walks up and bumps the wall of the flag's room
So far, it works!

New feature: "Claude, make the board wrap around"

Without LAWS.bend:
The player wraps around the edge and takes the flag
Laws broken. AI mistake: merged.

With LAWS.bend:
A wall on the far edge stops the player
Laws intact. AI mistake: blocked!

Without LAWS.bend, a bug was merged. With it, the AI had to retry, until no bugs were left! In this case, it added a wall, but it could have moved the flag, made the room kill you, or whatever. The only thing it can't do is commit a bug, because it is mathematically impossible to break laws in LAWS.bend. The compiler enforces it.

Using LAWS.bend is simple.

  1. Ask your AI to formalize your app's rules in LAWS.bend. Example:

    • LAW: "the sum of all balances must be zero"

    • LAW: "players can never pass through solid walls"

    • LAW: "list_sort() must always return ascending numbers"

    • LAW: "array_set() may never be called out-of-bounds"

    • LAW: "winning is impossible" (the demo above!)

    • And so on. Anything you can spell can become a law.

  2. Ask your AI to run bend PROOF.bend after editing any code.

  3. That's it. R