Bend

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, where it runs a hundred times faster than one core.

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.

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:

4.Bend blocks mistakes via 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:

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 you_cant_win(moves):
  # ... written by the AI

LAWS.bend is AGENTS.md backed by proof. “Make no mistakes” is now type-checked.

Live demo: edit the source to win (you won't)

5.Get started.

5.1.Install

# needs Bun 1.3+ and clang; Metal or CUDA for the GPU
git clone https://github.com/HigherOrderCO/bend4
cd bend4
ln -s "$PWD/bend2/main.ts" ~/.bun/bin/bend

5.2.Write hello.bend

import Base

def main() -> IO(Unit):
  IO.print("Hello, world!")

5.3.Check, compile, run

bend hello.bend            # check
bend hello.bend -o hello   # compile
./hello                    # run (on GPU!)

Then read the guide. The core is formalized in Lean, and two papers describe it: BendTT, the type theory, and BendRT, the runtime. The compiler is young: expect bugs and report them.