Bend Documentation

Technical Documentation: HigherOrderCO/Bend

ℹ️ Provenance: Multi-Tier Ingestion · CodeWiki Reference

Overview (README.md) Copy Section

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 Copy Chapter

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

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 Copy Chapter

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

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 Copy Chapter

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:

Bend BLOCKS mistakes - with proof Copy Chapter

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:

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. Rejoice as your app never again breaks or violates your rules.

You can also edit LAWS.bend yourself. Here's how it looks:

# LAWS.bend
law you_cant_win:                           # "winning is impossible"
  for moves: List<Game.Move>                # any sequence of moves
  board = Game.replay(Game.start(), moves)  # replayed from the start
  {Game.is_won(board) == False{} : Bool}    # never leads to victory

# PROOF.bend
def Laws.you_cant_win(moves):
  # ... written by the AI

In short, LAWS.bend is AGENTS.md backed by proof.

With LAWS.bend, "make no mistakes" becomes enforceable.

Skeptical? Edit the demo's code and break the "you can't win" law!

Get Started

1. Install: Copy Section

curl -fsSL https://bend-lang.com/install.sh | sh

This bend ignores a project's bunfig.toml and .env; bun bend2/main.ts
from a checkout reads them, so check untrusted code with bend.

2. Tell your agent to use Bend: Copy Section

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"!

3. Enjoy bug-free, fast vibe-coded apps! Copy Section

Hints:

• Ask it to write laws for anything that can't break.

• Ask it to parallelize anything you want to be fast.

• Bend is young. If anything goes wrong, ask it to open an issue. <3

Bend works best on the back-end, on Linux or macOS.

Examples

Syntax == Python + dependent types Copy Section

import Base

# Performs effects on the CPU.
def main() -> IO(Unit):
  do IO<Unit>:
    name : String <- IO.try(String, IO.get_env("USER"))
    IO.print("Hello, " ++ name)

Parallelism == divide-and-conquer Copy Section

import Base

# 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)

# Runs pow2 on the GPU, via `!`.
def main() -> IO(Unit):
  result = pow2!(20n)
  IO.print(U32.show(result))

Theorems == laws, Proofs == defs Copy Section

import Base

# CLAIM: for every nat x, x + 0 equals x.
law add_zero:
  for x: Nat
  {Nat.add(x, 0n) == x : Nat}

# PROOF: induction on `x`, one rewrite (`%`) per step.
def add_zero(x):
  match x:
    case 0n:
      {==}
    case 1n+xp:
      %add_zero(xp) : {1n+Nat.add(xp, 0n) == 1n+_ : Nat}
      {==}

References

• Guide: GUIDE.md, also printed by bend guide.
• Demos: demos/, apps, servers and proofs, each with its LAWS.bend.
• Base: base.bend, the base library, also printed by bend base.
• Paper: BendTT: An Affine Dependent Type Theory.
• Paper: BendRT: A Parallel Runtime for CPUs and GPUs.
• Formalization: bendtt.lean, the kernel of --verdict and its proofs, in Lean.
• Benches: bench/, every bench used to make the charts above.
• Formatter: bend-fmt-lsp, a formatting-only Bend 2 language server.
• Community language server: bend2-lsp, with formatting, diagnostics, and hover.
• Community workshop: Bend 2 pocket workshop, the checker and JS compiler in one HTML page, with goals and proof tools, phone first.

Community

• Website: https://bend-lang.com
• Discord: https://discord.bend-lang.com
• Twitter/X: https://x.com/bendlang
• Reddit: https://www.reddit.com/r/bendlang/
• Issues: https://github.com/bendlang/bend/issues

Limitations

/* Detailed source-code truncated for AI context efficiency. */

BEND IS YOUNG. EXPECT BUGS AND REPORT THEM.

Credits

Bend is created by Victor Taelin and built
by the team:

• Lorenzo W Battistela
• Paulo J Cavalcanti
• Nico Abril
• Vanessa Ostroski
• Vitor Chiarelli Neves
• Alex Van de Sande

If you were part of this and your name is missing, please get in touch so we
can add it here.

Thanks to Ayush Somani for reserving the
bend-lang name for us.

--- METRICS ---

• Files Extracted: 1
• Estimated Token Budget: ~2120 tokens
• Canonical Reference: https://codewiki.google/github.com/HigherOrderCO/Bend