Bend 2 · HVM · Interaction nets — the compendium

A.1 · bend-docs/src/content/tutorial/index.md

Bend 2 tutorial: table of contents · runnable · updated 2026-10-20 · canonical /tutorial/

Bend 2 tutorial

This tutorial teaches Bend 2 to someone who already knows Haskell or OCaml. It covers the syntax and the checker's rules, how values are owned and copied, the interaction-net model behind the language's history, parallel execution, and how to state and prove properties as laws.

It is unofficial and not affiliated with Higher Order Company. The reference is bend2.dev and the official guide, which bend guide prints from your installed compiler.

What you can do at the end

• Read a Bend 2 program, including its annotations, and predict whether the checker accepts it.
• State a law, prove it with a same-named def, and read the checker's messages when a proof fails.
• Say when a parallel call really runs in parallel, and how to measure it.
• Say what Bend 2 does not have (SupGen, sup syntax, copy-on-write forks of running code, homoiconic self-modification), and what to use instead.
• Open a real Bend repository, find its laws, entry point, tests, and effect boundary, and say what it proves and what it only measures.

Table of contents

Reading path

Read 01, 02, and 03 in order. They teach the language itself. Then read 07 and 08 (laws, proofs, dependent types), 05 (parallelism), and 09 (effects). Chapters 04 and 06 are the machine model and history: read them before 10, which applies everything to forking and testing branches. Keep 11 to 13 open as references, with 12 for every syntax form. Finish with 15, which combines the parts into one checked program. Then use 16 as a map of real repositories to read next.

How to read the boxes

Some sections set their key points apart in three kinds of box:

Core insight. The one idea that the next part depends on.

Definition. What a term means in this tutorial.

Composed of: a text block lists what a thing is made of. A - starts each part, a | between names means one of them, and indentation shows nesting. So CON | DUP | ERA reads as one of three cells.

Versions

• Checked with bend 2.0.25 on 2026-10-17. Run bend version to confirm yours.
• The examples on bend2.dev are pinned to 2.0.36 (commit ae1101c). 39 of its 42 examples print the documented output on 2.0.25. The other three print All terms check. where the site prints ALL PROOFS CHECK. 8 of 9 official diagnostics produce an error on 2.0.25, with the wording differences listed in chapter 11. The ninth uses f? names that 2.0.25 cannot parse.
• Version differences that change what you type are listed in chapter 11. The most important one: bend PROOF.bend --verdict does not exist in 2.0.25.

Honest limits

1. Bend 2 does not run on interaction nets. Chapter 04 explains the model behind the language's history. The released compiler emits a flat C evaluator called BendRT, which has no active pairs at runtime.
2. The released compiler has no SupGen, no sup syntax, and no homoiconic self-modification. Chapter 06 shows the evidence. &{1, 2} is a parse error, and nothing in bend base or bend guide describes SupGen.
3. "Cheap" and "fast" are measurements, not theorems. A law proves a property of the values a program computes. Cost, memory, and speed come from running the program and counting what the emitted C does.

How the examples are checked

Each ```bend block is a complete program. scripts/check-tutorial.py compiles and runs every one of them with the installed bend:

• a block followed by an ```output block must print exactly that text;
• a block followed by an ```error block must fail with those lines;
• a block followed by a ```contains block must print those lines;
• a block with no expectation must pass bend FILE --check-only.

ic and ic-collapse blocks run Victor Taelin's Interaction Calculus reference binary when IC_BIN points to it, and are reported as skipped otherwise. Fences marked text, sh, or bend-syntax are documentation and are not run.

python3 bend-docs/scripts/check-tutorial.py bend-docs/src/content/tutorial

A.2 · bend-docs/src/content/tutorial/01-first-programs.md

Bend 2 tutorial 01: first programs · runnable · updated 2026-10-18 · canonical /tutorial/01-first-programs/

01: first programs

Every program in this tutorial was checked with bend 2.0.25. Blocks marked output show what the compiler printed. Blocks marked error show the checker rejecting a program, and the lines are the real messages.

Install and check the toolchain

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

bend version prints the compiler version. bend guide prints the language reference that ships with the compiler, and bend base prints the standard library. Read the guide before you write Bend code: it is short and it is the authority.

bend update installs the latest compiler. The bend2.dev examples are checked against 2.0.36, which has the --verdict option. Version 2.0.25 does not have it, and chapter 07 explains what that option needs.

The four ways to run a file

Two options matter for the binaries: --threads N sets the number of CPU threads, and --gpu off runs ! calls on the CPU.

Hello, world

import Base

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

Hello, world!

• import Base loads the prelude. Every program in this tutorial starts with it.
• def main() -> IO(Unit): declares the entry point. IO(Unit) is an effect that returns Unit, the type with one value Unit{}. In Haskell, this is main :: IO ().
• do IO<Unit>: opens a block whose lines run in order, like Haskell's do.
• IO.print is an effect defined in Base.

Functions

import Base

def square(+x: U32) -> U32:
  (x * x : U32)

def main() -> U32:
  square(7)

49

• Parameter types follow :, and the result type follows ->.
• The last expression is the result. There is no return.
• Every operator needs an annotation, even on Nat: (n + 1n : Nat). One annotation can cover a whole expression of one type, as in (x * x * x : U32). A bare x * x is rejected, as the next example shows. The bundled guide (bend guide) still says a bare operator means Nat; the 2.0.25 checker rejects that. An annotation covers only the operators inside its own parentheses: in (U32.add(a + b, 1) : U32), the a + b needs its own annotation. Chapter 12 lists every rule of this kind.
• +x makes the parameter reusable, because x appears twice. Chapter 03 explains why plain parameters can be used only once.

import Base

def add(x: U32, y: U32) -> U32:
  x + y

def main() -> U32:
  add(40, 2)

- message  : a type for this operator (write (a + b : Nat))

In Haskell, square :: Word32 -> Word32 and square x = x * x would compile without any annotation. Bend asks for the annotation because it does almost no type inference, and that keeps its error messages precise.

Reading :, ->, and =

Three marks do most of the work:

• name: Type says has type. It appears in parameters, constructor fields, and for binders.
• (expr : Type) annotates an expression, and {term : Type} annotates one term, as in {12 : U32}. Bend does almost no inference, so you write the type where the checker needs it.
• A : at the end of a line opens a block: a body, a case, a do, or a law.
• -> separates the parameters from the result type. = binds a value. A : never means "equals".

A signature reads from left to right:

import Base

def greet(name: String) -> IO(String):
  do IO<String>:
    return "Hello, " ++ name

• name: String gives the parameter name its type.
• -> IO(String) gives the result: an effect that returns a String.
• The final : opens the body. The do IO<String>: header is a separate form, with angle brackets. Chapter 12 lists the rules for both.

Let bindings

import Base

def main() -> U32:
  +price = {12 : U32}
  tax = {3 : U32}
  (price + price + tax : U32)

27

• tax = {3 : U32} binds a value used once.
• +price = {12 : U32} binds a value that the body uses twice.
• Inside a do block, a let needs its type, as in n : U32 = (6 * 7 : U32). Chapter 09 covers do.

Why a let needs a type

A let has no type to take from, and Bend does no inference, so a bare literal is rejected:

import Base

def main() -> U32:
  +price = 12
  (price + price : U32)

- expected : an annotated term (cannot infer)

The fix is an annotation, {12 : U32}. That is not a constructor: a constructor has a name in front of its braces, as in Tok{3n} (chapter 02). Braces with no name hold one term and its type.

Braces or parentheses

Braces annotate one term, such as {12 : U32} or {x : U32}. An operator needs parentheses, so that the annotation covers it:

import Base

def main() -> U32:
  {6 * 7 : U32}

- message  : a type for this operator (write (a * b : Nat))

Write (6 * 7 : U32) instead. The parentheses only group and annotate. They do not delay the work: Bend is strict, so the term runs when its definition runs (chapter 12, section 11).

Conditionals: match, not if

Bend has no if. You branch with match on True{} and False{}, and the scrutinee must be a parameter, not a computed call:

import Base

def choose(test: Bool, yes: U32, no: U32) -> U32:
  match test:
    case True{}:
      yes
    case False{}:
      no

def main() -> U32:
  choose(U32.is_lt(3, 5), 10, 20)

10

The computed comparison U32.is_lt(3, 5) is passed to choose, and choose matches its own parameter. Matching the call directly is rejected:

import Base

def main() -> U32:
  match U32.is_eq(1, 1):
    case True{}:
      1
    case False{}:
      0

- message  : a parameter or field scrutinee (a match cannot scrutinize a computed value: give it its own def)

Numbers

Bend has three numeric types. Nat is an unbounded natural, written with an n suffix (3n). U32 is a 32-bit unsigned integer, and its arithmetic wraps. F32 is a 32-bit float. This chapter uses Nat and U32.

import Base

def main() -> String:
  n = Nat.add(20n, 22n)
  w = (6 * 7 : U32)
  Nat.show(n) ++ " / " ++ U32.show(w)

"42 / 42"

Nat patterns use 0n and 1n+p, where p is the predecessor (chapter 02). U32 wraps at 2^32:

import Base

def main() -> U32:
  (4294967295 + 1 : U32)

0

F32 values print as written in a checked program (1.5). F32 arithmetic, however, is declared in Base as a law, so the checker shows F32.mul(1.5, 2.0) as an unevaluated term. A native build computes it, and IO.print(F32.show(F32.mul(1.5, 2.0))) prints 3.

Strings, tuples, and lists

Strings join with ++. String.length returns a Nat:

import Base

def main() -> IO(Unit):
  text = String.to_upper("bend")
  IO.print(text ++ " " ++ Nat.show(String.length("proof")))

BEND 5

A pair has type A & B and value (a, b):

import Base

def sum(pair: U32 & U32) -> U32:
  match pair:
    case (a, b):
      (a + b : U32)

def main() -> U32:
  sum((19, 23))

42

A list is Nil{} or Con{head, tail}, and [5, 10, 15] builds one:

import Base

def sum(xs: List<U32>) -> U32:
  match xs:
    case Nil{}:
      0
    case Con{head, tail}:
      (head + sum(tail) : U32)

def main() -> U32:
  sum([5, 10, 15])

30

The list in that example is consumed as the function walks it. Chapter 03 explains which lists can be reused and how List<&2, U32> changes that.

Exercises

1. Double and add. Write double_plus so that it returns 2a + b. The parameter a is used twice, so it needs +. Then main should print 25.

import Base

def double_plus(+a: U32, b: U32) -> U32:
  (a + a + b : U32)

def main() -> U32:
  double_plus(10, 5)

25

2. A label from a comparison. Write label(n) that returns "small" when n < 10 and "big" otherwise. Remember that match cannot inspect U32.is_lt(n, 10) directly, so pass it to a helper.

import Base

def pick(test: Bool) -> String:
  match test:
    case True{}:
      "small"
    case False{}:
      "big"

def label(n: U32) -> String:
  pick(U32.is_lt(n, 10))

def main() -> String:
  label(42)

"big"

Next

Chapter 02 covers data types, records, recursion and its termination rule, nested patterns, imports, and definition order.

A.3 · bend-docs/src/content/tutorial/02-data-and-recursion.md

Bend 2 tutorial 02: data and recursion · runnable · updated 2026-10-18 · canonical /tutorial/02-data-and-recursion/

02: data and recursion

This chapter covers the data types you define, how a match reads them, and the rule that makes recursion safe to check. Haskell and OCaml readers will recognize almost everything. The differences are the explicit annotations and the fixed order of definitions.

Algebraic data types

import Base

type Shape is Data:
  Point{}
  Segment{length: Nat}

def measure(shape: Shape) -> Nat:
  match shape:
    case Point{}:
      0n
    case Segment{length}:
      length

def main() -> Nat:
  measure(Segment{3n})

3n

• type Shape is Data: declares a type and says its values may be reused (chapter 03). Each indented line is a constructor.
• Constructors always use braces, even without fields: Point{}.
• Fields are named inside the braces: Segment{length: Nat} builds Segment{3n}.
• Haskell's data Shape = Point | Segment { length :: Nat } is the same declaration.

Types, constructors, and values

A type is a set of values: Shape. A constructor (often shortened to ctor) is a named way to build one of those values: Point{} and Segment{length: Nat} are the two constructors declared in type Shape. In Haskell, data Shape = Point | Segment Nat declares the same two constructors. A value is what a constructor builds: Point{} and Segment{3n} are both values of type Shape.

A name followed by braces, K{...}, is always a constructor. The braces do different jobs depending on where they appear:

• In a type declaration, Segment{length: Nat} lists the fields of the constructor.
• In an expression, Tok{3n} applies the constructor to 3n. The compiler reads it as Ctor(Tok, [3n]).
• In a match pattern, case Segment{length}: takes the value apart and binds the field.

Braces without a name are a different form. {12 : U32} is an annotation, Ann(12, U32), and it is not a constructor. Chapter 12 lists every use of braces.

import Base

type Shape is Data:
  Point{}
  Segment{length: Nat}

def main() -> Shape & Shape:
  (Point{}, Segment{3n})

(Point{}, Segment{3n})

Both values are built directly, and no match is needed to make them. Point{} takes no fields, and Segment{3n} takes one.

Base declares its own types the same way. bend base --types prints them:

Angle brackets name types. Maybe<&2, U32> is a type, and Some{42} is a value of that type. In Haskell, Maybe a is a type constructor and Just x is a data constructor. Bend keeps the two apart the same way.

A constructor needs its type from context. When a let has no context, write the type:

import Base

type Tok is Data:
  Tok{n: Nat}

def show(t: Tok) -> Nat:
  match t:
    case Tok{n}:
      n

def main() -> Nat:
  t : Tok = Tok{3n}
  show(t)

3n

Records

A record is a type with one constructor:

import Base

type Point is Data:
  Point{x: U32, y: U32}

def translate(p: Point) -> Point:
  match p:
    case Point{x, y}:
      Point{(x + 1 : U32), (y + 2 : U32)}

def main() -> Point:
  translate(Point{3, 4})

Point{4, 6}

match consumes p and binds its fields. The result is a new Point. Nothing is mutated.

Recursion and the termination rule

Bend repeats work by recursion, and every recursive call must be checked to terminate. The rule: a recursive call reads its arguments from left to right, and each argument must be passed unchanged until one of them is a smaller part of its parameter. Put the argument that shrinks first.

import Base

def sum(xs: List<U32>, acc: U32) -> U32:
  match xs:
    case Nil{}:
      acc
    case Con{head, tail}:
      sum(tail, (acc + head : U32))

def main() -> U32:
  sum([1, 2, 3, 4], 0)

10

tail is a smaller part of xs, which the match exposed, and xs is the first argument. The accumulator changes freely because it comes after the shrinking argument.

Counting with a machine integer does not work, because subtraction gives the checker no structural evidence. Count with a Nat and match its predecessor. The parameter often called fuel bounds a loop that the outside world decides when to stop:

import Base

def count_down(fuel: Nat, acc: U32) -> U32:
  match fuel:
    case 0n:
      acc
    case 1n+remaining:
      count_down(remaining, (acc + 1 : U32))

def main() -> U32:
  count_down(5n, 0)

5

A recursive call that passes its input unchanged is rejected:

import Base

def loop(n: Nat) -> Nat:
  loop(n)

def main() -> Nat:
  loop(1n)

- expected : a decreasing self-call

Mutual recursion is not allowed in a safe definition. Merge the two functions into one, with an extra argument that selects which branch to run. Chapter 11 covers the @unsafe escape hatch and why a law must never depend on it.

Matching in depth

Patterns nest. This one inspects the second element of a list:

import Base

def second(xs: List<U32>) -> U32:
  match xs:
    case Nil{}:
      0
    case Con{h, Con{k, rest}}:
      k
    case Con{h, Nil{}}:
      h

def main() -> U32:
  second([4, 9, 7])

9

match can take several scrutinees, and _ matches anything:

import Base

def both(a: Nat, b: Nat) -> Nat:
  match a b:
    case 0n 0n:
      0n
    case 0n 1n+q:
      1n+q
    case 1n+p 0n:
      1n+p
    case 1n+p 1n+q:
      Nat.add(p, q)

def first_or_zero(a: Nat, b: Nat) -> Nat:
  match a b:
    case 0n _:
      0n
    case 1n+p _:
      1n+p

def main() -> Nat & Nat:
  (both(3n, 4n), first_or_zero(5n, 7n))

(5n, 5n)

Three rules govern every match:

1. The scrutinee is a parameter or a variable bound by an earlier pattern. match U32.is_eq(1, 1): is rejected (chapter 01).
2. Matches are exhaustive. This one omits False{}:

import Base

def pick(b: Bool) -> U32:
  match b:
    case True{}:
      1

- expected : cases for False

3. Scrutinees follow binder order. A let cannot come before a match on a parameter.

Absence without null: Maybe

Bend has no null. A value that may be missing has type Maybe<&2, A>: None{} means no value, and Some{x} wraps one.

import Base

def add_strings(a: String, b: String) -> Maybe<&2, U32>:
  do Maybe<&2, U32>:
    x : U32 <- U32.read(a)
    y : U32 <- U32.read(b)
    return (x + y : U32)

def main() -> Maybe<&2, U32>:
  add_strings("40", "2")

Some{42}

Inside do Maybe<&2, U32>:, the first None ends the block with None, as the guide describes. Maybe.default turns the result back into a plain value:

import Base

def add_strings(a: String, b: String) -> Maybe<&2, U32>:
  do Maybe<&2, U32>:
    x : U32 <- U32.read(a)
    y : U32 <- U32.read(b)
    return (x + y : U32)

def main() -> U32:
  Maybe.default(&2, U32, add_strings("40", "oops"), 0)

0

A division that refuses to divide by zero uses the helper pattern from chapter 01: the helper matches its own parameter. b is marked + because the function uses it twice:

import Base

def pick_div(zero: Bool, a: Nat, b: Nat) -> Maybe<&2, Nat>:
  match zero:
    case True{}:
      None{}
    case False{}:
      Some{Nat.div(a, b)}

def safe_div(a: Nat, +b: Nat) -> Maybe<&2, Nat>:
  pick_div(Nat.is_eq(b, 0n), a, b)

def main() -> Maybe<&2, Nat>:
  safe_div(10n, 3n)

Some{3n}

Imports and modules

An import gives a file a name. The alias is local to the importing file:

numbers.bend

import Base

def three() -> Nat:
  3n

main.bend

import Base
import ./numbers.bend as Numbers

def main() -> Nat:
  Numbers.three()

3n

import Base needs no alias. Imports come before definitions in a file.

Definition order

Bend checks each definition against the definitions above it. Calling a function written below it is an error:

import Base

def main() -> U32:
  answer()

def answer() -> U32:
  42

- expected : a defined name

Move answer above main and the program checks. Datatypes follow a related rule. In bend 2.0.25, a constructor field may only name a type that is already defined above it:

import Base

type Outer is Data:
  Wrap{inner: Inner}

type Inner is Data:
  Leaf{n: Nat}

def main() -> Nat:
  0n

- expected : a defined name

The bend2.dev guide says datatypes may appear in any order. The compiler we checked does not allow it, so define the inner type first.

Exercises

1. Length of a list. Write length(xs) that returns the number of elements as a Nat. The head is not needed, and an unused binder is dropped without any annotation.

import Base

def length(xs: List<U32>) -> Nat:
  match xs:
    case Nil{}:
      0n
    case Con{head, tail}:
      1n+length(tail)

def main() -> Nat:
  length([1, 2, 3, 4])

4n

2. Largest element. Write max_of(xs, best) that folds a list and keeps the larger of each element and the running best. Use U32.max, which is in Base.

import Base

def max_of(xs: List<U32>, best: U32) -> U32:
  match xs:
    case Nil{}:
      best
    case Con{head, tail}:
      max_of(tail, U32.max(head, best))

def main() -> U32:
  max_of([3, 9, 4], 0)

9

Next

Chapter 03 explains why a plain binder can be used only once, and what + costs.

A.4 · bend-docs/src/content/tutorial/03-ownership-and-copying.md

Bend 2 tutorial 03: ownership and copying · runnable · updated 2026-10-18 · canonical /tutorial/03-ownership-and-copying/

03: ownership and copying

Haskell shares values by default, and a garbage collector frees them later. Bend does the opposite: every binder says how many times it may be used, and the checker enforces it. This chapter explains those quantities, the cost of each way to copy, and the containers that rely on them.

Affine by default

A plain binder may be used at most once. Dropping it is free:

import Base

def twice(n: Nat) -> Nat:
  Nat.add(n, n)

def main() -> Nat:
  twice(3n)

- expected : n
- observed : n (consumed more than once)

The fix is +, which marks the binder as reusable:

import Base

def twice(+n: Nat) -> Nat:
  Nat.add(n, n)

def main() -> Nat:
  twice(3n)

6n

+ is allowed only when the binder's type is Data. Nat, U32, Bool, and records declared is Data qualify. Functions, arrays, and file handles never do.

Data versus Type

A type declared is Data may be copied with +. A type declared is Type may not:

import Base

type Token is Type:
  Tok{n: Nat}

def show(t: Token) -> Nat:
  match t:
    case Tok{n}:
      n

def main() -> Nat:
  t : Token = Tok{3n}
  +u = t
  show(u)

- expected : Data
- observed : Type

The same program works when Token is declared is Data, and it uses an annotation to build the value:

import Base

type Tok is Data:
  Tok{n: Nat}

def show(t: Tok) -> Nat:
  match t:
    case Tok{n}:
      n

def main() -> Nat:
  +t = {Tok{3n} : Tok}
  Nat.add(show(t), show(t))

6n

Think of a kind as a reuse budget. Type allows one use, and Data allows as many copies as the code asks for, marked with +. A type with arguments takes its kind from them, so Maybe<&2, Nat> is Data and Maybe<&1, Nat> is Type:

import Base

def dup(+m: Maybe<&2, Nat>) -> Maybe<&2, Nat> & Maybe<&2, Nat>:
  (m, m)

def main() -> Maybe<&2, Nat> & Maybe<&2, Nat>:
  dup(Some{4n})

(Some{4n}, Some{4n})

With &1, the same +m is rejected:

import Base

def dup(+m: Maybe<&1, Nat>) -> Maybe<&1, Nat> & Maybe<&1, Nat>:
  (m, m)

def main() -> Maybe<&1, Nat> & Maybe<&1, Nat>:
  dup(Some{4n})

- expected : Data
- observed : Type

The minus sign: erased parameters

-A is a parameter that exists only at compile time. It appears in types and is deleted before the program runs. keep_first below ignores its second argument, which is dropped:

import Base

def twice(+n: Nat) -> Nat:
  Nat.add(n, n)

def keep_first(-A: Type, x: A, y: A) -> A:
  x

def main() -> Nat:
  keep_first(Nat, twice(3n), 9n)

6n

Why mark a parameter erased

Without the minus sign, A is an ordinary parameter. The checker accepts both versions, but the compiled programs differ: the plain version receives the type as a value and drops it at the end. Write the program twice, once with -A and once with A, and compare the C each one emits (chapter 05 shows -o file.c):

bend erased.bend -o erased.c
bend plain.bend -o plain.c
grep -c _A_0 erased.c plain.c

erased.c:0
plain.c:2

The erased version has no variable for A. The plain version has one, _A_0, which it receives and then drops. The minus sign removes that cost.

What a run-time use is

A binder is used at run time when the compiled body needs its value: it returns the value or computes with it. An erased binder cannot be used that way, because its only uses are in types and proofs:

import Base

def bad(-A: Type, x: A) -> A:
  A

def main() -> Nat:
  bad(Nat, 6n)

- expected : A
- observed : Type

Type arguments are explicit

Bend infers almost nothing, so a type argument is passed like any other argument. Leaving it out is rejected:

import Base

def identity(-A: Type, x: A) -> A:
  x

def main() -> U32:
  identity(42)

- expected : Type
- observed : U32

With the type passed, the call checks. The type is erased, so it costs nothing at run time:

import Base

def identity(-A: Type, x: A) -> A:
  x

def main() -> U32:
  identity(U32, 42)

42

Kinds: how often a value may be used

Every type has a kind that caps its uses. Type is Kind(&1) (affine) and Data is Kind(&2) (reusable). Base declares List<a, A> so that a list is exactly as reusable as its elements. A function can take the kind as an argument:

import Base

def count(a, -A: Kind(a), xs: List<a, A>) -> Nat:
  match xs:
    case Nil{}:
      0n
    case Con{head, tail}:
      1n+count(a, A, tail)

def main() -> Nat:
  count(&2, U32, [10, 20, 30])

3n

A parameter of type +List<U32> is a list whose elements are reusable. The type is List<&2, U32>, so the + on the parameter lets the function use the whole list twice:

import Base

def twice_len(+xs: +List<U32>) -> Nat:
  Nat.add(List.length(&2, U32, xs), List.length(&2, U32, xs))

def main() -> Nat:
  twice_len([1, 2, 3])

6n

Arrays: one owner, updated in place

An array has exactly one owner. Writing to it changes the storage in place, and the array comes back to you. [0 : U32*8n] creates eight slots (the count must be a power of two). A read returns the array together with the element:

import Base

def value(result: Array<U32> & U32) -> U32:
  match result:
    case (array, item):
      item

def main() -> U32:
  a = [0 : U32*8n]
  a[5] <- 42
  value(a[5])

42

The bracket form is an array literal, and its type part says what the slots hold. [fill : Type*slots] asks for slots slots, which must be a power of two. [fill : Type^depth] names a depth, so U32^3n is 2^3 = 8 slots. The function form is Array.new(-T: Data, +d: Nat, +v: T) -> Array<T> in Base. Array.new(U32, 3n, 0) builds the same array as [0 : U32^3n], because its second argument is the depth. Indexes wrap, so on an eight-slot array a[9] is slot 1. A slot count that is not a power of two is rejected:

import Base

def main() -> U32:
  a = [0 : U32*6n]
  a[5] <- 42
  0

- message  : a power of two count (^d takes a depth)

An array passed to a function is updated there and returned. Put the write in a def that takes the array as a parameter:

import Base

def first_of(r: Array<U32> & U32) -> U32:
  match r:
    case (arr, item):
      item

def set_first(a: Array<U32>) -> Array<U32>:
  a[0] <- 7
  a

def main() -> U32:
  a = [1 : U32*4n]
  b = set_first(a)
  first_of(b[0])

7

A second independent array needs Array.clone, which copies every slot. Its result is a pair, and the pair cannot be destructured in main: a match may not inspect a computed value. Pass it to a helper that matches its parameter:

import Base

def first_of(r: Array<U32> & U32) -> U32:
  match r:
    case (arr, item):
      item

def set_first(a: Array<U32>) -> Array<U32>:
  a[0] <- 7
  a

def use_clone(p: Array<U32> & Array<U32>) -> U32:
  match p:
    case (a1, a2):
      b = set_first(a1)
      x = first_of(b[0])
      y = first_of(a2[0])
      (x + y : U32)

def main() -> U32:
  a = [1 : U32*4n]
  use_clone(Array.clone(U32, a))

8

Here x is 7 and y is 1, so the copies stayed independent. Destructuring the result in main is rejected:

import Base

def main() -> U32:
  a = [1 : U32*4n]
  (a1, a2) = Array.clone(U32, a)
  first_of(a1[0])

def first_of(r: Array<U32> & U32) -> U32:
  match r:
    case (arr, item):
      item

- message  : a parameter or field scrutinee (a match cannot scrutinize a computed value: give it its own def)

Maps

A Map associates string keys with values. Map.new takes the kind and the value type. Map.set and Map.get return the map with their result, so the map keeps its owner. Map.get takes its default before the map:

import Base

def value(result: Map<&2, U32> & U32) -> U32:
  match result:
    case (map, item):
      item

def main() -> U32:
  m = Map.new(&2, U32)
  m = Map.set(&2, U32, m, "answer", 42)
  value(Map.get(U32, 0, m, "answer"))

42

A Set is a map with no values. Set.add returns the set, and Set.size counts its keys:

import Base

def main() -> Nat:
  s = Set.new()
  s = Set.add(s, "x")
  s = Set.add(s, "y")
  Set.size(s)

2n

Templates: compile-time arguments

A template parameter starts with ~. Its argument is substituted at compile time and is not passed at run time. Each distinct template argument produces its own compiled copy, so a template may be called as often as you like:

import Base

def twice(~f: U32 -> U32, x: U32) -> U32:
  f(f(x))

def main() -> U32:
  twice(~(x => (x + 1 : U32)), 40)

42

A template may call itself and pass its template argument along. Two different steps give two compiled copies of the same loop:

import Base

def run(~step: U32 -> U32, n: Nat, x: U32) -> U32:
  match n:
    case 0n:
      x
    case 1n+p:
      run(~step, p, step(x))

def main() -> U32 & U32:
  (run(~(x => (x + 1 : U32)), 3n, 0), run(~(x => (x + 2 : U32)), 3n, 0))

(3, 6)

A template argument must be closed: it may mention top-level definitions, but not a local variable of the caller. Here k is a local variable, and the checker rejects the call:

import Base

def twice(~f: U32 -> U32, x: U32) -> U32:
  f(f(x))

def add_k(k: U32, x: U32) -> U32:
  twice(~(y => (y + k : U32)), x)

def main() -> U32:
  add_k(1, 40)

- expected : a template applied to closed ~ arguments (k is a variable here, not comptime: pass it at run time)
- observed : twice

Why a template, not a closure

A parameter of type U32 -> U32 is a closure, and a closure is affine. f(f(x)) uses f twice, so the checker rejects this program:

import Base

def apply_twice(f: U32 -> U32, x: U32) -> U32:
  f(f(x))

def main() -> U32:
  apply_twice(x => (x + 1 : U32), 40)

- expected : f
- observed : f (consumed more than once)

A ~f argument is substituted at compile time, so f is code rather than a value that can be used up. The twice above is that fix.

Closures

A function may return a closure that captures a value. A closure is affine: it may be called once, even when everything it captures is Data:

import Base

def offset(k: U32) -> U32 -> U32:
  x => (x + k : U32)

def main() -> U32:
  add2 = offset(2)
  add5 = offset(5)
  add5(add2(35))

42

A top-level definition may be called many times. Use a template when you need a function called repeatedly.

Folds

List.foldl reduces a list. Its signature takes the quantity of the elements, their kind, the accumulator type, and the combining function as template arguments, then the list and the starting value. Here add is a top-level definition, so it costs nothing to pass:

import Base

def add(a: U32, b: U32) -> U32:
  (a + b : U32)

def main() -> U32:
  List.foldl(~&1, ~U32, ~U32, ~add, [10, 20, 12], 0)

42

List.filter and List.sort take the element type and a function as template arguments, and they return List<&2, A>, the reusable form. This filter keeps the elements greater than 5:

import Base

def is_big(x: U32) -> Bool:
  U32.is_gt(x, 5)

def main() -> List<&2, U32>:
  List.filter(~U32, ~is_big, [1, 6, 3, 8])

[6, 8]

What a copy costs

The guide says + pays a reference count. The emitted C keeps that count in 24 bits (RFC_CNT). Chapter 05 shows how to find the counts. Chapter 10 explains why none of this gives you copy-on-write forks of running code.

Exercises

1. Cube. The parameter appears three times in x * x * x. Add the qualifier that makes it reusable, then check that cube(3) prints 27.

import Base

def cube(+x: U32) -> U32:
  (x * x * x : U32)

def main() -> U32:
  cube(3)

27

2. Keep the original. Clone the array, change the first slot of one copy to 7, and return the first slot of the other copy. The answer is 1.

import Base

def first_of(r: Array<U32> & U32) -> U32:
  match r:
    case (arr, item):
      item

def set_first(a: Array<U32>) -> Array<U32>:
  a[0] <- 7
  a

def other_copy(p: Array<U32> & Array<U32>) -> U32:
  match p:
    case (a1, a2):
      b = set_first(a1)
      first_of(a2[0])

def main() -> U32:
  a = [1 : U32*4n]
  other_copy(Array.clone(U32, a))

1

Next

Chapter 04 is the machine model: interaction nets, the rules that rewrite them, and why the model is the reason copying is explicit in Bend.

A.5 · bend-docs/src/content/tutorial/04-interaction-nets.md

Bend 2 tutorial 04: interaction nets · docs-only · updated 2026-10-18 · canonical /tutorial/04-interaction-nets/

04: interaction nets

This chapter is about a computation model, not a Bend program. You will not run any code here. Its purpose is to explain three words you will see in Bend's documentation, active pair, confluence, and duplication, and why the designers started from this model.

Status: docs-only. The examples are pen-and-paper exercises. Chapter 05 shows what the released compiler does.

The problem: copying is the whole game

Lambda calculus has one operation that does the work: β-reduction, which substitutes an argument into a function body. A variable used twice in the body forces you to copy the argument, and if the argument is itself an expensive computation, the copy repeats the work. Tree-shaped rewriting has no way to share that work.

Interaction nets solve this by representing a term as a graph. A shared piece of the graph is one node with several wires leaving it, so it is computed once. The price is that copying becomes an explicit operation with its own rules.

Cells, ports, and nets

A cell has a symbol (its name), exactly one principal port, and a fixed number of auxiliary ports. A net is a collection of cells whose ports are joined pairwise by wires. A port that has no wire is free, and the free ports form the net's interface.

        aux 1     aux 2
          |         |
        +-----------+
        |  symbol   |
        +-----+-----+
              |
           principal

Core insight. A net is a graph, and its rules rewrite the graph. Released Bend 2 does not build that graph. Its runtime runs definitions, as the BendRT block below shows.

Composed of: a net.

net
- cells: CON | DUP | ERA, each with one principal port
- auxiliary ports: CON 2, DUP 2, ERA 0
- wires: each joins two ports; a port with no wire is part of the interface

Active pairs and rules

Two cells joined by a wire between their principal ports form an active pair. Only an active pair can be reduced. A rule replaces an active pair with another net that has the same free ports. The rule is local: it reads two cells and rewrites them, and nothing else.

Each unordered pair of symbols has at most one rule. A net with k symbols therefore has at most k(k+1)/2 rules. A net is in normal form when no active pair remains.

Two active pairs never share a cell. A cell has one principal port, so it can be part of at most one active pair. This is the property that makes local, parallel reduction safe.

Confluence: order does not matter

Take two distinct active pairs in one net. Reducing either one leaves the other still reducible, and reducing both in either order produces the same net. This is one-step confluence, the diamond property:

          N
        /   \
   reduce a  reduce b
        \   /
          M

The bend2.dev page on interaction nets states a stronger property for the same systems: if a net has a normal form, reduction order does not change that result, or the number of interaction steps needed to reach it. The same page is clear about what this does not give you. It does not guarantee that every program terminates, that every implementation of the rules is correct, or that the implementation is free of synchronization, allocation, and scheduling costs.

Read those two claims as the model's claims. Chapter 05 shows what a real runtime must still pay for.

The symmetric interaction combinators

Lafont (1997) showed that three symbols are enough. The system is symmetric because its two binary symbols have the same shape, one principal and two auxiliary ports, so no special primitive is needed for lambda or copy. The bend2.dev page uses the Greek names γ, δ, ε; this chapter uses the names common in later literature:

There are six rules, one for each unordered pair of symbols:

1. CON–CON annihilates. The two cells disappear, and their auxiliary ports are reconnected pairwise: first with first, second with second.
2. DUP–DUP annihilates. The same crosswise reconnection as rule 1.
3. ERA–ERA annihilates. Both cells disappear and nothing replaces them.
4. CON–DUP commutes. Four new cells appear: two DUP copies attached to the CON's auxiliary wires, and two CON copies attached to the DUP's auxiliary wires. Each new CON is wired to each new DUP, so the four new cells form a 2×2 crossing. The number of cells goes from two to four.
5. CON–ERA erases. The CON cell disappears, and two new ERA cells are attached to its two auxiliary wires.
6. DUP–ERA erases. The same as rule 5, for a DUP cell.

Rule 4 is the one that copies. A DUP that meets a CON is pushed through it, so each of the CON's two results gets its own DUP. Repeated application copies a structure one layer at a time, and each step is one local interaction.

Lafont proved that these six rules are universal: a translation maps any other interaction system into them and preserves its computation and its parallelism. The bend2.dev page describes this as "universal", and it does not claim that the six rules alone make programs fast.

Labels: the Interaction Calculus

The three combinators above have one kind of DUP. Victor Taelin's Interaction Calculus (IC) keeps the same three kinds of cell, gives every DUP a label (a number), and adds a text notation for nets. The text is not a drawing: !&L{x,y} = t; body names cells and wires, the way λx.t names a CON. Read the text as cells:

Give every DUP one label, and the rule that two DUPs annihilate (rule 2 above) is the case where their labels match. Different labels commute instead. So the symmetric combinators are the special case with a single label.

So a superposition is not a new kind of cell. &L{a,b} is a DUP labelled L, read from the other side: its principal port faces the value, and its aux ports hold the alternatives. Both readings are drawn side by side:

!&L{x,y} = t; body      &L{a,b}
    x         y                 │
    │         │                 s
  ┌─┴─────────┴─┐        ┌──────┴──────┐
  │  DUP   L    │        │  DUP   L    │
  └──────┬──────┘        └─┬─────────┬─┘
         │                 │         │
         t                 a         b

Chapter 14 runs these rules on the reference implementation, prints the interaction counts, and shows where a superposition is born.

β-reduction as one interaction

Interaction nets encode a lambda abstraction and an application as two CON cells:

• λx. M is a CON whose principal port is the lambda's output, whose first auxiliary port is the variable x (a wire to every use of x), and whose second auxiliary port is the body M.
• (F A) is a CON whose principal port connects to the function F, whose first auxiliary port carries the argument A, and whose second auxiliary port carries the result.

When a lambda meets an application through their principal ports, that is an active pair of two CONs, and rule 1 applies. The first auxiliary wires join: the variable's wire now connects to the argument A. The second auxiliary wires join: the body M now connects to the result. β-reduction is one interaction.

If the variable is used twice, its wire must be duplicated, and each copy is a separate CON–DUP commutation. That is the duplication cost. The model does not hide it, and Chapter 04's exercises count it.

Why this matters for Bend, and what it does not

The bend2.dev notes describe interaction nets as the model behind Bend's earlier HVM runtimes. Released Bend 2 does not run them. Its compiler emits a flat C evaluator, called BendRT, that keeps pending work explicitly and does not reduce graphs. The notes list what BendRT does instead:

• Affine ownership. Each ordinary value has at most one live use, so the compiler knows when memory can be freed. No tracing garbage collector is needed.
• Counted sharing. A + value keeps a reference count. A value used through + is shared by count, not by graph.
• Balanced forks. a b = f(x) g(y) hands each call to a core once. The programmer promises the two calls take about the same time.

Core insight. BendRT is a flat evaluator of definitions. Its primitives are words, definitions, jumps and tasks, not cells and rewrites.

Composed of: BendRT, the released runtime.

BendRT
- term: one 64-bit word; a small value is stored inline, anything else is a pointer into one heap shared by every core and the GPU
- definition: a segment of a flat state machine; a call is a jump
- parallel call: one join task, plus one task per call, dealt to CPU or GPU lanes
- memory: no garbage collector; a match frees the node it opens; only `+` values carry a reference count, which the emitted C keeps in 24 bits

The guide's Under the Hood section gives the first three parts and the memory rule. The 24-bit width comes from the emitted C.

So the model explains why Bend is affine and why copying is spelled out. It does not predict how fast a program runs. The notes quote the Asperti and Mairson result that the implementation cost of optimal reduction cannot be bounded by an elementary function of the number of reduction steps. Counting interactions is not the same as measuring time.

Summary of properties

Exercises (pen and paper)

1. Erase a cell. A CON has its principal port wired to an ERA. Its two auxiliary ports are wired to two free ports, p and q. How many interactions happen, and what is left?

Solution. One interaction: rule 5. The CON disappears and two new ERA cells attach to p and q. Before the step there were two cells (CON, ERA). After it there are two cells (ERA, ERA). No active pair remains, so the net is in normal form.

2. Count the cells of a commutation. A CON and a DUP are joined through their principal ports. Their four auxiliary ports are wired to four free ports. How many cells and how many internal wires exist after rule 4?

Solution. Four cells: two DUP copies and two CON copies. The copies' principal ports take the four free wires, and their auxiliary ports form four internal wires, one for each (CON copy, DUP copy) pair. The number of cells rises from two to four.

3. Two active pairs. Net N has two active pairs, A and B, that share no cell. Show that reducing A then B gives the same net as reducing B then A.

Solution. Rule A rewrites only the cells of A and creates wires only to A's free ports, which are cells or interface ports that B does not touch. The same holds for B. Both orders therefore produce the same set of cells and wires, and the diamond closes.

4. Beta in one step. Encode (λx. x) y with two CONs, where y is a free port. Reduce it.

Solution. The lambda CON's first auxiliary wire (the variable x) meets the application's first auxiliary wire (the argument y), and the lambda's body wire meets the result wire. The body of the lambda is x, which is the variable's wire, so the result is directly connected to y. One interaction; no DUP was needed because x is used once.

Next

Chapter 05 shows what the released compiler does for a parallel call, and what a balanced fork looks like in code.

A.6 · bend-docs/src/content/tutorial/05-parallelism-and-runtime.md

Bend 2 tutorial 05: parallelism and the runtime · runnable · updated 2026-10-18 · canonical /tutorial/05-parallelism-and-runtime/

05: parallelism and the runtime

Bend runs independent recursive calls in parallel without threads, locks, or annotations. You write a parallel call, and the compiler makes it a fork. Two promises come with it. The calls must be independent, which purity and affine ownership guarantee. They must also take about the same time, which is your job. This chapter shows the shape that meets the second promise, and how to check the result honestly.

The parallel call

import Base

def pow2(+d: Nat) -> U32:
  match d:
    case 0n:
      1
    case 1n+p:
      a b = pow2(p) pow2(p)
      (a + b : U32)

def main() -> U32:
  pow2(12n)

4096

a b = pow2(p) pow2(p) is one line with two calls. Both start together, and the line continues when both have finished. +d lets both calls use the depth. The checker runs this program and prints 4096. A native binary runs the same calls on several cores. Compile it with bend pow2.bend -o pow2 and run ./pow2 --threads 8.

Bang runs the calls on a GPU. pow2!(12n) sends that call and every parallel call it makes to the GPU. The lab machine for this tutorial has no GPU device (there is no /dev/dri and no NVIDIA device), so the bang form was not timed here. On a machine with no usable GPU, --gpu off runs bang calls on the CPU threads.

How a call runs

A top-level definition is code, not a value, so calling it does not use it up. The checker counts uses of values: a closure may be called once, and a + value costs a reference count when it is shared (chapter 03). A definition may call itself as often as its argument shrinks (chapter 02).

The guide describes the run-time shape of those calls:

• A tail call compiles to a loop. leaf below calls itself in tail position, so each leaf becomes one loop.
• Bend has no C stack. Each definition compiles to a segment of a flat state machine, and a call is a jump.

The fork shape: a tree of leaves

A parallel call that splits one call into two equal halves is a fork. Forking at every level down to single numbers costs more in scheduling than the work itself. The shape that works has two parts:

• Tree. Above a fixed depth, split the range in two equal halves with a parallel call.
• Leaf. Below the tree, a tail loop walks 8 to 64 consecutive items with scalar accumulators. A loop of this kind compiles to one native loop.

This program sums the numbers from 0 to 511 with eight leaves of 64 items each:

import Base

def leaf(+n: Nat, +i: U32, acc: U32) -> U32:
  match n:
    case 0n:
      acc
    case 1n+p:
      leaf(p, (i + 1 : U32), (acc + i : U32))

def tree(+d: Nat, +i: U32) -> U32:
  match d:
    case 0n:
      leaf(64n, i, 0)
    case 1n+p:
      a b = tree(p, i) tree(p, (i + (64 << p) : U32))
      (a + b : U32)

def main() -> U32:
  tree(3n, 0)

130816

The check is arithmetic: the numbers 0 to 511 sum to 511 × 512 / 2 = 130816. Two details carry the design:

• The second half starts at i + (64 << p). Each leaf covers 64 indices, so a tree of depth p covers 64 << p indices, and the second half begins right after the first. The general formula is i + (L << p), where L is the leaf size. With leaves of one item it is i + (1 << p), which is why that form appears in other examples. With leaves of 64 it must use 64.
• The tree's halves are equal in work, because every leaf does the same 64 steps. A fork over unequal halves would leave one core idle.

Use a tree for data a fork splits, and a List for data a leaf walks once. Head-and-tail recursion over a list runs on one core, so use it only inside a leaf. Use an Array for data you index or update in place (chapter 03).

Exercises

1. Four levels. Change the depth to 4n. How many numbers are summed, and what is the output? Check your answer by running the program.

Solution. The tree covers 64 × 2⁴ = 1024 numbers, so the sum is 1023 × 1024 / 2 = 523776.

import Base

def leaf(+n: Nat, +i: U32, acc: U32) -> U32:
  match n:
    case 0n:
      acc
    case 1n+p:
      leaf(p, (i + 1 : U32), (acc + i : U32))

def tree(+d: Nat, +i: U32) -> U32:
  match d:
    case 0n:
      leaf(64n, i, 0)
    case 1n+p:
      a b = tree(p, i) tree(p, (i + (64 << p) : U32))
      (a + b : U32)

def main() -> U32:
  tree(4n, 0)

523776

2. Break the midpoint. Replace 64 << p with 1 << p in the program above and run it. Explain the output before you run it.

Solution. The halves overlap. The second half starts only one index after the first, so most indices are summed several times and the total is wrong. Expect the program to print 17920, and that the number is not 130816.

import Base

def leaf(+n: Nat, +i: U32, acc: U32) -> U32:
  match n:
    case 0n:
      acc
    case 1n+p:
      leaf(p, (i + 1 : U32), (acc + i : U32))

def tree(+d: Nat, +i: U32) -> U32:
  match d:
    case 0n:
      leaf(64n, i, 0)
    case 1n+p:
      a b = tree(p, i) tree(p, (i + (1 << p) : U32))
      (a + b : U32)

def main() -> U32:
  tree(3n, 0)

17920

Each leaf still sums 64 consecutive values from i. With the midpoint i + (1 << p), the second half of a level-one tree starts one index after the first, so every leaf overlaps its neighbour by 63 values. The total counts many values several times, and 17920 is not the sum 0 to 511. The check is simple: whenever a parallel sum disagrees with the sequential sum, recompute the midpoints first.

Build a native binary and run it

The checker runs a pure main slowly, so measure with a native build:

bend main.bend -o main
./main --threads 1
./main --threads 8

Both runs must print the same output. If they do not, the program has a bug, not a scheduling problem. The speedup is the one-thread time divided by the multi-thread time, measured on the same input, with checks that the outputs match.

Measure honestly

A speedup claim needs five things:

1. The same input for every run, and the same output checked against the one-thread result.
2. Several runs per mode, reported as a median, with the order rotated between modes.
3. The machine, thread count, GPU setting, and compiler version written down with the numbers.
4. A named baseline. "Twelve times faster" means nothing without the two times.
5. Build time separate from run time. Compile first, then time only the binary.

Small inputs mislead: for work this small, process startup dominates the time. Measure with inputs big enough that the run takes long enough to time reliably, and state how long that is.

Choosing the thread count

Bend has no automatic setting. --threads takes a number from 1 to 128, and without the flag a binary uses the CPU count, which ./main --help prints. --threads auto is rejected:

$ ./main --threads auto
bend: expected a thread count of 1 or more after --threads

Definition. The thread count is the --threads N setting of a native binary: the number of CPU threads it runs on, from 1 to 128. Without the flag it is the CPU count.

Core insight. The fastest count belongs to one program, one input, and one machine. The number of leaves does not give it. tree(d) has 2^d leaves, far more than any thread count, and the scheduler hands each task to a core once and never moves it (the guide). Measure.

A script can do the measuring. It runs each count after a warm-up, requires every run to print the output of the one-thread run, and reports the median and the range:

#!/usr/bin/env bash
# sweep.sh PROGRAM [THREADS...]
# Runs PROGRAM at each thread count after one warm-up run. Every timed run must
# print the same output as the one-thread run, or the sweep stops. Prints the
# median and range of RUNS runs per count, then the fastest count.
set -euo pipefail
prog=$1
shift
[ "$#" -gt 0 ] || set -- 1 2 4 8 12
runs=5
reference=$("$prog" --threads 1)
best_t=""
best_ms=""
for t in "$@"; do
  "$prog" --threads "$t" >/dev/null
  times=""
  for _ in $(seq "$runs"); do
    start=$(date +%s%N)
    out=$("$prog" --threads "$t")
    end=$(date +%s%N)
    if [ "$out" != "$reference" ]; then
      echo "threads=$t printed a different result; stopping" >&2
      exit 1
    fi
    times="$times $(( (end - start) / 1000000 ))"
  done
  sorted=$(printf '%s\n' $times | sort -n)
  median=$(printf '%s\n' "$sorted" | sed -n "$(( (runs + 1) / 2 ))p")
  low=$(printf '%s\n' "$sorted" | head -1)
  high=$(printf '%s\n' "$sorted" | tail -1)
  echo "threads=$t median=${median} ms (range ${low}-${high} ms)"
  if [ -z "$best_ms" ] || [ "$median" -lt "$best_ms" ]; then
    best_t=$t
    best_ms=$median
  fi
done
echo "fastest: --threads $best_t (${best_ms} ms)"

Save it as sweep.sh and run bash sweep.sh ./main 1 2 4 8 12 16 24, with main set to tree(26n, 0). On the lab machine (12 CPUs) it printed:

threads=1 median=366 ms (range 343-372 ms)
threads=2 median=214 ms (range 208-237 ms)
threads=4 median=150 ms (range 143-151 ms)
threads=8 median=108 ms (range 102-118 ms)
threads=12 median=112 ms (range 107-115 ms)
threads=16 median=108 ms (range 100-113 ms)
threads=24 median=101 ms (range 98-112 ms)
fastest: --threads 24 (101 ms)

Three things stand out:

• Most of the gain comes by 8 threads: 366 ms falls to 108 ms.
• The default of 12 was not the fastest. Sixteen and 24 were a few milliseconds faster, but their ranges overlap with the range of 12.
• On tree(22n, 0), one thread took 22 ms, and each of 4, 8, 12, 16, and 24 threads took 14 to 17 ms. Those differences are about the size of the run-to-run spread, so the sweep cannot choose a count there. Use an input large enough to time, as the section Measure honestly says.

The script has limits. It times wall-clock time on the machine it runs on, so other load changes the numbers. It needs bash and GNU date. Its answer holds for this program, this input, and this machine. The guide says the GPU shines on uniform numeric work, such as mandelbrot or nbody, and that divergent work, such as n-queens, stays faster on the CPU. Measure those too, with ! and without it.

Count what the compiler emits

bend main.bend -o main.c writes the C source. Three names mark runtime work that copies or releases a shared value: term_keep, ctr_take, and rfc_seal. A reference count is a term_keep. A program that uses + on values pays for them, and a program that does not should have none in its own functions.

For the pow2 program above, the compiler emitted term_keep 2 times, ctr_take 3 times, rfc_seal 2 times, and term_peek 6 times. A program with no sharing at all, def main() -> U32: 1, emits exactly the same counts. So those occurrences come from the runtime, and pow2 adds none of its own. term_peek is a borrow, which costs no count. When you audit a program, compare its counts with that baseline, and treat any new keep in your own code as a regression to remove or explain.

Next

Chapter 06 covers duplication and superposition, the terms behind labels and search. It also says plainly what the released compiler does not have.

A.7 · bend-docs/src/content/tutorial/06-duplication-superposition.md

Bend 2 tutorial 06: duplication, superposition, and SupGen · docs-only · updated 2026-10-18 · canonical /tutorial/06-duplication-superposition/

06: duplication, superposition, and SupGen

Your question mentions three things: copy-on-write with sup and dup, SupGen, and forks of running code. This chapter explains what the words mean in the lineage behind Bend, then shows what the released compiler accepts. Short version: the released Bend 2 has no sup syntax, no SupGen in its compiler or Base library, and no copy-on-write forks of running code. The rest of this chapter gives the evidence.

Duplication and superposition, in the calculus

The Interaction Calculus, which HVM4 implements, has two kinds of term for sharing:

• A duplication dup takes one value and gives two copies, linked by a label. It is the term-level form of the DUP cell in chapter 04.
• A superposition sup holds two alternatives at once, also linked by a label. It is the term-level form of a choice that exists in several places.

The bend2.dev HVM4 page gives a worked example in its own syntax, where &{1, 2} is a superposition of two numbers. Adding 10 to it gives the two results 11 and 12. The page says the evaluator performs an addition for each alternative, and that duplication "still consumes work and memory". Sharing saves work only when the alternatives share their computation.

Labels decide how two terms meet. In the HVM literature, a dup and a sup with the same label route their parts to each other, and with different labels they commute, creating new dup and sup terms. Chapter 14 runs these rules on Victor Taelin's Interaction-Calculus reference implementation, which is a separate implementation from HVM4. HVM4 itself was not run.

Core insight. dup and sup are two terms of one calculus. Their syntax differs, and they meet only through a label. Equal labels route, and different labels commute.

Composed of: a sharing term with label L.

sharing term, label L
- dup: !&L{x, y} = t; body     one value t, two uses x and y
- sup: &L{a, b}                two alternatives a and b, held in one place

Chapter 14 runs both rules. In its examples, equal labels take 2 interactions and different labels take 9.

Search by superposition

The bend2.dev note Search by superposition describes a technique built on this calculus. Apply a function to a superposition of its whole input domain, and the evaluator shares work across all inputs at once. The note reports results for a SAT instance and for program search. Those experiments used earlier HVM syntax. The page marks them documentation only: the numbers were reported by their author and were not re-run. Do not cite them as Bend 2 measurements.

What the released compiler accepts

These two programs are rejected by bend 2.0.25, and the messages are the real ones:

import Base

def main() -> U32:
  x = &{1, 2}
  (x + 10 : U32)

- expected : a name
- observed : '{'

if is not a keyword either. Bend branches with match, as chapter 01 shows:

import Base

def main() -> U32:
  if True{}:
    1
  else:
    2

- expected : '='
- observed : ':'

Adding a label does not help. The labelled form is rejected as well:

import Base

def main() -> U32:
  x = &0{1, 2}
  (x + 10 : U32)

- expected : ':'
- observed : ','

The released guide, Base, and the compiler say nothing about SupGen, and the bend2.dev pages document none. The site's own release-status note lists "Bend2–SupGen integration" among the launch blockers, and its HVM runtime note calls SupGen integration "still private". Treat SupGen as not available in the released compiler. Chapter 10 explains what you can do in its place.

What Bend 2 has instead of copy-on-write

The released language has copying operations, but none of them is a copy-on-write fork of a running program:

• + on a Data value shares the value and counts the sharing. Nothing is copied, and the count is kept in 24 bits.
• Array.clone copies every slot into a second array. The cost grows with the array's size.
• Array.fork gives two handles to one array in constant time. Both handles read and write the same cells, so racing writes go through atomic operations. It is marked @unsafe in Base, which means the checker does not verify it, and no law may depend on it.
• Templates make one compiled copy for each distinct template argument. The copy happens at compile time, not while the program runs.

None of these forks a live program. A running Bend program is a value that the compiler has already compiled, and nothing in the language rewrites it.

Exercises

1. Read the error. Explain, in one sentence each, why &{1, 2} and if are rejected.

Solution. &{ begins a superposition in HVM syntax, which the released parser does not accept, so it expects a name where it sees the brace. if is not a keyword, so the parser reads if True{} as the start of a binding and expects = where it finds :.

2. Two alternatives without superposition. Replace the idea of a superposed price with an ordinary choice. Write a Choice type with two constructors and a function that prices each one. Print both prices as a pair.

Solution. The alternatives are values, so they can be passed around, stored, and checked by laws. The output below is the pair of both prices.

import Base

type Choice is Data:
  Low{}
  High{}

def price(c: Choice) -> Nat:
  match c:
    case Low{}:
      10n
    case High{}:
      20n

def main() -> Nat & Nat:
  (price(Low{}), price(High{}))

(10n, 20n)

3. Why no law can use Array.fork. Explain what the @unsafe marker in Base changes for a law that depends on Array.fork.

Solution. The checker treats an @unsafe definition as outside its proof guarantees. A law whose proof depends on it is rejected in the proof check, so the law would be unverified. Chapter 11 shows the exact message.

Next

Chapter 07 covers laws and proofs, the part of Bend that checks properties of the values a program computes.

A.8 · bend-docs/src/content/tutorial/07-laws-and-proofs.md

Bend 2 tutorial 07: laws and proofs · runnable · updated 2026-10-18 · canonical /tutorial/07-laws-and-proofs/

07: laws and proofs

A law is a claim about a program, written as a type. Bend has no tactics and no proof search, so a proof is an ordinary definition with the same name as the law. The compiler checks that the definition has the claimed type. If you know Haskell, think of a QuickCheck property that the compiler must check for every input, not just sampled ones. If you know Lean, the table below maps the ideas, with one big difference: Bend has no tactics and no proof search, so every step is a term you write.

Core insight. A law is a type, and a proof is a program of that type. This is the Curry-Howard idea: a claim is a type, and a term that inhabits it is its proof. bend PROOF.bend accepts a proof only if its def has the law's type, its recursive calls terminate, and each {==} holds because both sides compute to the same term.

Composed of: a law and its proof.

law add_zero                      the type: a claim
- for x: Nat                      a binder
- {Nat.add(x, 0n) == x : Nat}     the claim

def add_zero(x)                   the program, with the law's name
- one case per constructor of x
- each case: {==}, or a rewrite %e : P followed by {==}

Your first law: induction

This law says that adding zero to any natural number does nothing:

import Base

law add_zero:
  for x: Nat
  {Nat.add(x, 0n) == x : Nat}

def add_zero(x):
  match x:
    case 0n:
      {==}
    case 1n+p:
      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
      {==}

def main() -> Nat:
  Nat.add(42n, 0n)

42n

Read the file in three parts.

• law add_zero: names the claim. for x: Nat quantifies over every natural. The equation {Nat.add(x, 0n) == x : Nat} is the claim itself: the two sides are equal at type Nat.
• def add_zero(x): is the proof. It has the same name as the law and one parameter for each for.
• match x: splits the proof into cases, and each branch refines the goal.

Look at the goal in each branch. In the case 0n, the left side Nat.add(0n, 0n) computes to 0n, which is the right side, so {==} closes the goal. In the case 1n+p, the left side is Nat.add(1n+p, 0n), and it computes to 1n+Nat.add(p, 0n), which is not yet 1n+p. The recursive call add_zero(p) is the induction hypothesis: it proves the claim for the smaller number p. The line %add_zero(p) : {...} rewrites the goal with that equation. The _ marks where the right-hand side of the equation goes. After the rewrite, both sides are the same, and {==} closes the goal.

The induction hypothesis is allowed only because p is smaller than x: it is a pattern-bound variable from 1n+p, so the termination rule of chapter 02 holds.

Equality by computation

When both sides compute to the same term, {==} alone is enough. The law below holds because Nat.add matches on its first argument, so 0n on the left reduces without any induction:

import Base

law zero_left:
  for x: Nat
  {Nat.add(0n, x) == x : Nat}

def zero_left(x):
  {==}

def main() -> Nat:
  Nat.add(0n, 5n)

5n

The same reasoning fails when the computed argument is a variable. This law puts the variable where the computation needs it, and {==} cannot prove it:

import Base

law twice_is_double:
  for x: Nat
  {Nat.add(x, x) == Nat.double(x) : Nat}

def twice_is_double(x):
  {==}

- expected : Nat.add(x, x)
- observed : Nat.double(x)

Both sides are correct, but {==} needs them to reduce to the same term, and the variable x blocks the reduction. Split the variable with match and prove each case, or use induction as add_zero does.

Boolean laws by cases

A law over a finite type needs one {==} per constructor. This law says negating twice gives back the original value:

import Base

law not_not:
  for b: Bool
  {Bool.not(Bool.not(b)) == b : Bool}

def not_not(b):
  match b:
    case True{}:
      {==}
    case False{}:
      {==}

def main() -> Bool:
  Bool.not(Bool.not(True{}))

True{}

Equality as a relation

Equality laws state that two computations give the same result. The bend2.dev example proves that cancelling a job twice has the same effect as cancelling it once, for every state. The job type and its cancel function live in another file:

job.bend

import Base

type State is Data:
  Queued{}
  Running{}
  Cancelled{}
  Finished{}

def cancel(state: State) -> State:
  match state:
    case Queued{}: Cancelled{}
    case Running{}: Cancelled{}
    case Cancelled{}: Cancelled{}
    case Finished{}: Finished{}

main.bend

import Base
import ./job.bend as Job

law cancel_idempotent:
  for state: Job.State
  {Job.cancel(Job.cancel(state)) == Job.cancel(state) : Job.State}

def cancel_idempotent(state):
  match state:
    case Job.Queued{}: {==}
    case Job.Running{}: {==}
    case Job.Cancelled{}: {==}
    case Job.Finished{}: {==}

def main() -> Job.State:
  Job.cancel(Job.cancel(Job.Running{}))

job.Cancelled{}

The law is checked as a type, so main does not need to call it. The output prints the constructor with its module prefix, job.Cancelled{}.

Two equality lemmas in Base help you rewrite equations: Equal.sym turns e : {a == b : T} into {b == a : T}, and Equal.trans chains two equations. The next example uses Equal.sym:

import Base

law flip:
  for +a: Nat
  for +b: Nat
  for e: {a == b : Nat}
  {b == a : Nat}

def flip(a, b, e):
  Equal.sym(Nat, a, b, e)

All terms check.

Existential laws

exs y: T in a law asks for a witness. The proof returns the witness together with the proof of the equation:

import Base

law has_zero:
  exs y: Nat
  {Nat.add(y, 0n) == 0n : Nat}

def has_zero():
  (0n, {==})

All terms check.

Holes: unfinished proofs

A ?TODO in a proof leaves that branch open. The checker counts open holes, and a file with any open hole fails the proof check:

import Base

law cancel_all:
  for x: Nat
  {Nat.add(x, 0n) == x : Nat}

def cancel_all(x):
  match x:
    case 0n:
      {==}
    case 1n+p:
      ?TODO

Error: 1 TODO found.
The code is incomplete, and not a valid proof yet.

A named hole, ?name, stops the check and prints the goal that the branch must prove. Here the goal is printed for the branch 1n+p:

import Base

law add_zero:
  for x: Nat
  {Nat.add(x, 0n) == x : Nat}

def add_zero(x):
  match x:
    case 0n:
      {==}
    case 1n+p:
      ?inspect

- expected : {1n+Nat.add(p, 0n) == 1n+p : Nat}
- observed : ?inspect

Use ?name to see the goal you must prove, then replace it with a proof. Leave ?TODO only while you write the file. The proof gate rejects both.

LAWS and PROOF: the project layout

A project keeps its claims and its proofs apart. LAWS.bend imports the code and states the laws. PROOF.bend imports both and proves each law with a def of the same name, as def Laws.name for a law named name. The example below stores three files in one directory. job.bend is the code under test, and it is the same file as in the equality example. LAWS.bend states four laws about it:

job.bend

import Base

type State is Data:
  Queued{}
  Running{}
  Cancelled{}
  Finished{}

def cancel(state: State) -> State:
  match state:
    case Queued{}: Cancelled{}
    case Running{}: Cancelled{}
    case Cancelled{}: Cancelled{}
    case Finished{}: Finished{}

LAWS.bend

import Base
import ./job.bend as Job

law cancel_idempotent:
  for state: Job.State
  {Job.cancel(Job.cancel(state)) == Job.cancel(state) : Job.State}

law cancels_queued:
  {Job.cancel(Job.Queued{}) == Job.Cancelled{} : Job.State}

law cancels_running:
  {Job.cancel(Job.Running{}) == Job.Cancelled{} : Job.State}

law preserves_finished:
  {Job.cancel(Job.Finished{}) == Job.Finished{} : Job.State}

PROOF.bend

import Base
import ./job.bend as Job
import ./LAWS.bend as Laws

def Laws.cancel_idempotent(state):
  match state:
    case Job.Queued{}: {==}
    case Job.Running{}: {==}
    case Job.Cancelled{}: {==}
    case Job.Finished{}: {==}

def Laws.cancels_queued():
  {==}

def Laws.cancels_running():
  {==}

def Laws.preserves_finished():
  {==}

All terms check.

bend PROOF.bend is the gate. It checks every law and every proof, and it prints All terms check. only when none is open. Run bend LAWS.bend alone and every law is an open claim. The message counts them as TODOs:

Error: 4 TODOs found.

Two rules follow from the layout:

• An accepted law is never weakened to pass. Changing a law so that its proof becomes easy defeats its purpose. If a proof is hard, the law may be correct and the proof is what needs work.
• A law with no def is an open claim. It stays open until a same-named def proves it. A file that states a law and leaves it unproved fails the gate.

Chapter 11 covers the gate's other failure mode: a proof that depends on an @unsafe definition. Version 2.0.25 prints a warning and still exits with status 0, so do not treat exit status alone as the gate. Bend 2.0.36 adds bend PROOF.bend --verdict, which rechecks the proofs with a separate kernel. The bend2.dev notes say that option needs Lean v4.34.0 exactly, or a prebuilt kernel named by the BENDTT variable. Version 2.0.25 has no such option, and no Lean toolchain was installed on the lab machine, so the gate in this tutorial is bend PROOF.bend plus a reading of its output.

Exercises

1. Prove a right identity. Prove Nat.add(x, 0n) == x without copying add_zero, by naming the induction hypothesis and rewriting with it.

Solution. This is the proof above. Put the hypothesis add_zero(p) in a rewrite whose motive is 1n+_, then close with {==}.

2. Find the failing proof. The law cancels_running states that cancelling a running job yields Cancelled{}. Change the Running{} branch of cancel to return Queued{} and predict what the gate prints.

Solution. The gate fails, because cancels_running no longer holds for the new cancel. The law is the specification, and the implementation has to meet it.

Next

Chapter 08 covers types that depend on values, and why they make preconditions checkable.

A.9 · bend-docs/src/content/tutorial/08-dependent-types-and-totality.md

Bend 2 tutorial 08: dependent types and totality · runnable · updated 2026-10-18 · canonical /tutorial/08-dependent-types-and-totality/

08: dependent types and totality

A dependent type is a type that a function computes from a value. In Haskell you reach for GADTs or type families. In Bend every type is an ordinary function call, so the same machinery that checks values checks types. This chapter shows three uses: a type that is Unit for one input and Empty for another, a list whose length is part of its type, and the rule that keeps every such definition terminating.

Three kinds of type appear in this chapter:

A dependent type is a function that returns a type. IsZero takes a Nat and returns Unit or Empty, and that result limits what a caller may pass: for 0n there is one value to pass, and for 1n+p there is none. The two sections below build those dependent types.

A type that computes

IsZero(n) is Unit when n is zero and Empty otherwise. Empty has no values, so a function that demands an IsZero argument can only be called with zero:

import Base

def IsZero(n: Nat) -> Type:
  match n:
    case 0n:
      Unit
    case 1n+p:
      Empty

def require_zero(n: Nat, evidence: IsZero(n)) -> Nat:
  n

def main() -> Nat:
  require_zero(0n, Unit{})

0n

Unit{} is the only value of Unit, so the caller must supply it. Calling require_zero(1n, Unit{}) is rejected, because IsZero(1n) is Empty and Unit{} is not an Empty:

import Base

def IsZero(n: Nat) -> Type:
  match n:
    case 0n:
      Unit
    case 1n+p:
      Empty

def require_zero(n: Nat, evidence: IsZero(n)) -> Nat:
  n

def main() -> Nat:
  require_zero(1n, Unit{})

- expected : Empty

A function whose argument has type Empty can be written with an empty match. It needs no case, because no value can exist:

import Base

def from_empty(-A: Type, e: Empty) -> A:
  match e:

def main() -> Nat:
  0n

0n

Length in the type

A Vec is a nested pair, and its type depends on a Nat length. first takes a list of length 1n+n, which is one or more, so it has no empty case:

import Base

def Vec(-A: Type, n: Nat) -> Type:
  match n:
    case 0n:
      Unit
    case 1n+p:
      A & Vec(A, p)

def first(-A: Type, -n: Nat, xs: Vec(A, 1n+n)) -> A:
  (x, rest) = xs
  x

def total(n: Nat, xs: Vec(U32, n)) -> U32:
  match n:
    case 0n:
      0
    case 1n+p:
      (x, rest) = xs
      (x + total(p, rest) : U32)

def main() -> U32 & U32:
  x = first(U32, 2n, (10, (20, (30, Unit{}))))
  s = total(3n, (10, (20, (30, Unit{}))))
  (x, s)

(10, 60)

Two things make this work. The length n determines how many pairs total consumes, and its recursive call gets the smaller length p. The parameter n of first is erased: it appears only in the type, so it does not exist at run time (the - marks it).

Haskell would enforce this with a length-indexed GADT and a Nat-kinded phantom type. Bend uses the same idea, but the index is an ordinary function that the checker evaluates.

A proof that uses a type

A law can take evidence as an argument. IsEven(x) below is Unit for zero, Empty for one, and IsEven(p) for 2n+p. The law says halving an even number and doubling the result gives the number back. The evidence e is what makes the law true for only even inputs:

import Base

def IsEven(n: Nat) -> Type:
  match n:
    case 0n:
      Unit
    case 1n+0n:
      Empty
    case 2n+p:
      IsEven(p)

def half(n: Nat) -> Nat:
  match n:
    case 0n:
      0n
    case 1n+0n:
      0n
    case 2n+p:
      1n+half(p)

law half_ok:
  for x: Nat
  for e: IsEven(x)
  {Nat.double(half(x)) == x : Nat}

def half_ok(x, e):
  match x:
    case 0n:
      {==}
    case 1n+0n:
      match e:
    case 2n+p:
      %half_ok(p, e) : {2n+Nat.double(half(p)) == 2n+_ : Nat}
      {==}

def main() -> Nat:
  half(8n)

4n

The branch 1n+0n has no proof body of its own. Its evidence e has type Empty, so match e: with no cases closes the branch. The indentation of case 2n+p: is the one the checker accepts after an empty match, and it is the same as the bend2.dev example.

Totality: every recursion shrinks

Bend requires every safe recursive call to pass a structurally smaller input, as chapter 02 explains. The rule holds for proofs as well as for programs, because a proof is also a recursive definition. Two consequences matter in practice.

1. A recursion that does not shrink is rejected, so a loop bounded by the outside world takes a Nat fuel argument and matches its predecessor.
2. Mutual recursion is not allowed in a safe definition. Merge the functions into one with a selector argument.

When @unsafe changes the rules

@unsafe disables the termination check for one definition. The compiler still runs the function, but any proof that depends on it is outside the guarantee. This program runs and prints 3, with a warning that the proof check now depends on unsafe code:

import Base

@unsafe def idu(n: Nat) -> Nat:
  match n:
    case 0n:
      0n
    case 1n+p:
      1n+idu(p)

def main() -> Nat:
  idu(3n)

3n
All terms check, but 2 defs rely on unsafe or foreign code:

The same definition used by a law is the case that matters. Version 2.0.25 reports it and exits with status 0, so the gate must read the message, not just the status:

import Base

@unsafe def idu(n: Nat) -> Nat:
  match n:
    case 0n:
      0n
    case 1n+p:
      1n+idu(p)

law idu_two:
  {idu(2n) == 2n : Nat}

def idu_two():
  {==}

All terms check, but 2 defs rely on unsafe or foreign code:

Be careful with unsafe loops too. A law that requires the checker to evaluate a non-terminating @unsafe function does not finish. In one run on this machine, a law of that shape ran for more than 20 seconds before the run was stopped. Keep @unsafe out of every definition that a law depends on, and keep laws about terminating functions.

Exercises

1. Odd numbers. Write IsOdd(n) that is Empty for zero, Unit for one, and IsOdd(p) for 2n+p. It is the complement of IsEven. Check that a function pred_odd(n, e) needs IsOdd(n): prove IsOdd(1n) by building Unit{}, and check that IsOdd(0n) is empty.

Solution. IsOdd mirrors IsEven. The function pred_odd takes evidence that its argument is odd. IsOdd(0n) is Empty, so the zero case is closed by an empty match. Odd numbers such as 5n pass the evidence Unit{}:

import Base

def IsOdd(n: Nat) -> Type:
  match n:
    case 0n:
      Empty
    case 1n+0n:
      Unit
    case 2n+p:
      IsOdd(p)

def pred_odd(n: Nat, e: IsOdd(n)) -> Nat:
  match n:
    case 0n:
      match e:
    case 1n+p:
      p

def main() -> Nat:
  pred_odd(5n, Unit{})

4n

To check that IsOdd(0n) is empty, match on evidence of that type. A match with no cases closes the branch:

import Base

def IsOdd(n: Nat) -> Type:
  match n:
    case 0n:
      Empty
    case 1n+0n:
      Unit
    case 2n+p:
      IsOdd(p)

def odd_zero_empty(e: IsOdd(0n)) -> Nat:
  match e:

def main() -> Nat:
  1n

1n

2. Fuel. Write repeat(fuel, x) that returns x plus fuel, using the fuel as the loop bound: each step adds 1 to x. Explain why it terminates.

Solution. It terminates because the first argument fuel is matched and the recursive call gets its predecessor. The following program adds 5 to 10:

import Base

def repeat(fuel: Nat, x: U32) -> U32:
  match fuel:
    case 0n:
      x
    case 1n+p:
      repeat(p, (x + 1 : U32))

def main() -> U32:
  repeat(5n, 10)

15

Next

Chapter 09 covers the IO monad, files, command-line arguments, and the compilation targets.

A.10 · bend-docs/src/content/tutorial/09-io-files-and-targets.md

Bend 2 tutorial 09: IO, files, and targets · runnable · updated 2026-10-18 · canonical /tutorial/09-io-files-and-targets/

09: IO, files, and targets

Bend is pure. Effects live in the type IO, and a do block sequences them, much as Haskell's IO monad does. The differences are that every bind names its type, and that a file handle is affine: an operation on a handle gives the handle back with its result. This chapter covers the effect forms, files, arguments, and the three compilation targets.

Sequencing effects

A do block runs its lines in order. A bind x : T <- action runs an action and names its result with a type. A plain line runs an action whose result is Unit, and return v ends the block with a pure value:

import Base

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print("first")
    IO.print("second")

first
second

The last line of a do block must be an effect or a return. A pure term there is rejected:

import Base

def main() -> IO(Unit):
  do IO<Unit>:
    (6 * 7 : U32)

- observed : U32

import Base

def greet(name: String) -> IO(String):
  do IO<String>:
    IO.sleep(1)
    return "Hello, " ++ name

def main() -> IO(Unit):
  do IO<Unit>:
    text : String <- greet("Ada")
    IO.print(text)

Hello, Ada

In that example IO.sleep(1) waits one millisecond, and return wraps the pure string as an IO result. Every bind carries a type, as in text : String <- greet("Ada"). Without it, the checker cannot choose the monad's type arguments.

Boxes: pure, bind, and effects

The picture is a model, not the runtime. An IO(A) is an effect: when it runs, it produces an A. Read the outer box as the effect and the inner box as the value, which exists only after the effect runs. A do block moves values between the boxes:

               String
          ┌──────────────┐
          │ "Hello, Ada" │
          └──────────────┘
                  │ return v: box a pure value
                  ▼
        ┌──────────────────┐
        │ IO(String)       │
        │                  │
        │ ┌──────────────┐ │
        │ │ "Hello, Ada" │ │
        │ └──────────────┘ │
        └──────────────────┘
                  │ text <- ...: run, then unbox
                  ▼
           text : String
              ┌──────┐
              │ text │
              └──────┘
                  │ IO.print(text): box a new effect
                  ▼
       ┌────────────────────┐
       │ IO(Unit)           │
       │                    │
       │ ┌────────────────┐ │
       │ │ IO.print(text) │ │
       │ └────────────────┘ │
       └────────────────────┘

The same program, checked:

import Base

def greet(name: String) -> IO(String):
  do IO<String>:
    return "Hello, " ++ name

def main() -> IO(Unit):
  do IO<Unit>:
    text : String <- greet("Ada")
    IO.print(text)

Hello, Ada

• return v boxes a pure value. It is IO.pure.
• text : String <- greet("Ada") runs the effect and takes the value out. This is the only way out of a box.
• IO.print(text) makes a new effect: a box of type IO(Unit).

What a do block means

The guide defines do by two rules. x : A <- v becomes M.bind(xs.., A, R, v, x => ...), and return e becomes M.pure(xs.., R, e). For IO, Base defines IO.pure(A, x) and IO.bind(A, B, m, f). The program above is the same as these calls:

import Base

def greet(name: String) -> IO(String):
  IO.pure(String, "Hello, " ++ name)

def main() -> IO(Unit):
  IO.bind(String, Unit, greet("Ada"), text => IO.print(text))

Hello, Ada

A plain line is a bind whose result is Unit, so two effects in a row are one bind with a lambda that ignores its argument:

import Base

def main() -> IO(Unit):
  IO.bind(Unit, Unit, IO.print("x"), u => IO.print("y"))

x
y

Matching on IO

An IO(A) has no constructors, so a constructor pattern on it is rejected:

import Base

def greet(name: String) -> IO(String):
  do IO<String>:
    return "Hello, " ++ name

def show(io: IO(String)) -> IO(Unit):
  match io:
    case Some{x}:
      IO.print("some")
    case None{}:
      IO.print("none")

def main() -> IO(Unit):
  show(greet("Ada"))

- expected : a datatype

A match also cannot head a statement inside do, because a match heads a def body. Binding a value and then matching it in the same block is rejected:

import Base

def greet(name: String) -> IO(String):
  do IO<String>:
    return "Hello, " ++ name

def main() -> IO(Unit):
  do IO<Unit>:
    text : String <- greet("Ada")
    match text:
      case _:
        IO.print(text)

- expected : a term (a match heads a def body, not a term)

A wildcard case _: on an IO parameter is accepted, but its branch cannot see inside the effect. The pattern that works is to bind the value with <- and pass it to a def whose match inspects it:

import Base

def find(n: U32) -> IO(Maybe<&2, U32>):
  do IO<Maybe<&2, U32>>:
    return Some{n}

def show(m: Maybe<&2, U32>) -> IO(Unit):
  match m:
    case Some{x}:
      IO.print(U32.show(x))
    case None{}:
      IO.print("none")

def main() -> IO(Unit):
  do IO<Unit>:
    m : Maybe<&2, U32> <- find(7)
    show(m)

7

Concurrency: fork and join

IO.fork starts an effect in the background and returns a channel for its result. IO.join waits on that channel. Between the two, the main effect keeps running:

import Base

def delayed() -> IO(String):
  do IO<String>:
    IO.sleep(1)
    return "done"

def main() -> IO(Unit):
  do IO<Unit>:
    channel : Chan(String) <- IO.fork(String, delayed())
    IO.print("waiting")
    text : String <- IO.join(String, channel)
    IO.print(text)

waiting
done

The event loop interleaves the effects. It is not a parallel call: an effect that waits on a timer, a socket, or a channel steps aside for the others. The guide says each computation runs its pure code, possibly in parallel on every core, up to its next effect. Use IO.fork for work that waits, and a parallel call (chapter 05) for pure work that divides.

Chan.new, Chan.send, Chan.recv, and Chan.close are the low-level operations under IO.fork and IO.join. Their signatures are in Base, and bend base Chan prints them.

Channels: values between computations

IO.fork returns a channel for one result. For a stream of values, make a channel with Chan.new, give the sending computation the channel, and receive from the other side. Chan.new(U32, 4) makes a channel with room for four values. Chan.recv returns Some{value} for each value sent, and None{} once the channel is closed:

import Base

def send_numbers(+chan: Chan(U32)) -> IO(Unit):
  do IO<Unit>:
    sent1 : Bool <- Chan.send(U32, chan, 10)
    sent2 : Bool <- Chan.send(U32, chan, 20)
    Chan.close(U32, chan)

def show_message(m: Maybe<&1, U32>) -> IO(Unit):
  match m:
    case None{}:
      IO.print("closed")
    case Some{n}:
      IO.print(U32.show(n))

def main() -> IO(Unit):
  do IO<Unit>:
    +chan : Chan(U32) <- Chan.new(U32, 4)
    IO.spawn(Unit, send_numbers(chan))
    first : Maybe<&1, U32> <- Chan.recv(U32, chan)
    show_message(first)
    second : Maybe<&1, U32> <- Chan.recv(U32, chan)
    show_message(second)
    third : Maybe<&1, U32> <- Chan.recv(U32, chan)
    show_message(third)

10
20
closed

IO.spawn starts a computation whose result nobody waits for. Here the sender runs in the background, and the receiver reads the values in the order they were sent.

Files: affine handles

A file is a handle, and a handle has one owner. Each operation on it returns the handle beside its result, so you must keep the handle and pass it on. File.open returns a Result, and IO.try unwraps it or ends the program with the error. This program writes a file and closes it:

import Base

def finish(result: File & Result<&1, &1, U32 & String, Unit>) -> IO(Unit):
  match result:
    case (file, status):
      do IO<Unit>:
        File.close(file)
        IO.pass(Unit, status)
        IO.print("written")

def main() -> IO(Unit):
  do IO<Unit>:
    file : File <- IO.try(File, File.open("message.txt", "w"))
    result : File & Result<&1, &1, U32 & String, Unit> <- File.write(file, "Hello from Bend")
    finish(result)

written

The program writes message.txt in the directory where you run it, and it replaces any earlier contents. The finish helper closes the handle on every path before it passes the status along. A handle that is not closed is a leak: the checker does not force you to close it, so you must do it yourself.

The guide's list of effect kinds includes TCP and UDP sockets, windows, and audio. Their handles follow the same affine rule. bend base prints their signatures.

Command-line arguments

IO.args() returns the arguments after the program name, as a List<String>. The compiler's own options are removed, and -- ends them. Here the program prints how many arguments it received:

import Base

def main() -> IO(Unit):
  do IO<Unit>:
    args : List<String> <- IO.args()
    IO.print(Nat.show(List.length(&1, String, args)))

0

Run it with arguments to see the count change:

bend main.bend one two
bend main.bend -- one two

Both commands print 2 in this lab. The List.length call takes its quantity first, &1 for a list of affine elements, which is why the version without it is rejected (chapter 11).

Error results and exits

Two Base effects end a program on purpose. IO.die(-A, code, msg) ends the program with the exit code and the message. IO.pass(-A, r) turns a Result into an effect that either returns the value or fails with its error. Prefer IO.pass and IO.try when the failure can be handled, and reserve IO.die for a program that cannot continue.

Reading the environment

IO.get_env returns a Result. Matching on it handles the failure case. This variable is unset, so the program prints missing:

import Base

def describe(r: Result<&1, &1, U32 & String, String>) -> IO(Unit):
  match r:
    case Fail{e}:
      IO.print("missing")
    case Done{v}:
      IO.print(v)

def main() -> IO(Unit):
  do IO<Unit>:
    r : Result<&1, &1, U32 & String, String> <- IO.get_env("BEND_TUTORIAL_UNSET")
    describe(r)

missing

Compilation targets

Bend has three targets. The same source compiles to each of them.

bend main.bend -o main.c
bend main.bend -o main
./main --threads 8
bend main.bend -o main.js
node main.js

• -o main.c writes one C file that contains the runtime and your program. Compile it with any C compiler, or inspect it, as chapter 05 does.
• -o main builds a native executable with clang 14 or newer. A binary that uses ! also writes main.gpu, which must stay beside it. --gpu off runs bang calls on the CPU.
• -o main.js writes standalone JavaScript. The JavaScript target runs parallel bindings one after another.

The native and JavaScript targets print the same text, which this lab checked for the program below. It is the example from the compile-to-JavaScript page:

import Base

def main() -> IO(Unit):
  IO.print("Bend on JavaScript")

Bend on JavaScript

bend main.bend without -o runs the program directly. An IO main runs compiled, and a pure main is evaluated by the checker, so a pure main is slow for large work.

Exercises

1. Two greetings. Write main so that it runs greet("Ada") and then greet("Lin"), printing each greeting on its own line.

Solution. Two binds in one do block run in order.

import Base

def greet(name: String) -> IO(String):
  do IO<String>:
    return "Hello, " ++ name

def main() -> IO(Unit):
  do IO<Unit>:
    first : String <- greet("Ada")
    second : String <- greet("Lin")
    IO.print(first)
    IO.print(second)

Hello, Ada
Hello, Lin

2. Count the handles. Explain why File.write(file, ...) returns the handle again, and what would break if it did not.

Solution. A file handle is affine. If the write consumed the handle and returned only the result, the program could not close it afterwards. The handle would be lost, and the file would stay open. Returning the handle with the result keeps the single owner, so the program can close it on every path.

Next

Chapter 10 applies everything so far to your questions: forks, branches, and self-changing code.

A.11 · bend-docs/src/content/tutorial/10-branching-and-self-change.md

Bend 2 tutorial 10: branching and self-change · runnable · updated 2026-10-18 · canonical /tutorial/10-branching-and-self-change/

10: branching and self-change

The request behind this chapter asks for four things: SupGen, cheap copy-on-write forks of code (with sup and dup), homoiconic code that changes itself, and forking a running program with new code so that the main code keeps working and new branches can be tested cheaply. This chapter says which of these the released Bend 2 compiler offers, which it does not, and what to do instead. The short answer is that the part you can have is the laws-first workflow for pure code, and the rest is either absent from the compiler or cannot be stated as a law.

What each requirement needs

Two lines in that table are absolute. A law states what a value computes, and the released compiler has no way to state the cost of sharing. Time and memory are measurements.

The workflow that works today

For pure code, a branch is a new value or a new constructor, and the checker tests it against the same laws as main.

1. State the requirement as laws. Put the claims in LAWS.bend, and never weaken an accepted law to get a proof through.
2. Implement the main behaviour as pure functions over Data. Keep the input and output shell thin, so the laws can pin the pure part.
3. Add a branch as a new constructor or a new definition. Existing cases do not change, so the main laws keep their proofs.
4. Write one law per branch, plus laws that relate the branch to main. A difference law says where the branch may differ from main. A fork law says a branch that changes nothing behaves exactly like main.
5. Prove in PROOF.bend. The gate must print All terms check. with no line about unsafe or foreign code.
6. Measure the branch separately, with native builds, as chapter 05 describes.

The pattern works because the laws quantify over every constructor. A new constructor that is not covered by a proof makes the gate fail. The compiler enforces that every new branch carries its own proof.

Pattern 1: a branch as a template

A template argument is a compile-time choice. Two different steps give two compiled copies of one loop, with no run-time selection:

import Base

def run(~step: U32 -> U32, n: Nat, x: U32) -> U32:
  match n:
    case 0n:
      x
    case 1n+p:
      run(~step, p, step(x))

def main_step(x: U32) -> U32:
  (x + 1 : U32)

def branch_step(x: U32) -> U32:
  (x + 2 : U32)

def main() -> U32 & U32:
  (run(~main_step, 3n, 0), run(~branch_step, 3n, 0))

(3, 6)

A law can pin the branch at one input, and the proof is computation. The checker evaluates the concrete U32 arithmetic, so {==} is enough:

import Base

def branch_step(x: U32) -> U32:
  (x + 2 : U32)

law branch_at_zero:
  {branch_step(0) == 2 : U32}

def branch_at_zero():
  {==}

def main() -> U32:
  branch_step(0)

2

A law over every input needs induction or a proof by cases, as chapter 07 shows. The concrete law is the smallest useful claim, and it runs in the same gate.

Pattern 2: a program as data

Homoiconic code means that a program is also data that other code can build and inspect. Bend does not quote its own definitions, but you can represent an expression as a Data type and interpret it. A branch is then a different expression value, and the main expression is untouched. Bend is strict, so the data below is built and not computed: eval is the only step that computes a value. To keep work unevaluated, you can use a lambda (x => ...), a template (~f), or data like this. Chapter 12, section 11, shows all three:

import Base

type Expr is Data:
  Lit{n: Nat}
  Add{a: Expr, b: Expr}
  Mul{a: Expr, b: Expr}

def eval(e: Expr) -> Nat:
  match e:
    case Lit{n}:
      n
    case Add{a, b}:
      Nat.add(eval(a), eval(b))
    case Mul{a, b}:
      Nat.mul(eval(a), eval(b))

def main() -> Nat & Nat:
  main_expr : Expr = Add{Lit{2n}, Lit{3n}}
  branch_expr : Expr = Add{Lit{2n}, Mul{Lit{3n}, Lit{2n}}}
  (eval(main_expr), eval(branch_expr))

(5n, 8n)

Both values are pure, so evaluating the branch cannot change the main value. The interpreter eval is the place for laws: a law such as "eval of Add{a, b} is the sum of the evals" can be proved by a case split. This is homoiconic in a limited sense: the program is data you can build and test. It is not self-modification of the running binary, and it does not give you cheap sharing of two programs. Each Expr value is built and stored in memory, and the cost is what chapter 05 measures.

Pattern 3: the difference between branches

The most useful law for a branch relates it to main. Suppose the branch should never give a larger answer than main. Write the claim, and let the gate check it:

law branch_never_more:
  for x: U32
  {U32.is_le(branch_step(x), main_step(x)) == True{} : Bool}

That law is false for the example above, because branch_step adds 2 and main_step adds 1. The gate would reject it, and that is the point: a difference law states exactly how the branch may differ from main, and a branch that breaks it is not accepted. Write the law you want, then change the branch until the gate accepts it, not the other way round.

What is not possible, and why

• SupGen is not in the released compiler. Nothing in this chapter depends on it, and no law can refer to it.
• Copy-on-write forks with sup and dup need a construct the parser rejects (chapter 06). The nearest things are Array.fork, which is @unsafe and so cannot support a law, and Array.clone, which copies.
• Bend 2 does not fork a running program. It compiles each program to a fixed binary, and a second program is a second file that you compile. The calculus forks terms, not processes: a superposition holds two alternatives, and applying it runs both on one shared input (chapter 14). The released compiler does not expose that.
• Cost is not a law. The checker proves that a branch computes the right values. It does not prove that the branch is cheap. Measure it, count the keeps in the emitted C (chapter 05), and compare builds.

Exercises

1. A third step. Add a template step triple_step that adds 3, and make main return the three results as a triple. Predict the output before you run it.

Solution. The result is (3, 6, 9) for three steps of three applications each. Triples are written A & B & C.

import Base

def run(~step: U32 -> U32, n: Nat, x: U32) -> U32:
  match n:
    case 0n:
      x
    case 1n+p:
      run(~step, p, step(x))

def main_step(x: U32) -> U32:
  (x + 1 : U32)

def branch_step(x: U32) -> U32:
  (x + 2 : U32)

def triple_step(x: U32) -> U32:
  (x + 3 : U32)

def main() -> U32 & U32 & U32:
  (run(~main_step, 3n, 0), run(~branch_step, 3n, 0), run(~triple_step, 3n, 0))

(3, 6, 9)

2. A law for a concrete input. Write the law that triple_step(0) is 3, and prove it by computation.

Solution. The same shape as branch_at_zero. The concrete arithmetic reduces, so {==} proves it.

import Base

def triple_step(x: U32) -> U32:
  (x + 3 : U32)

law triple_at_zero:
  {triple_step(0) == 3 : U32}

def triple_at_zero():
  {==}

def main() -> U32:
  triple_step(0)

3

Next

Chapter 11 lists the checker's rules and every official diagnostic with the message the released compiler prints.

A.12 · bend-docs/src/content/tutorial/11-rules-and-errors.md

Bend 2 tutorial 11: checker rules and errors · runnable · updated 2026-10-17 · canonical /tutorial/11-rules-and-errors/

11: checker rules and errors

This chapter is a reference. The checker runs before any program executes, and it stops with a message when a rule fails. Each rule below is taught in an earlier chapter, and each official diagnostic appears here with the text bend 2.0.25 prints. The official index on bend2.dev was written against 2.0.36, and its wording differs in places. Both wordings are in the tables.

The rules

The official diagnostics

Each heading names the diagnostic on bend2.dev. The code is the broken program from the official catalogue, and the error lines are what bend 2.0.25 printed for it. Where a chapter already shows the program and its message, this page links to it.

A variable was consumed more than once

Chapter 03 shows the program and its fix. The message is - expected : n and - observed : n (consumed more than once).

An operator has no type annotation

Chapter 01 shows the program and its fix. The message is - message : a type for this operator (write (a + b : Nat)).

A match cannot inspect a computed value

Chapter 01 shows the program and its fix. The message is - message : a parameter or field scrutinee (a match cannot scrutinize a computed value: give it its own def).

A function calls one defined below it

Chapter 02 shows the program and its fix. The message is - expected : a defined name.

A recursive call does not decrease

Chapter 02 shows the program and its fix. The message begins - expected : a decreasing self-call.

A name is not defined

import Base

def main() -> Nat:
  missing()

- expected : a defined name
- observed : missing

Define missing above main, or import the file that defines it.

A law is missing its proof

Chapter 07 shows the program. The message is Error: 1 TODO found., and the same file with {==} as its proof prints All terms check.

Definitions rely on unsafe or foreign code

Chapter 08 shows the case that matters. The official program in this catalogue uses names that end in ?, which bend 2.0.25 cannot parse:

import Base

def is_even?(n: Nat) -> Bool:
  match n:
    case 0n: True{}
    case 1n+p: is_odd(p)

- expected : '('

The fix in 2.0.36 is @unsafe, and 2.0.25 accepts that spelling too. The rule itself: a law that depends on an @unsafe definition is not verified. Chapter 08 shows the warning this version prints.

The result has the wrong type

import Base

def main() -> U32:
  True{}

- expected : U32
- observed : Bool

Return a value of the declared type.

Errors this tutorial found beyond the official list

These errors were produced by real programs while writing the chapters. They are not in the official index.

A superposition literal. &{1, 2} is rejected (chapter 06).

An if statement. Bend has no if (chapter 06).

A constructor without a type. A let with no context cannot infer the type of a constructor:

import Base

type Tok is Data:
  Tok{n: Nat}

def show(t: Tok) -> Nat:
  match t:
    case Tok{n}:
      n

def main() -> Nat:
  t = Tok{3n}
  show(t)

- expected : an annotated term (cannot infer)

Write t : Tok = Tok{3n}, as chapter 02 does.

A quantity argument left out. List.length takes its quantity first, so List.length(String, args) fails:

import Base

def main() -> IO(Unit):
  do IO<Unit>:
    args : List<String> <- IO.args()
    IO.print(Nat.show(List.length(String, args)))

- expected : Quant

Write List.length(&1, String, args), as chapter 09 does.

A destructured computed value. (a, b) = f(x) inside a definition is a match on a computed value (chapter 03).

A hole inside a branch. ?name stops the proof check and prints the goal (chapter 07).

A constructor field naming a later type. Chapter 02 shows the message.

Version differences

The index page is the table of contents. The table below compares the compiler installed for this tutorial, bend 2.0.25, with the 2.0.36 build the bend2.dev examples were checked against.

Two consequences for your workflow. First, the gate must read the output, not only the exit status, because 2.0.25 can exit 0 with an unsafe dependency. Second, bend update installs the latest compiler. The site's examples use 2.0.36, which has --verdict. The bend2.dev notes say that option needs Lean v4.34.0 exactly, or a prebuilt kernel named by BENDTT. Chapter 07 explains what the final check adds. This lab has neither the compiler option nor a Lean toolchain, so it has not run that check.

Reading an error

Every message has the same shape: a headline, then - expected and - observed lines, and sometimes a Location with the source around it. Read expected first. It names what the checker needed at that point, such as a defined name, Data, or cases for False. Then find the same spot in your file. The observed line shows what it found instead.

Next

Chapter 12 is the syntax reference, and chapter 13 is the glossary.

A.13 · bend-docs/src/content/tutorial/12-syntax-reference.md

Bend 2 tutorial 12: syntax reference · runnable · updated 2026-10-18 · canonical /tutorial/12-syntax-reference/

12: syntax reference

This page is the language on one sheet. Read sections 1 and 4 once, then use the tables as a lookup. Blocks marked bend are checked by the tutorial gate with bend 2.0.25. The table rows were also run with that compiler when this page was written, except the forms that section 13 lists as not run. Section 12 gives the checker's exact messages for the common mistakes.

1. The model

Three layers. Each one classifies the layer below it.

Types are terms, so a definition can return one. The guide splits a program in two. Live code runs. Dead code is types, erased arguments and proofs: the checker reads it, and the compiled program never runs it.

import Base

def twice(+n: Nat) -> Nat:
  Nat.add(n, n)

def identity(-A: Type, x: A) -> A:
  x

def main() -> Nat:
  identity(Nat, twice(3n))

6n

In that call, identity is code. Nat is an erased argument, so the compiled program never receives it. twice(3n) is a value computed at run time.

2. Declarations

import Base

type Box<a, -A: Kind(a)> is Kind(a):
  Box{value: A}

def unbox(a, -A: Kind(a), b: Box<a, A>) -> A:
  match b:
    case Box{value}:
      value

def main() -> U32:
  unbox(&1, U32, Box{7})

7

3. Marks and punctuation

• A name directly before braces makes a constructor. Braces with no name make an annotation (:), an equality (==), or a proof ({==}).
• No space goes between a constructor and its braces. Some{4n} is a constructor, and Some {4n} is rejected.
• Operators need a space on each side: a + b, not a+b.
• == appears only in types. Compare values with U32.is_eq(a, b).
• Signatures write IO(A) and Chan(A) with parentheses, and datatypes with angle brackets, as in Maybe<&2, Nat>. A do header takes angle brackets: do IO<Unit>:.

4. Kinds, quantities, and erasure

import Base

def replicate(-A: Data, n: Nat, +x: A) -> List<A>:
  match n:
    case 0n:
      Nil{}
    case 1n+p:
      x <> replicate(A, p, x)

def main() -> List<U32>:
  replicate(U32, 3n, 7)

[7, 7, 7]

import Base

def dup_k(-A: Kind(&2), +x: A) -> A & A:
  (x, x)

def main() -> Nat & Nat:
  dup_k(Nat, 6n)

(6n, 6n)

replicate mixes three kinds of parameter. -A is erased, n is affine, and +x is reusable because each step uses x twice. <> puts the head in front of the rest.

• A Type argument is written at the call: identity(U32, 42). Bend infers no type arguments (section 12).
• + needs Data. A function is a Type and cannot be copied, so pass a template ~f instead (chapter 03).
• An erased argument does not reach the compiled program. Compile the same program with -A and without it, and compare the C: the version without - passes the type in and drops it (chapter 03).

5. Types

import Base

def IsZero(n: Nat) -> Type:
  match n:
    case 0n:
      Unit
    case 1n+p:
      Empty

def needs_ne(e: {1n != 0n : Nat}) -> Nat:
  1n

def require_zero(n: Nat, e: IsZero(n)) -> Nat:
  n

def main() -> Nat:
  require_zero(0n, Unit{})

0n

import Base

def pick(b: Bool) -> U32 | Bool:
  match b:
    case True{}:
      Inl{4}
    case False{}:
      Inr{False{}}

def main() -> U32 | Bool:
  pick(False{})

Inr{False{}}

6. Terms and values

import Base

def inc(x: U32) -> U32:
  (x + 1 : U32)

def twice(~f: U32 -> U32, x: U32) -> U32:
  f(f(x))

def main() -> U32:
  twice(~inc, 40)

42

import Base

def value(r: Array<U32> & U32) -> U32:
  match r:
    case (array, item):
      item

def main() -> U32:
  a = [0 : U32*8n]
  a[9] <- 7
  value(a[1])

7

• A constructor takes its type from its context. In a let with no context, annotate it: +t = {Tok{3n} : Tok} (chapter 03).
• The braces after a constructor name hold its fields in a type (Segment{length: Nat}), its arguments in a term (Segment{3n}), and its binders in a pattern (case Segment{length}:) (chapter 02).
• There is no if. Branch with match on True{} and False{} (chapter 01).

7. Statements and matching

import Base

type Pt is Data:
  Pt{x: U32, y: U32}

def sum_pt(p: Pt) -> U32:
  Pt{x, y} = p
  (x + y : U32)

def swap(p: U32 & U32) -> U32 & U32:
  (a, b) = p
  (b, a)

def main() -> U32 & U32:
  swap((sum_pt(Pt{3, 4}), 0))

(0, 7)

• A recursive call must make a smaller argument. Arguments are read left to right, and each is passed unchanged until one of them is a smaller part. Otherwise the checker prints expected : a decreasing self-call (chapter 02).
• @unsafe turns that check off, and section 9 says what that costs.

8. Operators

import Base

def le(a: U32, b: U32) -> Bool:
  (a <= b : U32)

def main() -> U32 & U32 & U32 & U32 & Bool:
  ((6 .|. 1 : U32), (1 << 3n : U32), (8 >> 2n : U32), (7 % 2 : U32), le(3, 5))

(7, 8, 2, 1, True{})

• Each operator needs an annotation. (a + b : U32) covers the operators in its own parentheses. A call's arguments start a new group, so (U32.add(a + b, 1) : U32) is rejected (section 12).
• Braces annotate one term. {12 : U32} is fine, but {6 * 7 : U32} is rejected, so write (6 * 7 : U32).
• A bare operator is rejected. The guide says it means Nat, but 2.0.25 rejects it, so write (n + 1n : Nat).

9. Laws, proofs, and properties

A law is a claim, and a def of the same name is its proof. The proof of add_zero splits the cases of x, uses reflexivity in each, and rewrites with the induction hypothesis.

import Base

law add_zero:
  for x: Nat
  {Nat.add(x, 0n) == x : Nat}

def add_zero(x):
  match x:
    case 0n:
      {==}
    case 1n+p:
      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
      {==}

def main() -> Nat:
  Nat.add(42n, 0n)

42n

Properties the checker guarantees:

• A law with no def is an open claim. A hole is open too: ?TODO makes bend PROOF.bend print Error: 1 TODO found. and refuse the file.
• A false law fails the gate. The gate prints All terms check. only when every law has a proof that checks (chapters 07 and 15).
• A safe recursive def terminates, because each recursive call shrinks an argument (section 7). @unsafe is outside these guarantees, so no law may depend on it (chapter 08).
• A plain value is used at most once. A second use is an error, consumed more than once.
• An erased value is deleted before the program runs (section 4).
• A call computes its arguments first (section 11).
• Nothing is inferred, so type arguments, let types and operator types are written (section 12).

10. Effects and do

import Base

def greet(name: String) -> IO(String):
  do IO<String>:
    return "Hello, " ++ name

def main() -> IO(Unit):
  do IO<Unit>:
    text : String <- greet("Ada")
    n: U32 = (6 * 7 : U32)
    IO.print(text ++ " " ++ U32.show(n))

Hello, Ada 42

11. Evaluation: Bend is strict

• A compiled Bend program is strict: a call computes its arguments before its body runs. A native build of first(1n, spin(0n)), where spin loops forever and first ignores its second argument, did not finish under timeout 20. With 0n in place of spin(0n), it printed 1 at once.
• The checker does not show evaluation order. bend file.bend normalises a pure main, so judge the order with a native build under timeout.
• To keep work unevaluated, use one of three forms: a lambda (x => ...), whose body runs when it is applied; a template (~f), which is substituted at compile time; or data that eval interprets, as below.
• Parentheses and annotations delay nothing. Tail calls compile to loops, and the runtime has no C stack: each definition is a segment of a flat state machine, and a call is a jump (the guide; chapter 05).

import Base

type Expr is Data:
  Lit{n: Nat}
  Add{a: Expr, b: Expr}

def eval(e: Expr) -> Nat:
  match e:
    case Lit{n}:
      n
    case Add{a, b}:
      Nat.add(eval(a), eval(b))

def twice(~f: U32 -> U32, x: U32) -> U32:
  f(f(x))

def main() -> U32 & Nat & U32:
  later: U32 -> U32 = x => (x + 1 : U32)
  program : Expr = Add{Lit{2n}, Lit{3n}}
  (later(41), eval(program), twice(~(x => (x + 1 : U32)), 40))

(42, 5n, 42)

12. Rejected forms

Each row is a program the checker rejects. The message is the checker's own, and the right column is the fix.

13. Not run here

• Foreign effects (import "./e.c", import "./e.js") need host files. bend guide effects describes them.
• bend main.bend --publish, bend page.html -o dist, and import 0x<hash>/main.bend as P need the package hub or the web bundler.
• A working named rewrite %e@E : P, and a where binder whose claim reads its value out of the pair (section 12).
• GPU timing: the lab machine has no GPU, so ! runs on the CPU here.
• The a <&> b quantity combinator, which the guide describes and this page does not run.

Next

Chapter 13 maps these terms onto Haskell and OCaml. Chapter 15 uses the forms from this page in one complete program.

A.14 · bend-docs/src/content/tutorial/13-glossary.md

Bend 2 tutorial 13: glossary for Haskell and OCaml programmers · docs-only · updated 2026-10-18 · canonical /tutorial/13-glossary/

13: glossary for Haskell and OCaml programmers

Each row says what a Haskell or OCaml programmer would reach for first, and what Bend 2 does with the same idea. The last column flags a difference that will change how you write code.

Concepts you already know

Terms specific to Bend 2

Affine. A binder used at most once. Dropping it is free. Chapter 03.

Strict. Compiled Bend computes a call's arguments before the body runs. To keep work unevaluated, use a lambda, a template, or data that an interpreter runs. Chapter 12, section 11, shows all three.

Quantity. The number of uses a binder may have: &1 means at most once, and &2 means reusable. The binder markers choose one: +x is reusable, x is used at most once, and -x is erased, existing only for the checker. Chapter 03.

Kind. A classifier of types that carries a usage budget, written Kind(q), where q is a quantity. Type is Kind(&1): its values are used at most once. Data is Kind(&2): its values may be copied with +. A kind is not a quantity. The quantity is the count, and the kind is the classifier that carries it. Haskell's kinds are different; see the table below. Chapter 03.

Constructor (ctor). A named way to build a value of a type. Segment{3n} applies the constructor Segment to 3n. Chapter 02.

Term and value. A term is an expression as written, such as (6 * 7 : U32). Its value is what it computes to, 42. Chapter 12, section 11.

Annotation. (e : T) gives the type of an expression, and {t : T} gives the type of one term. An operator needs parentheses. Chapter 01.

Erased (-). A binder that exists only for the checker. The compiler deletes it, so it is not a run-time argument. Chapter 03.

Runtime use. The compiled body needs the binder's value: it returns the value or computes with it. An erased binder cannot be used at run time. Chapter 03.

Explicit type argument. Bend infers almost nothing, so a type is passed at the call, as in identity(U32, 42). Chapter 03.

Closure. A function value, such as x => (x + 1 : U32). It is affine, so it may be called once. Chapter 03.

Array literal. [v : T*n] or [v : T^d]: a fill value v, an element type T, and either n slots (a power of two) or 2^d slots. Array.new(T, d, v) builds the same array. Chapter 03.

Law. A claim checked by the compiler. A law has a same-named proof def. Chapter 07.

Proof. A definition whose type is a law's claim. Chapter 07.

Curry-Howard. A law is a type, and its proof is a program of that type. Chapter 07 shows what the gate checks beyond the type.

{==}. Proves an equality when both sides compute to the same term. Chapter 07.

Rewrite %e : P. Replaces the goal using the equation e, with _ marking where the right-hand side goes. Chapter 07.

Hole. ?TODO leaves a goal open, and ?name prints the goal. Chapter 07.

exs. A law that asks for a witness; the proof returns it with the equation. Chapter 07.

Unit and Empty. Unit has one value. Empty has none, so a function that takes an Empty need only match nothing. Chapter 08.

Dependent type. A type computed by a def from a value, such as IsZero(n) or Vec(A, n). A normal type such as U32 has no parameters, and a function type such as U32 -> U32 maps values to values. Chapter 08.

Pure (return). return v in a do block boxes a pure value as an effect. It is IO.pure. Chapter 09.

Bind (<-). Runs an effect and names its result with a type. It is IO.bind. Chapter 09.

IO value. An effect of type IO(A). It has no constructors, so only <- opens it. Chapter 09.

Totality. Every safe recursive call shrinks its first changing argument. Chapter 02.

Fuel. A Nat argument that bounds a loop the outside world stops. Chapter 02.

@unsafe. A definition exempt from the termination check and outside the proof guarantees. Chapter 08.

Parallel call. a b = f(x) g(y), two calls the compiler may run at once. Chapter 05.

Bang. f!(x), the call on the GPU, with its parallel calls. Chapter 05.

Balanced fork. A parallel call whose halves do about the same work. Chapter 05.

Leaf. A tail loop over 8 to 64 items that runs on one core. Chapter 05.

Thread count. The --threads N setting of a native binary. It defaults to the CPU count, and the fastest value depends on the program, the input, and the machine, so measure it. Chapter 05.

term_keep, ctr_take, rfc_seal. Runtime names for reference counts in the emitted C. Chapter 05.

BendRT. The runtime that compiles Bend to flat C with affine ownership and balanced forks. Chapter 04.

Interaction net. A graph of cells rewritten by local rules. Chapter 04.

Cell and port. A cell has a symbol, one principal port, and auxiliary ports. Chapter 04.

Active pair. Two cells joined at their principal ports. Only these reduce. Chapter 04.

Confluence. Distinct active pairs commute, so the order does not change the result. Chapter 04.

CON, DUP, ERA. The three symbols of Lafont's symmetric interaction combinators. Chapter 04.

Duplication (dup). ! &L{x,y} = t; body splits t into two uses, with label L. Chapter 14.

Superposition (sup). &L{a,b} holds two alternatives with label L. In a net it is a DUP cell with label L, read from the other side. The released Bend 2 parser rejects it. Chapter 14.

Label. The number on a &L{} or ! &L{}. Equal labels pair superpositions, and different labels commute. Chapter 14.

Interaction Calculus (IC). Victor Taelin's text notation for labelled nets: λ, application, duplication, superposition, and erasure. Chapter 14.

Collapse. Rewrites a result so that no superposition or duplication remains inside its alternatives (ic run FILE -C). Chapter 14.

SupGen. Victor Taelin's program synthesizer, built on superposition search. Its source is not published, and released Bend 2 does not include it. Chapter 14.

Homoiconic. Code that is also data the program can build and inspect. Chapter 10 shows a limited form.

Gate. bend PROOF.bend. It passes only when every law is proved, with no holes and no unsafe dependency. Chapter 07.

Terms that look alike but differ

Next

Return to the table of contents in the index.

A.15 · bend-docs/src/content/tutorial/14-superposition-and-supgen.md

Bend 2 tutorial 14: superposition, collapse, and SupGen · runnable · updated 2026-10-18 · canonical /tutorial/14-superposition-and-supgen/

14: superposition, collapse, and SupGen

This chapter is the one place in the tutorial where the code does not run on bend. It runs on the Interaction Calculus (IC), the calculus behind the sup and dup of chapter 06. Victor Taelin's reference implementation runs it on a CPU. Every IC program below was run with that binary, and the lines under each program are its real output.

What is verified here, and what is quoted

• Verified in this lab: the rules, labels, and collapse results below, with their outputs and interaction counts (WORK). Reference build: Interaction-Calculus at commit e9f0185, default branch, CPU mode.
• Quoted, not re-run: the search results for SAT and program synthesis, the enumerator counts, and every SupGen claim. Each one names its gist or post.
• Not verified: wall-clock time and memory. The binary reports interaction counts and its own timing, and the timing does not compare across machines.

Build the reference implementation

git clone https://github.com/VictorTaelin/Interaction-Calculus.git
cd Interaction-Calculus && make
IC_BIN="$PWD/bin/ic" python3 bend-docs/scripts/check-tutorial.py bend-docs/src/content/tutorial

The checker runs ic blocks only when IC_BIN is set, and reports them as skipped otherwise.

The calculus in six forms

Labels are numbers. The grammar is the one in the calculus's README.

One program per rule

Each program is followed by the lines the binary prints. WORK is the number of interactions.

APP-LAM: beta reduction is one interaction.

(λx.x λy.y)

λ$a.$a
WORK: 1 interactions

APP-SUP: applying a superposition runs both alternatives.

(&0{λx.x,λy.y} λz.z)

&0{λ$a.$a,λ$b.$b}
WORK: 5 interactions

The argument λz.z is duplicated, so each alternative gets its own copy.

DUP-SUP, same label: the duplication routes the parts.

!&0{x,y}=&0{λa.a,λb.b}; (x y)

λ$a.$a
WORK: 2 interactions

DUP-SUP, different labels: the two commute.

!&0{x,y}=&1{λa.a,λb.b}; (x y)

&1{λ$a.$a,λ$b.$b}
WORK: 9 interactions

DUP-LAM and the erasures.

!&0{x,y}=λz.z; (x y)

λ$a.$a
WORK: 3 interactions

(* λx.x)

*
WORK: 1 interactions

!&0{x,y}=*; (x y)

*
WORK: 2 interactions

Labels: same routes, different commute

The README says a superposition "works like a pair", and a duplication of a superposition "works exactly like a pair projection" when the labels match. The two DUP-SUP programs show both cases. With equal labels the duplication takes the pair apart, and the 2 interactions are routing and the final application. With different labels the duplication cannot route the alternatives, so it duplicates each one. The superposition comes out with label 1, at a cost of 9 interactions.

Labels also decide which alternatives are paired when two superpositions meet. The next program is the AND function applied to two boolean superpositions. True is λt.λf.t, False is λt.λf.f, and (a b F) computes AND. First, with different labels:

((λa.λb.(a b λt.λf.f)) &0{λt.λf.t,λt.λf.f} &1{λt.λf.t,λt.λf.f})

&0{&1{λa.λb.a,λc.λd.d},λe.λf.f}
WORK: 18 interactions

Next, with the same label on both inputs:

((λa.λb.(a b λt.λf.f)) &0{λt.λf.t,λt.λf.f} &0{λt.λf.t,λt.λf.f})

&0{λa.λb.a,λc.λd.d}
WORK: 12 interactions

Equal labels pair the alternatives: the first of one input meets the first of the other, so the result has two leaves, True and False. Different labels give every combination, and AND throws away the cases that do not matter. When the first input is False, AND never looks at the second, so the second superposition is erased in that branch. The result has three leaves. Labels and erasure, not just the function, decide the shape of the answer.

How this sits on interaction nets

The calculus uses the same three cells as chapter 04, and gives every DUP a label. Read the text as cells:

The rules are chapter 04's, with labels on the DUP cells. The counts are the ones the binary printed above:

A superposition is not a new kind of cell. It obeys the rules of a DUP with its label: it commutes with an application, annihilates with a duplication of the same label, and commutes with a duplication of another label. The README says a superposition "works like a pair". That describes what the cell holds, two alternatives. The cell itself is a DUP read from the other side (chapter 04 draws both readings).

With equal labels, the two cells meet at their principal ports and annihilate. Each aux wire goes straight through, so x is wired to a and y to b:

    x         y
    │         │
  ┌─┴─────────┴─┐
  │  DUP   L0   │
  └──────┬──────┘
         │          principal ports meet: annihilate
  ┌──────┴──────┐
  │  SUP   L0   │
  └─┬─────────┬─┘
    │         │
    a         b

A superposition is born in DUP-LAM. A duplication that meets a lambda copies the lambda, and the lambda's variable becomes &L{X0,X1} with the duplication's own label L. The two copies of the variable are the alternatives, and the body is duplicated behind them. The count fits this reading: !&0{f,g}=λx.x; f takes 2 interactions, one DUP-LAM and one annihilation of the body's copy with the same label. A different label would commute instead, and take more steps.

The README also notes that without labels the system cannot clone pairs, or clone a cloned lambda. The labels are what let the net copy a superposition. None of this runs in Bend 2; the reference binary runs it.

Collapse: from superpositions to plain results

The reference binary has a collapse mode. ic run FILE -C rewrites a result so that no superposition or duplication remains inside its alternatives. The outermost superposition stays, and each alternative is a plain term. The first program in the previous section already shows this: its output is a tree of plain λ-terms, with the labels kept only at the top.

Search by superposition, with erasure as the filter

A selector turns a result into a filter. The selector λr.(r A *) returns A when r is True, because True takes its first argument, and erases everything else when r is False. Applied to the AND of the two superpositions, it keeps exactly the input pairs for which AND is True:

((λa.λb.((λr.(r λx.λy.x *)) (a b λt.λf.f))) &0{λt.λf.t,λt.λf.f} &1{λt.λf.t,λt.λf.f})

&0{&1{λa.λb.a,*},*}
WORK: 37 interactions

One alternative survives: A for the single pair (True, True). Every other alternative is erased to *. This is search in its smallest form. The program is written once, the candidates are a superposition, and erasure keeps only the candidates that pass the test. The SAT note calls this "search without loops". The search does no enumeration in the program text, and the filter does the selection.

Exercise: keep the False cases

The selector λr.(r * A) keeps A when r is False, because False takes its second argument. Predict how many alternatives survive, before you run the program below.

Solution: two, not three. The pairs (False, True) and (False, False) reach the same branch of AND, and that branch never uses the second input. So the second superposition is erased in that branch, and only one alternative is produced there. Counting alternatives counts the results that reach the output, not the assignments you might expect.

((λa.λb.((λr.(r * λx.λy.x)) (a b λt.λf.f))) &0{λt.λf.t,λt.λf.f} &1{λt.λf.t,λt.λf.f})

&0{&1{*,λa.λb.a},λc.λd.c}
WORK: 37 interactions

Exercise: predict the label

Predict the label of the result of !&0{x,y}=&1{λa.a,λb.b}; (x y), and the number of interactions. Then run it.

Solution: the label is 1 and the count is 9. The duplication has label 0 and the superposition has label 1, so they commute, and the result is a superposition with label 1.

!&0{x,y}=&1{λa.a,λb.b}; (x y)

&1{λ$a.$a,λ$b.$b}
WORK: 9 interactions

Search in the published material

The author's public work applies the same idea to larger problems. These results are quoted, not re-run here.

• Program search, add-carry (gist fast_dps_add_carry, updated July 2026). A template with 16 unknown bits is written once, its candidates are superposed, two test cases are applied, and the result is collapsed. The gist reports about 36 thousand interactions for the search, against about 262 million for 65,536 separate runs of a conventional loop. It is written in HVM1 syntax. The author says the full source will not be released.
• SAT (gist sat.md, 2024). Each boolean is a superposition of True and False, a formula is applied to all assignments at once, and the result is collapsed. The gist's text reports 3 minutes in Rust against 1 second in HVM for a 32-variable instance, but the code in the gist is a 16-variable instance. The author writes that he knows little about the asymptotic behaviour.
• Enumerating λ-terms (gist superposed_lambda_calculus_evaluator.c, 2025). The enumerator builds affine λ-terms directly as a superposition of constructors such as #Lam and #App, so the candidate programs are data. The gist reports about 76 thousand interactions for an untyped search, against about 32 million for a naive enumerator, and about 3 thousand for a dependently typed version. Its header says it mirrors a file in HVM3's book. That path returned HTTP 404 when this chapter was checked, so the mirror was not confirmed.

SupGen: what is public

SupGen is the synthesizer these techniques were built for. Its source is not public. The evidence:

• The DPS gist says: "We'll not release the full source, but, meanwhile, I can talk about the theory." It also says HOC "will soon (EOY?) launch an API for our DPS solution".
• A 2025 HOC thesis gist says: "SupGen, our program synthesizer that outperformed existing solutions by up to 1000x." That is a claim, and no code accompanies it.
• A post surfaced by web search, which I did not open, says SupGen "could only discover functions when given their type signatures" until a breakthrough. A YouTube demo is titled "SupGen: an AI-free code synthesis tool". Neither was checked against source.
• Taelin's GitHub account lists 261 public repositories, and none is named SupGen. HigherOrderCO's public repositories are Kind, HVM1 to HVM4, Bend1, and Bend2, which now lives at bendlang/bend. Other GitHub repositories named supgen are unrelated, except BabySupGen, a browser playground that describes itself as inspired by the research.
• The tutorial's own notes agree. The release-status note lists "Bend2–SupGen integration" among the launch blockers, and the HVM runtime note calls the integration "still private".

So the mechanism is public: the calculus, its labelled rules, collapse, and the examples above. The synthesizer is not.

Is a cheap fork of running code available?

Partly, and only inside the calculus.

• Yes, as alternatives inside one term. A fork of a function can be written as a superposition of two versions. Applying it to an input runs both versions, and the input is shared through a duplication. In the program below the main version is the identity, and the branch is NOT. One run returns both answers:

(&0{λx.x,λx.(x λt.λf.f λt.λf.t)} λt.λf.t)

&0{λ$a.λ$b.$a,λ$c.λ$d.$d}
WORK: 8 interactions

The result &0{True, False} holds the main version's answer and the branch's answer side by side.

• Limits. The fork is an alternative inside one term. It is not a copy of a running process with its own memory. Its cost is counted in interactions, which is the author's metric. Memory and wall-clock time were not measured here, and the speedups quoted above are interaction counts.
• No, in released Bend 2. The compiler rejects &{a, b} (chapter 06), and BendRT does not reduce nets (chapter 04). A Bend program compiles to a fixed binary, and a branch is a second definition that you test with laws (chapter 10).
• The homoiconic angle. The enumerator builds programs as data, using constructors such as #Lam. That is the closest public thing to code that other code can build and inspect. Released Bend 2 has no such representation. Chapter 10 shows a small Expr interpreter in Bend, which is a limited form of it.

What to watch for

• A Bend release that adds sup syntax or the SupGen integration. The search note in the tutorial's notes says to re-read it when SupGen ships.
• A published SupGen source or API. Until then, every SupGen claim in this chapter is a quoted claim.
• An HVM4 or IC release that reports wall-clock results on the programs above. The interaction counts here do not give those numbers.

Next

Chapter 13 is the glossary. Chapter 10 applies the fork idea to Bend's laws-first workflow.

A.16 · bend-docs/src/content/tutorial/15-capstone.md

Bend 2 tutorial 15: capstone, a checked command parser · runnable · updated 2026-10-18 · canonical /tutorial/15-capstone/

15: capstone, a checked command parser

This chapter builds one small program from the parts of the tutorial. It reads commands from the command line, moves a job through states, and proves properties of the transitions. The laws are the specification, and the gate checks that the code meets them.

The project has three files in one directory:

• job.bend: the program. Pure code comes first: types, a codec, and the transition function. The IO shell main comes last.
• LAWS.bend: the claims. A person writes them, and nobody edits them to make a proof pass (chapter 07).
• PROOF.bend: one proof per law. bend PROOF.bend is the gate.

1. The three files

job.bend

import Base

type Cmd is Data:
  Start{}
  Cancel{}
  Finish{}

type State is Data:
  Queued{}
  Running{}
  Cancelled{}
  Finished{}

def encode(c: Cmd) -> String:
  match c:
    case Start{}:
      "start"
    case Cancel{}:
      "cancel"
    case Finish{}:
      "finish"

def only(hit: Bool, c: Cmd) -> Maybe<&2, Cmd>:
  match hit:
    case True{}:
      Some{c}
    case False{}:
      None{}

def decode(+s: String) -> Maybe<&2, Cmd>:
  Maybe.or(&2, Cmd, only(String.eq(s, "start"), Start{}), Maybe.or(&2, Cmd, only(String.eq(s, "cancel"), Cancel{}), only(String.eq(s, "finish"), Finish{})))

def step(+s: State, c: Cmd) -> State:
  match s c:
    case Queued{} Start{}:
      Running{}
    case Queued{} Cancel{}:
      Cancelled{}
    case Running{} Cancel{}:
      Cancelled{}
    case Running{} Finish{}:
      Finished{}
    case _ _:
      s

def state_name(s: State) -> String:
  match s:
    case Queued{}:
      "queued"
    case Running{}:
      "running"
    case Cancelled{}:
      "cancelled"
    case Finished{}:
      "finished"

def run1(m: Maybe<&2, Cmd>) -> IO(Unit):
  match m:
    case Some{c}:
      IO.print(state_name(step(Queued{}, c)))
    case None{}:
      IO.die(Unit, 2, "unknown command")

def run2(m: Maybe<&2, Cmd>, n: Maybe<&2, Cmd>) -> IO(Unit):
  match m n:
    case Some{c} Some{d}:
      IO.print(state_name(step(step(Queued{}, c), d)))
    case _ _:
      IO.die(Unit, 2, "unknown command")

def dispatch(args: List<String>) -> IO(Unit):
  match args:
    case Nil{}:
      IO.print("usage: job CMD [CMD]")
    case Con{a, Nil{}}:
      run1(decode(a))
    case Con{a, Con{b, Nil{}}}:
      run2(decode(a), decode(b))
    case _:
      IO.die(Unit, 2, "too many commands")

def main() -> IO(Unit):
  do IO<Unit>:
    args : List<String> <- IO.args()
    dispatch(args)

Read the file from the top. encode and decode are inverses: encode writes a command as a string, and decode reads it back and returns a Maybe. step is the transition function, and every pair it does not list leaves the state unchanged. dispatch takes one or two commands, and main passes it the arguments. Each helper is defined above the function that uses it, so the file has no forward references (chapter 02).

LAWS.bend

import Base
import ./job.bend as J

law round_trip:
  for c: J.Cmd
  {J.decode(J.encode(c)) == Some{c} : Maybe<&2, J.Cmd>}

law finished_stays:
  for c: J.Cmd
  {J.step(J.Finished{}, c) == J.Finished{} : J.State}

law start_then_cancel:
  {J.step(J.step(J.Queued{}, J.Start{}), J.Cancel{}) == J.Cancelled{} : J.State}

round_trip says that every command survives encoding and decoding. finished_stays says that a finished job stays finished, whatever command arrives. start_then_cancel is a concrete claim that needs no case split: starting and then cancelling a job cancels it.

PROOF.bend

import Base
import ./job.bend as J
import ./LAWS.bend as Laws

def Laws.round_trip(c):
  match c:
    case J.Start{}:
      {==}
    case J.Cancel{}:
      {==}
    case J.Finish{}:
      {==}

def Laws.finished_stays(c):
  match c:
    case J.Start{}:
      {==}
    case J.Cancel{}:
      {==}
    case J.Finish{}:
      {==}

def Laws.start_then_cancel():
  {==}

All terms check.

PROOF.bend imports job.bend, so the gate also type-checks the program's main. Every proof here is a case split with {==} in each case, because each case computes to the same term on both sides.

4. Run it

The program is a command-line tool. These are the results of running it:

bend job.bend start
bend job.bend start cancel
bend job.bend start finish
bend job.bend
bend job.bend bogus
bend job.bend start bogus cancel

running
cancelled
finished
usage: job CMD [CMD]
unknown command        (exit status 2)
too many commands      (exit status 2)

5. Break it on purpose

Each exercise has an answer that was checked by running the gate.

1. A broken encoder. Change the "cancel" string in encode to "start". Predict the gate's first message.

   Answer: the gate fails in LAWS.round_trip:

   - expected : Some{job.Start{}}
   - observed : Some{job.Cancel{}}
   

   round_trip catches the bug because the claim names the behaviour that broke.

2. A gap the laws do not cover. Restore the encoder. Change step so that Queued plus Cancel stays Queued. Run the gate.

   Answer: the gate still prints All terms check. No law mentions that pair, so the broken transition passes. The laws are the specification, and the gate proves only what they say.

3. Close the gap. Add this law to LAWS.bend and this proof to PROOF.bend:

   law cancel_queued:
     {J.step(J.Queued{}, J.Cancel{}) == J.Cancelled{} : J.State}
   
   def Laws.cancel_queued():
     {==}
   

   Answer: the gate fails until step is fixed. It reports expected : job.Queued{} and observed : job.Cancelled{} at LAWS.cancel_queued. Restore Cancelled{} in step, and the gate passes again.

What to take away

A law names a behaviour, and the gate checks it. Passing the gate says nothing about behaviour that no law names. Write the claim first, keep it fixed, and let the proof change to match the code, not the reverse (chapter 07).

Next

Chapter 16 maps the repositories that assemble these pieces into real programs, and says which files to read first.

Continue to chapter 16.

A.17 · bend-docs/src/content/tutorial/16-references.md

Bend 2 tutorial 16: reading real Bend repositories · docs-only · updated 2026-10-20 · canonical /tutorial/16-references/

16: reading real Bend repositories

The tutorial teaches one idea per page. A repository teaches the next thing: how the pieces are arranged when the program is larger than one screen. The useful question is not which repository is biggest. It is where the boundary between pure code, effects, proofs, and measurement sits, and whether that boundary is visible in the file tree.

This chapter maps repositories worth reading. The list is not a ranking and it is not official. Each entry says what the repository demonstrates and which files to open first.

Core insight. A Bend repository is readable when its claims, its pure code, its effects, and its evidence live in separate places. Most of the repositories below differ in size, not in that shape.

The shape of a Bend repository

A small repository usually looks like this:

repo/
  README.md          the pinned compiler, how to run it, what it proves
  LAWS.bend          the claims, written by a human
  PROOF.bend         one same-named def per law
  main.bend          the entry point
  src/               pure domain modules
  tests/             golden files, unit tests, differential tests
  bench/             measurements, with the machine and version recorded
  host/ or *.c/*.js  foreign effects, kept at the edge

Larger repositories repeat the pattern per package or per layer:

repo/
  package-a/
    LAWS.bend
    PROOF.bend
    check.bend       runtime checks for the parts the checker cannot reach
    VERSION          the hub version, independent of its neighbours
    package-a.bend
    bench/
  package-b/
    ...

Not every repository has every row. A package with no effects has no host/. A teaching example may put everything in one file. What matters is that you can tell which row a file belongs to.

How to read one

Read in this order, and stop when you can predict the next file:

1. README. Find the compiler version. Bend 2 changes between releases, and a repository that pins 2.0.37 may not check on 2.0.25. Find the command that runs the proof gate.
2. LAWS.bend. Read the claims before the implementation. They tell you what the author thinks the program means.
3. PROOF.bend. Look at the shape of a proof, not every line: {==}, a rewrite, an induction hypothesis, or a call to a lemma.
4. The entry point. Find main, the CLI, or the test driver. Trace one path from it into one leaf module.
5. One leaf module and its test. This is where the writing style lives: how types are annotated, how matches are ordered, how effects are avoided.
6. The build and the benchmark. Check whether the numbers name the compiler, the thread count, and the machine. A number without those is an anecdote.

Useful questions to carry from repository to repository:

• Does PROOF.bend import the adjacent LAWS.bend? Without that import, the laws you read are not the ones the proof file proves.
• Is check.bend testing the same behaviour as the laws, or something the checker cannot express?
• Are foreign effects behind a small named module, or scattered through the domain code?
• Does the benchmark compare against another implementation, or only against itself?
• Does the README say what the repository does not prove?

A short reading list

The community repositories

metal-bending: the smallest complete project

Repository: AdrielSantana/metal-bending · Browser walkthrough: adrielsantana.github.io/metal-bending

A playground on Apple Silicon with seven single-concept examples, six graphics programs, and a working proof gate. The README is in Portuguese; the code is the common language.

Read it for: the smallest repository that still has the full shape. Each example is one file, and each file is one idea: 01_hello.bend for do, 02_types.bend for type ... is Data, 03_recursion.bend for terminating recursion, 04_parallel.bend for the fork shape, 05_arrays.bend for one-owner arrays, 06_io.bend for IO.fork and channels, 07_monads.bend for do over Maybe.

Start at: examples/02_types.bend, then LAWS.bend. The file opens with add_zero and append_nil from Base, then states total_cons about the repository's own src/math.bend. That is the progression the tutorial describes: prove a Base fact, then prove a fact about your code. gfx/01_mandelbrot.bend is the same language doing a GPU-shaped loop in a window.

Composition lesson: one concept per file, one claim per law, and a gate the README shows failing as well as passing. The gfx/ directory is separate from examples/ because rendering is a different concern with a different driver.

bend-voxel: an engine, an app, and acceptance scripts

Repository: aivv73/bend-voxel

A voxel engine with destructible environments and a native window. The repository separates the editable body (voxel.bend), the renderer (render.bend), lighting (lighting.bend), materials (material.bend), and the DDA traversal (dda.bend) from the application shell (atelier.bend, main.bend).

Read it for: acceptance checks written in Bend rather than in a separate test framework. scripts/reference_check.bend, scripts/lighting_check.bend, scripts/material_check.bend, scripts/image_check.bend, and scripts/ui_check.bend are programs that compare complete outputs: cell sets, sun-depth texels, material exports, and CPU/GPU images. The docs/ directory keeps the evidence, including the raw TSV and log files behind the DDA comparison.

Start at: LAWS.bend for the material and geometry invariants, then voxel.bend and dda.bend. Then read scripts/reference_check.bend to see how a test is just another Bend program with an exit condition.

Composition lesson: the engine is a library of pure modules, and every executable is a thin driver. The Makefile exposes make test, make geometry, make lighting, make materials, and make images so each layer of evidence can be run alone.

bend-craft: a deterministic game core

Repository: costamatheus97/bend-craft

A block world with terrain, a first-person player, and a per-pixel voxel ray tracer. The whole game is U32 fixed point, so a run is a function of its seed and input log, and every frame is the same bytes on JavaScript, native C at one or many threads, and the GPU.

Read it for: the cleanest small example of the pure-core pattern. world.bend is the world as one flat Array<U32> and its terrain generator. render.bend is the Amanatides-Woo DDA and four shading tiers. game.bend is a pure 60 Hz step plus render(state). play.bend is the only game file that reads a clock, a window, or a device; the benchmarks read them too.

Start at: the README's file list, then game.bend and play.bend side by side. The gap between them is the architecture. tests/world.bend, tests/render.bend, and tests/game.bend test the pure side; run_tests.sh runs them. bench/ holds the scripts that produced the README's numbers, and LOG.md and OPTIMIZATIONS.md record what was tried and rejected.

Composition lesson: determinism is a design constraint, not a test added later. Keeping time and I/O in play.bend is what lets the same step run in a benchmark, a replay, and the window.

bendoom: a large port, decomposed

Repository: eliesgalvira/bendoom

Doom's first level, E1M1, written in Bend 2. The README carries a "SLOP WARNING" and says there was no adult supervision of the code. Treat that as a warning about style, not about usefulness: the decomposition is the lesson.

Read it for: how to port a large C program without turning it into one file. src/ has one module per concern: wad.bend for the archive, bsp.bend for the level tree, render.bend, sim.bend, things.bend, sprites.bend, sfx.bend, opl.bend, and music.bend. doom.bend is the game driver; film.bend replays a demo to video; tests/ mirrors the module list with one test file per subject.

Start at: LAWS.bend, which states byte, WAD, key, sound, and simulation invariants, then src/bytes.bend and src/sim.bend. Read nix/proof.nix and nix/tests.nix to see how the proof gate and the test matrix are wired into CI.

Composition lesson: a port is a set of named modules plus a reference oracle. tools/oracle.nu compares frames against Chocolate Doom, so the port has an external definition of correct, not just an internal one.

elpis-fast: spec, laws, proof, diff

Repository: gildrb/elpis-fast

A 4-bit quantized Qwen inference engine with decode and prefill kernels, measured on one RTX 3090. It is dense and specialized; read it for the unit of work, not for a general application layout.

Read it for: the spec/laws/proof/diff discipline around each optimized kernel. A kernel such as attn_chunk has attn_chunk.bend, attn_chunk_spec.bend, attn_chunk_laws.bend, attn_chunk_proof.bend, and attn_chunk_diff.py. The .bend file is the fast implementation, _spec is the reference definition, _laws states their relationship, _proof proves it, and _diff compares against a trusted implementation. The *_TABLE.bend files are decision tables for scheduling and attention shapes.

Start at: LAWS.bend and PROOF.bend at the root, then one kernel family from the README table. The repository's "What fast means" section is as important as the code: a speedup is kept only if the output is unchanged or passes a named quality gate, and each gate records thresholds set before the runs.

Composition lesson: performance work is not exempt from specification. The spec stays readable, the optimized kernel stays fast, and the proof plus the differential test connect them.

bend-collections: a library with specs and proofs

Repository: Giulio2002/bend-collections

Containers and cryptographic primitives in stock Bend, benchmarked against optimized C implementations of the same algorithms. The README has a table of containers and another for SHA-256, Keccak, BLAKE, AES-GCM, Argon2id, and the other crypto modules.

Read it for: how a real library separates the public module, the specification, and the proof. src/containers/ holds the implementations (dynamic_array.bend, deque.bend, balanced_search_tree.bend, hash_table.bend, lru.bend). spec/ holds reference definitions, proofs/ holds the proof modules, and the root laws.bend, laws_containers.bend, laws_crypto.bend, and laws_math.bend group the claims by area. benchmarks/bend/ runs the same workloads as the native C baselines.

Start at: src/containers/deque.bend and its proof under proofs/containers/, then laws.bend. The cryptographic modules show the same shape at a larger scale: a specification, a proved equality, and published test vectors.

Composition lesson: a container is not "done" when it works. It is done when its invariants have a specification, a proof, and a measurement against the implementation it replaces.

backplane: a large application in flat modules

Repository: i2cjak/Backplane

A large workspace for agentic hardware development, with deterministic KiCad and STEP viewers. It is a real product with a release process, not a sample.

Read it for: how a large Bend codebase stays navigable. src/core/ is a flat set of roughly 140 small modules named after one concept each: json.bend, codec.bend, semver.bend, sha256.bend, schematic.bend, pcb2d.bend, pcb3d.bend, model.bend, store.bend. src/app/ holds the view layer: main.bend, layout.bend, render.bend, viewer.bend, theme.bend, and one module per surface.

Start at: src/app/main.bend to see the entry point, then src/core/json.bend or src/core/codec.bend as a representative leaf. LAWS.bend and PROOF.bend sit at the root, so the proof gate covers the whole product with one command.

Composition lesson: flat names beat deep hierarchies when the names are specific. src/core is a vocabulary; src/app is a presentation of that vocabulary. Neither imports sideways for convenience.

bend-frontend: a checker with a typed output

Repository: ind-igo/bend-frontend

A composable frontend for full upstream Bend 2. It checks a program once and returns a typed, serializable Core.Program for a backend.

Read it for: the boundary between a language and its consumers. src/core.bend is the authoritative schema for the output. src/decode.bend turns upstream terms, patterns, declarations, and templates into that schema and rejects proof holes and missing LAWS imports. src/frontend.bend exposes Frontend.check and Frontend.or_die. src/wire.bend handles metadata numbers. src/cli.bend is a small driver. host/adapter.js and host/run.js attach the checker and I/O to the Bend process.

Start at: src/core.bend, then src/decode.bend, then src/LAWS.bend. The laws are about the output: bare_idempotent, missing_laws_rejected, complete_accepted, and metadata_overflow_rejected. That is a useful example of laws stated at an API boundary rather than about arithmetic.

Composition lesson: the IR is a schema, decoding is a pure step, the host adapter is the only JavaScript in the runtime path, and every backend consumes the same serializable value. ind-igo/bend-evm is a separate repository that does exactly that.

bend-packages: a map of the ecosystem

Repository: lilalittle/bend-packages

A curated, regularly refreshed overview of BendHub: top packages, source repositories, publishers, and an A–Z list. The snapshot in this chapter's sources lists 703 packages on 2026-10-19.

Read it for: finding the next repository. The README groups picks by purpose: verified math and proofs, tensors and autodiff, web and networking, tools, games. Each row names the hub package, the version, the source repository when one is public, and the import line.

Start at: the "Top picks" tables, then ALL_PACKAGES.md when you know the name you want. The README also explains the two import forms: a name and version such as bend-mathlib@0.7.3.0/nat.bend, which resolves to a content hash, and the raw hash form, which always resolves to the same code.

Composition lesson: packages are the unit of reuse. A repository that publishes several packages, such as bend-kit or bend-ml, shows how to keep each one independently versioned and independently proved.

Eight more repositories

These are the repositories I would open next. They are grouped by what they teach, not by stars.

bendlang/bend: the official source

Repository: bendlang/bend

The compiler, the Base library, the guide, the official demos, and the test suite. This is the authority the rest of the tutorial cites.

Read it for: guide/GUIDE.md, which bend guide prints; bend2/base.bend, which bend base prints; demos/ for complete programs; and tests/ for the exact syntax and error behavior the checker accepts. Read the official tests when a tutorial chapter and a community repository disagree.

Start at: guide/GUIDE.md, then bend2/base.bend, then one demo and the tests for the feature you are using. Do not copy from Base without checking the version: the standard library changes between 2.0.x releases.

Lulzx/bendc: a self-hosting compiler

Repository: Lulzx/bendc

A compiler for Bend 2, written in Bend 2, that compiles itself and reproduces its own output byte for byte. The README reports a bootstrap fixpoint and 80 tests passing under both stages.

Read it for: how to structure a compiler as passes. bendc.bend is the driver, check.bend the type checker, core.bend the shared representation, and boot.bend the bootstrap path. Each optimization or transformation has a matching proof file: LIT.bend with LITPROOF.bend, SUBST.bend with SUBSTPROOF.bend, INLINE.bend with INLINEPROOF.bend, DEAD.bend with DEADPROOF.bend. rt/ is the runtime, split by concern (bendrt.h, native.c, cc.c, gpu.h, hub.c).

Start at: bootstrap.sh, then bendc.bend and check.bend. Then read one small pass and its proof together. tests/ pairs its test programs with .out golden files, and tests/check/ is a numbered suite of checker errors.

Composition lesson: a compiler pass is a module with an input language, an output language, and a proof obligation. The proof file next to the pass makes that obligation visible.

paymog/bend-kit: packages with their own gates

Repository: paymog/bend-kit

A general-purpose library for Bend 2, split into packages such as bytes, bignum, collections, concurrency, crypto, json, http, and cache. Each package is published separately and has its own version.

Read it for: the package layout. The mature package directories contain LAWS.bend, PROOF.bend, check.bend, VERSION, the implementation (bytes.bend), and a bench/ directory. bytes/check.bend is especially useful: it says in a comment that the laws run in the checker, where Array is a tree of defs, while check.bend runs the same operations on the runtime's native array at sizes the checker would not reach. That is a precise statement of what each gate covers.

Start at: bytes/LAWS.bend, bytes/PROOF.bend, and bytes/check.bend, then the README's "Same type" section. It explains why a caller must import the same package version the callee imports: a different version is a different type.

Composition lesson: one package equals one name, one version, one proof gate, and one benchmark. Dependencies are pinned by name and hash, not floating.

nuxyel/bend-ml: dependent types in a library

Repository: nuxyel/bend-ml

Machine learning in Bend 2 with tensor shapes in the type. A mismatched matrix product does not compile; a reshape needs a proof that the element count is preserved. Six packages are published on BendHub, with an MNIST demo and a GPT-2 demo.

Read it for: how dependent types shape an API. tensor/ uses lists with Vec<n> and Mat<r,c>; tensor-array/ uses a flat Array<F32> with the same type-level sizes and a Bands<r,c> type for parallel matrix-vector work; autograd/ has a typed backward pass; bpe/ proves the tokenizer round trip; binary-read/ keeps foreign code out of the proved packages. demos/gpt2 and demos/mnist are the integration tests.

Start at: the README's two shape-error examples, then tensor-array/main.bend, then autograd/main.bend. Read the package README before the code: it names the package version, its laws, and its dependencies.

Composition lesson: put the invariant in the type when the type checker can carry it, and in a law when it cannot. The shape is checked at the boundary, and every layer after that is checked for any shape.

angerman/birc: a pure core with a thin foreign edge

Repository: angerman/birc

A terminal IRC client with a pure Bend core and a small C FFI for terminal rendering and POSIX sockets. The README reports more than 91% of the code in Bend, a zero-poll event loop, and a native DNS client.

Read it for: the actor-and-frame architecture. src/bend/irc.bend parses the protocol, frame.bend handles CRLF framing, client.bend and buffer.bend hold state, submit.bend builds outbound lines, view.bend lays out the screen, session.bend ties the pieces together, and actor.bend and net.bend do the I/O. src/ffi/ is the thin C layer, and src/ui/timui.h is the rendering library.

Start at: LAWS.bend for the protocol and client invariants, then src/bend/irc.bend and src/bend/frame.bend. The tests/pty/ directory is the part most projects skip: it drives the real terminal through a pseudo-terminal, including resize, paste, EOF, and UTF-8 split across reads.

Composition lesson: foreign code is acceptable when it is small, named, and at the edge. The domain stays testable because the protocol and state transitions are pure.

FabianVegaA/mylsm: a systems program with per-module laws

Repository: FabianVegaA/mylsm

An experimental durable LSM key-value store. It writes to a log, keeps sorted tables, recovers after a restart, and exposes byte and UTF-8 views of the same database.

Read it for: law files per module. src/ holds the storage modules (ByteWal.bend, Wal.bend, ByteMemTable.bend, SstFile.bend, and the rest), laws/ holds a matching file for each (laws/ByteWal.bend, laws/ByteMemTable.bend, and so on), and PROOF.bend imports them into one gate. app/cli/ and app/repl/ are separate applications over the same library. bench/smoke/, bench/crash/, and bench/workload/ cover ordinary paths, fault injection, and sustained runs.

Start at: laws/ByteWal.bend and src/ByteWal.bend together, then app/cli/main.bend. The README is unusually explicit about the limits: the laws cover pure decisions, not filesystem behavior, process locking, or the C and JavaScript host effects.

Composition lesson: a large systems program can keep its proof surface small by stating laws per module and importing them at the root. The app/ layer is a client of the library, not part of it.

bendlib/bendlib: lemmas and a law checker

Repository: bendlib/bendlib

A foundation library with bend-mathlib (published lemmas about Nat, Bool, List, String, Maybe, equality, and order) and lawcheck, a tool that looks for counterexamples before you try to prove a law.

Read it for: how to publish proofs as a library. packages/bend-mathlib/ has one module per subject (nat.bend, list.bend, bool.bend, maybe.bend, order.bend, sort.bend, perm.bend), an all.bend entry point, and a README with a lemma index. tools/lawcheck is the complement of the proof gate: it tests the law against the implementation and shrinks a failing input.

Start at: packages/bend-mathlib/README.md for the lemma index, then nat.bend for the style. Read the lawcheck section of the README before writing a new law; a false law is cheaper to find by testing than by attempting a proof.

Composition lesson: proofs are reusable when they are packaged like code. The all.bend facade keeps imports stable while the individual modules stay focused.

777genius/awesome-bend: the current index

Repository: 777genius/awesome-bend

A curated list for current Bend 2, explicitly not Bend 1. It tracks the latest release, the hub, the official compiler, packages, tools, demos, benchmarks, papers, and community links.

Read it for: discovery and release context. The list records the changes between 2.0.x releases and warns which packages may need a newer compiler. The catalog section links to generated indexes with search and filters, which are better than a static list when you are looking for a specific package.

Start at: the "Packages", "Demos", and "Benchmarks" sections. Then check the repository's "Last checked" date; a list is only as current as its snapshot.

Composition lesson: an index is part of the ecosystem. It tells you which repositories are maintained, which are experiments, and which compiler version each one expects.

More to explore

What to copy, and what not to

Copy these:

• The gate. LAWS.bend plus PROOF.bend at the root of the project, and a README command that runs it.
• The pure core. A domain module that takes values and returns values, with the clock, the window, the filesystem, and the network in a separate driver.
• The named effect. A .c or .js file behind one Bend signature, with the host boundary documented.
• The matching test. A tests/ file for each domain module, and a check.bend for the parts the checker cannot reach.
• The pinned version. The compiler version in the README, and the package version or hash in the import.

Do not copy these:

• A law that restates the implementation. A claim such as "for every x, f(x) == f(x)" passes and says nothing. A law should name a behaviour a caller relies on.
• A proof that hides a hole. A ?TODO or an @unsafe dependency makes the gate weaker. The tutorial's chapter 07 shows the messages.
• A benchmark without a baseline. A time in milliseconds with no machine, thread count, compiler version, or comparison is not evidence.
• Foreign code as a shortcut. If a .c file does the work, the Bend code is a wrapper, and the laws prove the wrapper, not the work.
• A repository wholesale. Bend 2 is moving. A repository pinned to 2.0.22 may use syntax that 2.0.37 rejects, and the reverse. Read its version first.

Versions and freshness

All repository links in this chapter were checked on 2026-10-20. The latest stable release named by awesome-bend on that date was Bend 2.0.37. The tutorial's own runnable blocks were checked with Bend 2.0.25, so a repository that requires a newer compiler may reject code that this tutorial accepts, and a repository that uses an older feature may need bend update or a pinned checkout.

When a repository and this tutorial disagree, the compiler in front of you decides. Run bend version, then run the repository's proof command. If the proof gate passes, read the code; if it fails, read the version notes before changing anything.

Next

Go back to the table of contents, or pick one repository and read it in the order above. The most useful next step is to take metal-bending's shape, add one law about your own code, and run the gate.

B.1 · bend-docs/src/content/learn/data-matching.md

Data and matching · docs-only · updated 2026-09-05 · canonical /learn/data-matching/

Data and matching

Data definitions and the many shapes of match: algebraic data types, records, maps, pattern matching, recursion, and folds.

Algebraic data types

Algebraic data types introduce constructor-shaped values such as Nat.

Records

Records (planned).

Maps

Maps (planned).

Pattern matching

The proofs sample matches Nat by constructors — brace-suffixed patterns, one arm per constructor:

def is_zero(n: Nat) -> Bool:
  match n:
    case Z{}:
      True
    case S{p}:
      False

Numeric matching works the same way (case 0: / case 1+d:, binding the predecessor).

Lambda match

Lambda match (planned).

Recursion

Recursion is ordinary self-call, as in the parallel sum.

Mutual recursion

Mutual recursion (planned).

Higher-order functions

Higher-order functions (planned).

Closures

Closures (planned).

Folds

Folds (planned).

The bend construct

The bend construct that gives Bend its name awaits the public compiler.

B.2 · bend-docs/src/content/learn/effects-targets.md

Effects and targets · docs-only · updated 2026-09-05 · canonical /learn/effects-targets/

Effects and targets

Effects stay on the CPU in typed do blocks; pure code may fly to the GPU or compile to C, JavaScript, and Python.

IO

Effects run on the CPU in typed do blocks (hello) — input, print, sequenced with <-.

Files

Files extend the same IO surface (planned).

Command-line arguments

Command-line arguments extend the same IO surface (planned).

Compiling to C

HVM4's ahead-of-time compiler targets native C (current runtime tooling).

Compiling to JavaScript

Bend2's JavaScript target is planned.

Compiling to Python

Bend2's Python target is planned. Flags, outputs, and the GPU story per target arrive with the toolchain — the one hard rule is already known: pure code may fly to the GPU, effects stay on the host.

B.3 · bend-docs/src/content/learn/first-programs.md

First programs · docs-only · updated 2026-09-05 · canonical /learn/first-programs/

First programs

Functions, bindings, branching, numbers, strings, tuples, lists, and imports — the first ten Bend2 concepts, in the order a new programmer meets them.

Functions

import Base

# Adds two numbers.
def add(a: U32, b: U32) -> U32:
  a + b

def main() -> U32:
  add(20, 22)

def names the function, parameters carry types, the return type follows the arrow, and the body is an expression — no return.

Let bindings

Tuple assignment splits two calls at once (the fork from parallelism). A single binding is the same shape:

def main() -> U32:
  x = 40 + 2
  x

Conditionals

Branching goes through match on numbers and constructors.

def describe(n: U32) -> U32:
  match n:
    case 0:
      0
    case 1+d:
      1

Booleans

Boolean constructors and operators (planned).

Numbers

Numbers are typed as U32, including successor-style matching with case 0: and case 1+d:.

def identity(n: U32) -> U32:
  n

Strings and characters

Strings concatenate with ++ and print through IO::print (see hello). Characters and escaping are planned.

Tuples

Tuples destructure in assignment position: a, b = f(x), g(x).

Lists

List syntax (planned).

Imports

import Base brings in the standard library, including IO.

B.4 · bend-docs/src/content/learn/gpu.md

Running on GPUs · docs-only · updated 2026-08-13 · verified 2026-09-05 · canonical /learn/gpu/

Running on GPUs

Bend2 runs a function on the GPU when the call carries !: sum!(24, 0) evaluates on the GPU where sum(24, 0) would use the CPU. The function is the parallel sum, unchanged — only main differs. That is the entire GPU programming model.

def main() -> U32:
  sum!(24, 0)

What the mark does

! chooses where a call evaluates, not how it parallelizes. The fork inside sum is ordinary divide-and-conquer recursion, identical on either device; the GPU just points its thousands of threads at the same graph. Kernels, grids, blocks, and device memory do not appear in the language — the one-line contrast with Mojo from the comparison.

What stays on the CPU

Pure code goes through !; effects stay on the host. Hello world runs its input and print in IO on the CPU — what flies to the GPU here is arithmetic with no IO in its type.

The backends

Metal and CUDA, built on HVM4. No public toolchain ships them yet, so this page carries no measured numbers; they arrive when a compiler does.

B.5 · bend-docs/src/content/learn/hello.md

Hello world · docs-only · updated 2026-08-13 · verified 2026-09-05 · canonical /learn/hello/

Hello world

Every Bend2 program starts at main. This one reads a name and prints a greeting — and in doing so shows how Bend2 handles effects: not as statements that happen, but as values of type IO that describe what to do.

import Base

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

Line by line

• import Base brings in the standard library, which supplies IO.
• def main() -> IO<Unit>: declares a function, Python-style, with the return type after the arrow. IO<Unit> is IO applied to Unit: a computation run only for its effects. (main need not be effectful — a pure program declares def main() -> U32 and returns a number.)
• do IO<Unit>: sequences effects in a block that names its type.
• name <- IO::input() runs an effect and binds its result; <- is "run and name the answer".
• IO::print("Hello, " ++ name) is the block's value. Strings concatenate with ++, library functions are reached with :: paths, # starts a comment.

Where effects run

On the CPU. GPU evaluation — marking a call with ! — is for pure functions; input and output stay on the host. That split is the whole story of the GPU page.

B.6 · bend-docs/src/content/learn/hvm-hands-on.md

HVM4 hands-on · runnable · updated 2026-09-05 · canonical /learn/hvm-hands-on/

HVM4 hands-on

This page is different from the Bend2 pages: everything here runs today. HVM4 is public, one C file, and the outputs below were produced by building it and running each snippet (gcc works; the README uses clang).

curl -sSL -o hvm.c https://raw.githubusercontent.com/HigherOrderCO/HVM4/main/src/hvm.c
gcc -O2 -o hvm hvm.c   # a few warnings, builds fine
./hvm file.hvm -s      # -s shows interaction/heap stats
./hvm file.hvm -s -C10 # -C collapses superpositions into separate results

First run: a function of two arguments

Books are @name = term lines; application is f(a, b) — never f a b (whitespace application is a parse error). Lambdas use λ:

@add = λa. λb. (a + b)
@main = @add(1, 2)
//3

Actual run: 3, 3 interactions, 23 heap nodes. Three interactions for 1 + 2 tells you the price model honestly: every step is graph surgery.

Superposition: one location, two values

@main = (&A{1,2} + 10)

Actual run (-C10): 11 then 12, 4 interactions, 13 nodes. Both values flowed through the same addition, sharing everything except the choice. Two corrections to the README here, found by running: the superposition needs a label (&A{…}, not &{…} — bare &{} is erasure), and there must be no spaces inside the braces.

Labels decide: annihilate or multiply

A duplication meeting a superposition with the same label extracts pairwise; with different labels it multiplies branches:

@main =
  !x&A = &A{1, 2};
  [x₀, x₁]
//[1,2]          -- one result, 1 interaction

@main =
  !x&A = &B{1, 2};
  [x₀, x₁]
//[1,1]
//[2,2]          -- two results, 5 interactions

Both verified by running. !x&A = v; body binds the two copies as x₀ and x₁ (subscripts required); [a, b] is list sugar.

Affinity: the compiler that says no twice

Variables may be used at most once. This fails:

@bad = λx. (x + x)   // PARSE/AFFINITY ERROR: x used twice

The fix is a cloned binder — & tells the parser to insert duplication:

@square = λ&x. (x * x)
@main = @square(5)
//25               -- verified: 3 interactions

Style rule from the primer, worth memorizing: dups are the expensive primitive, so arrange definitions as case-trees that avoid clones, and never apply an inline match (λ{...}(x)).

Fib, with a stopwatch

@fib = λ{
  0: 0
  1: 1
  λ&n. (@fib((n - 1)) + @fib((n - 2)))
}
@main = @fib(10)
//55

Actual run: 55, 760 interactions, 2512 nodes, 19.33M interactions/s on an ordinary CPU. 0:/1: switch on machine ints; the default arm names its binder (λ&n. — cloned, since n is used twice).

Pattern matching that actually parses

The primer's <>: list-cons pattern does not parse on current main (expected: name). Match the constructor explicitly:

@len = λ{
  []: 0
  #CON: λh. λt. (1 + @len(t))
}
@main = @len([1, 2, 3])
//3                -- verified: 16 interactions

[] is #NIL{} sugar and still works; Peano naturals use Nn sugar with 0n: / 1n+: arms. Where this guide deviates from upstream docs, the binary was the tiebreaker — every snippet above exited 0.

B.7 · bend-docs/src/content/learn/parallelism.md

Automatic parallelism · docs-only · updated 2026-08-13 · verified 2026-09-05 · canonical /learn/parallelism/

Automatic parallelism

Bend2 parallelizes ordinary recursion: split the work in two, and the runtime evaluates the halves concurrently. No pragmas, no threads, no scheduler in the program. The program below sums 2²⁴ numbers this way.

import Base

# Sums a range of numbers in parallel.
def sum(d: U32, i: U32) -> U32:
  match d:
    case 0:
      i
    case 1+d:
      a, b = sum(d, i*2), sum(d, i*2+1) # fork
      a + b

# Runs sum on the GPU, via `!`.
def main() -> U32:
  sum!(24, 0)

The fork

Bend2 forks where the data flow splits. a, b = sum(d, i*2), sum(d, i*2+1) starts both recursive calls, and nothing joins them until a + b needs both results. The calls share no state, so on the interaction-net runtime they are disjoint subgraphs — recall the model: disjoint pairs cannot conflict — and any idle core reduces either one without locks.

The match

Bend2 pattern-matches on numbers with a successor case. case 0: handles zero; case 1+d: matches anything ≥ 1, binding d to one less (shadowing the argument). A branch body is an expression — no return anywhere. The arguments are U32, 32-bit unsigned integers — full 32-bit range.

What it computes

Each call owns a block of 2ᵈ consecutive integers and splits it in half; at depth 0 the block is the single number i. So sum(24, 0) covers 0 through 16,777,215, for an exact total of 140,737,479,966,720 — which notably does not fit in a U32. Device selection (!) is a separate decision from parallelism; that is the GPU page.

B.8 · bend-docs/src/content/learn/proofs.md

Proofs · docs-only · updated 2026-08-21 · verified 2026-09-05 · canonical /learn/proofs/

Proofs

This page proves one fact end to end: addition commutes. If the previous page was the theory, this is the lab session — one theorem, one proof, every step shown. A Bend2 theorem is an assert block, and its proof is an ordinary def carrying the same name: the claim, then the evidence. Here the claim is that addition commutes, and the argument is the standard Peano one, induction on the first argument.

import Base

# Theorem: "for all numbers a and b, a + b equals b + a".
assert add_comm:
  for all a : Nat
  for all b : Nat
  {add(a, b) = add(b, a) : Nat}

# Proof: case analysis, induction, rewrites (`%`).
def add_comm(a, b):
  match a:
    case Z{}:
      %add_zero(b)
      {=}
    case S{p}:
      %add_succ(b, p)
      %add_comm(p, b)
      {=}

The statement

Propositions are types. for all a : Nat (two words) quantifies over the naturals; {add(a, b) = add(b, a) : Nat} is an equality between Nat expressions, braces around the proposition. The assert names the obligation; the def of the same name discharges it, parameter types supplied by the assert.

The proof

Case analysis plus rewriting. match a: splits on Nat's constructors — Z{} zero, S{p} successor, brace-suffixed patterns. Each % line rewrites the goal with a named equation: %add_zero(b) and %add_succ(b, p) apply lemmas from Base; %add_comm(p, b), the recursive call, is the induction hypothesis. {=} closes a branch once rewriting made both sides identical.

Following the goals

Track each branch's goal and the % lines read plainly. Zero case: goal add(Z, b) = add(b, Z); left reduces by definition, %add_zero(b) rewrites add(b, Z) to b, {=} closes b = b. Successor case: goal add(S(p), b) = add(b, S(p)); left reduces to S(add(p, b)), %add_succ(b, p) turns the right into S(add(b, p)), the induction hypothesis equates them for {=}.

Next to Lean

Term-level proofs, Agda register: recursion as induction, no tactic layer (simp, omega) in sight. Whether that trade pays off is the comparison.

B.9 · bend-docs/src/content/learn/sharing.md

Sharing, duplication, superpositions · docs-only · updated 2026-09-05 · canonical /learn/sharing/

Sharing, duplication, superpositions

Sharing one value between two uses is where Bend2's cost model lives: the fork shares nothing, duplication is explicit, and superpositions branch. Runtime claims link to runnable HVM4.

Sharing and duplication

def main() -> U32:
  x = 40 + 2      # one value...
  x + x           # ...two uses: this is the duplication point

Bend2's types are linear by default (at most one live use per binder; duplication written +x, only Data kinds duplicable). Where the checker demands it, shared values duplicate explicitly rather than by accident — the language-level face of the runtime primitive.

Unscoped lambdas

Unscoped lambdas exist in the runtime today (λ$x binders — run them in HVM4 hands-on). Their Bend2 surface syntax (planned).

Superpositions

Superpositions are deliberately introduced later, in HVM4 Runtime 9.4. Their Bend2 surface syntax (planned).

Evaluation order

Evaluation needs no annotations — order is the scheduler's business, and confluence keeps every schedule correct.

Measuring speedup

Measuring speedup is a release-day exercise: same program, CPU call vs ! call, with the runtime's interaction counters as the stopwatch (planned).

B.10 · bend-docs/src/content/learn/synthesis.md

Synthesis with SupGen · docs-only · updated 2026-09-05 · canonical /learn/synthesis/

Synthesis with SupGen

SupGen turns precise types into programs: holes mark the unfinished, specifications set the target, and search fills the gap.

Holes

A hole marks an unfinished program the synthesizer should fill — the ?name of Kind's grammar, expected in Bend2's surface (planned).

Types as specifications

"Sorted list", "parser round-tripping with its printer": types precise enough to pin behavior down. Writing them is already proving half the program; the rest is search.

SupGen

Named on the March 2026 launch-blocker list, demonstrated nowhere public. Interface, examples, and limits arrive with the release — this page will be rewritten from the compiler.

B.11 · bend-docs/src/content/learn/types-proofs.md

Types and proofs, step by step · docs-only · updated 2026-09-05 · canonical /learn/types-proofs/

Types and proofs, step by step

From annotations to proofs: how Bend2 types carry values, state equalities, and discharge obligations by recursion. The full worked proof is on the proofs page.

What is a type-based prover?

Every compiler checks your code a little. A type-based prover checks it all the way down — not just "is this a number?" but "is this claim true for every possible input?"

Three analogies, from familiar to exact:

A blueprint inspector. A function signature is a promise about shape: takes two numbers, returns a number. A normal type checker verifies the shape. A prover verifies the behavior written into the shape: takes any two numbers, returns their sum regardless of order. The checker is an inspector who refuses to sign off until the building matches the blueprint — before anyone moves in, i.e. before the program ever runs.

A fact-checker, not a spell-checker. Testing runs examples: it tries a million pairs and finds no counterexample. Proving covers the cases you didn't try — including the one your test suite missed. A test says "it worked every time we looked"; a proof says "there is nowhere for a bug to hide."

Claims are types; evidence is code. This is the whole trick, called propositions as types. The type {add(a, b) = add(b, a) : Nat} is the claim "addition commutes." A program with exactly that type is the evidence — it can only exist if the claim holds, the way a key can only exist if it fits its lock. Writing the proof means constructing that program; checking it means the compiler trying the key. In Bend2 you state the claim with assert and deliver the evidence with an ordinary def of the same name. No separate proof language, no tactic scripts: the proof is a program, and the checker simply runs its type discipline over it.

Type annotations

Every posted def annotates parameters and results (a: U32, -> U32, -> IO<Unit>).

Polymorphism

Polymorphism — functions generic over types (planned).

Dependent types

Types can mention values: the proofs sample quantifies for all a : Nat and states equality {add(a, b) = add(b, a) : Nat} as a type. Sized lists ("a list of exactly this length") and equality types are the same idea pushed further (planned).

Sized lists

Sized lists (planned).

Equality

Equality appears in the public theorem sample as {add(a, b) = add(b, a) : Nat}.

Induction

Induction in Bend2 is recursion: the add_comm proof calls itself as the induction hypothesis, and each % rewrite is checked.

Totality

The guarantee that functions terminate, which is what makes proofs sound, is enforced by the Live linear mode (planned).

B.12 · bend-docs/src/content/notes/four-interactions.md

The four interactions · stable · updated 2026-09-05 · canonical /notes/four-interactions/

The four interactions

The interaction-net model says rewrites are local and confluent. The Interaction Calculus says which four rewrites. Everything else in HVM — numbers, constructors, pattern matching — is practical extension. The theory below comes from HVM4's own docs/theory/interaction_calculus.md; the traces are quoted from it.

Why lazy needs two new forms

Strict evaluation computes everything now; lazy computes on demand but recomputes shared values used twice. Haskell memoizes thunks, which works for data and breaks inside lambdas. The calculus instead makes sharing structural, with two dual primitives (Lafont's fan nodes, opposite polarities):

• Duplication !x&L = v; t — one value in two locations (x₀, x₁).
• Superposition &L{a, b} — two values in one location.

Duplication is incremental: cloning [1,2,3] peels one layer per step, and the tail's duplication only fires when both copies are touched. Work is never duplicated — even inside lambdas.

The four rules

Two create computation, two propagate it. Superpositions are introduced here, after the language and basic runtime foundations:

Superpositions

Superposition &L{a, b} puts two values in one location. It is the runtime primitive behind branching search and shared evaluation; start with the HVM4 hands-on examples before treating it as a programming technique.

Two create computation, two propagate it:

1. APP-LAM — application eliminates lambda: (λx.body)(arg) binds x ← arg in body. Ordinary β.
2. DUP-SUP (same label) — duplication eliminates superposition: !x&L = &L{a,b}; t becomes x₀ ← a, x₁ ← b in t. Pair projection.
3. APP-SUP — application propagates through superposition: (&L{a,b})(c) becomes !x&L = c; &L{a(x₀), b(x₁)}. Applying a pair distributes over both elements.
4. DUP-LAM — duplication propagates through lambda: !f&L = λx.body yields two lambdas with a superposed bound variable, x ← &L{…}, and the body shared behind a new dup. This is the deep one: the variable temporarily escapes its scope, which is exactly why the calculus needs global variables — and exactly how sharing extends inside lambdas.

With different labels, DUP-SUP commutes instead of annihilating, nesting one superposition inside the other (the cross product from the hands-on page, formalized).

Optimal sharing, on paper

Duplicate a lambda containing (2+2), apply the copies to different arguments — the addition computes once and the result 4 flows to both copies. The trace (abridged from the theory doc) pivots on one step: DUP-LAM shares the body behind b, OP2-NUM fires a single time marked "shared!", and both branches observe 4. Memoization could never do this: the shared work sits inside a duplicated function body.

Church 2² in 14 interactions

Applying Church-2 to itself is the literature's sharing benchmark. The full trace runs APP-SUP, DUP-LAM, and DUP-SUP (both modes) across a network where bound variables visibly escape scope mid-computation — then collapses to λf.λx.f(f(f(f(x)))). HVM completes it in 14 interactions, which is optimal. The point for Bend2: this is the machinery that makes "the evaluator schedules" more than a slogan.

Collapse: reading the answer out

Reduction has three destinations: WNF (head only), SNF (full, keeps SUPs/DUPs), CNF (collapsed back to pure lambda terms via DUP-VAR/DUP-APP cleanup). The -C flag selects collapse — the enumeration of 11, 12 you saw hands-on. Proofs about programs are proved against SNF; humans read CNF.

One word per term

The machine guest of honor: every term is one 64-bit word — TAG (8) | EXT (24) | VAL (32). Tags name the node kind (APP, LAM, SUP, DUP, NUM, constructors by arity, MAT/SWI, OP2, REF…); EXT carries the dup label, op code, or binder level; VAL is a heap slot or an unboxed u32.

B.13 · bend-docs/src/content/notes/hvm-runtime.md

The HVM4 runtime · stable · updated 2026-09-05 · canonical /notes/hvm-runtime/

The HVM4 runtime

If interaction nets are the idea, HVM4 is the machine: public, a single C file built with one compiler invocation, with its memory layout and interaction rules documented next to the code. It is the half of Bend2 you can read today — the language, the type checker, and SupGen remain private, but the calculus, the memory layout, and the rules are inspectable, and they constrain what the language above them can be: parallel by default, superposition-capable, compiled rather than interpreted.

The calculus underneath

HVM4 implements the Interaction Calculus: affine variables (each used at most once — which makes garbage collection cheap and parallelism simple), global lambdas with no scope boundaries (enabling continuations and linear encodings), and two first-class primitives most runtimes lack:

• Superposition &A{a, b}: one term holding two values. (&A{1,2} + 10) yields both 11 and 12 in 4 interactions, sharing all work that does not depend on the choice. This is how an evaluator explores many branches of a search space while paying for the common structure once.
• Duplication !x&A = v; body: one value feeding two uses (x₀, x₁) without copying up front — the incremental copy described on the interaction nets page. Same label annihilates against a superposition; different labels multiply branches.

@main = (&A{1,2} + 10)
//11
//12

Metal and CUDA backends

HVM4 ships both GPU backends. The CUDA port was produced overnight by a coding model working against the Metal implementation as executable specification and test oracle; its benchmark puts CUDA ahead of Metal on RTX hardware at roughly 10x parallel C for most programs.

What the AOT compiler changes

An interpreted evaluator pays dispatch on every rewrite: fetch the node, branch on its kind, mutate the graph. Compiling a program's rules ahead of time to native C removes the dispatch and specializes memory access per rule — attacking exactly the constant factor that lets a tuned CPU core rival GPU throughput on many workloads. The AOT compiler was one of three items on the March 2026 launch-blocker list, alongside the GPU runtime (since resolved) and SupGen integration (still private).

9.1 Runtime model

An HVM program is a book of named terms. A definition such as @main = ... is a reusable static term. Evaluation instantiates the term into a mutable graph, then repeatedly finds an active pair: two principal ports connected together.

Each interaction consumes a small local configuration and replaces it with another configuration. The evaluator does not walk the entire program to decide what is safe to run. Locality and confluence make that decision independent for every active pair.

clang -O2 -o hvm src/hvm.c
./hvm file.hvm -s       # interaction statistics
./hvm file.hvm -s -C10  # collapse alternatives
./hvm file.hvm -D       # print intermediate steps

9.2 Surface syntax

The runtime language is deliberately smaller than Bend2. Definitions use @name = term; application uses parentheses, not whitespace application: @add(1, 2), not @add 1 2.

@add = λa. λb. (a + b)
@main = @add(1, 2)
//3

Variables are affine: an ordinary variable may be used at most once. When the same value must be used twice, write a cloned binder (λ&x) or an explicit duplication. This is what lets the evaluator represent copying as graph interaction rather than a global memory operation.

9.3 The 64-bit term

Every term is represented by one 64-bit word:

+--------+------------------------+--------------------------------+
| TAG 8  | EXT 24                 | VAL 32                        |
+--------+------------------------+--------------------------------+

TAG identifies the term kind. EXT carries metadata such as an operation code, constructor identity, duplication label, or binder level. VAL contains an immediate number or an index into the heap/book.

Dynamic terms live in the mutable heap; static definitions live in the immutable book. ALO allocation terms bridge them: a static term expands into a dynamic term only when evaluation forces that layer, preserving compact definitions and sharing.

9.4 Evaluation and collapse

HVM distinguishes the amount of a term it evaluates:

• WNF — weak normal form; expose the head shape.
• SNF — strong normal form; reduce the whole term while preserving superpositions and duplication nodes.
• CNF — collapsed normal form; enumerate ordinary readable results.

Collapsing is a presentation step, not the same thing as evaluation. A superposition is not automatically a list, and collapsing it too early can destroy the sharing that made the computation cheap.

9.5 GPU boundary

HVM4 has Metal and CUDA backends. The GPU does not change the interaction rules; it changes where independent graph work is scheduled. Bend2 keeps input/output on the host and sends pure computation to a device call marked with !.

Read next: The four interactions, HVM4 hands-on, and Search by superposition.

B.14 · bend-docs/src/content/notes/interaction-nets.md

Interaction nets, explained · stable · updated 2026-09-05 · canonical /notes/interaction-nets/

Interaction nets, explained

Every runtime problem that matters is a copying problem. Using a value twice means duplicating its computation or its data; throwing it away means reclaiming the memory. Conventional machines solve both with coordination — locks, reference counts, stop-the-world collectors — and coordination is what stops programs from scaling. Linear logic's great export was making this explicit: treat values as resources consumed exactly once, and copying becomes a first-class operation you can see, price, and control. Interaction nets (Lafont, POPL 1990) are the machine that takes that lesson literally.

Why coordination is unnecessary

• No coordination. Redexes are disjoint before any analysis runs; any idle worker fires any pending pair. Parallelism is scheduling, not a language feature.
• Copying is incremental and local. Duplication copies one cell per step, interleaved with the computation consuming the copies — never a whole structure in one gulp. Shared subgraphs stay shared until use forces the split.
• Erasure is garbage collection. Throwing a value away is just another local rewrite (ε), with no collector thread pausing anything.
• Every step is atomic. Each rule completes in constant time with a clear physical mapping — unlike substitution, which can copy an unbounded term.
• Perfectly symmetric. No rule has an active side and a passive side: two cells meet as equals through their principal ports. The whole system is meetings, never commands.
• Three symbols suffice. γ, δ, ε under six rules compute anything — the smallest universal machine with all of the above intact.

Copying, erasure, and confluence

A program is a graph, and sharing means what it says: two parents point at one child. When both parents need the child, a duplicator (δ) walks it — one cell per interaction, copying each cell and moving on while the rest of the net keeps reducing around it. Nothing stops, nothing locks, and work common to both copies happens once, before the split. Contrast the alternatives: textual substitution duplicates unevaluated work blindly; memcpy-style cloning drags in unused substructure; reference counting serializes every touch. Here the copy is the computation, interleaved cell by cell.

The dual move is annihilation: when a symbol meets itself, both vanish and the wires join through — erasure and pairing handled by the same geometry. In the drawings below, matching colors mark the same wire continued across the step. The richer interaction between duplication and alternative values belongs to the advanced runtime chapter; first understand the local graph and its mathematical guarantees.

The model in one minute

A program is a graph of cells. A cell is one constructor or operation — a number, a +, a list node, a λ. It has one principal port (drawn at the apex, the only place it can react) and any number of auxiliary ports where arguments and results wire in. Computation happens in exactly one configuration: two cells wired principal-port to principal-port, called an active pair. For each pair of symbols there is at most one rule, which consumes the two cells and writes a fixed replacement on the same free ports.

The two theorems that carry everything

Confluence (1990). Fire two different active pairs in either order and both orders land on the same net in one step — the pairs share no cell, so firing one leaves the other intact.

Consequences: every order reaches the same result (no scheduler can be wrong), every route takes the same number of steps (work is a property of the program, so profiling counts mean something), and any idle worker may fire any pair it finds.

Universality from three symbols (1997). γ δ ε under six rules suffice for anything computable — and every rule is one of the two symmetric meetings above. That is the whole machine: meet, annihilate, commute, repeat — at any scale, in any order, with no one in charge.

The λ-calculus, with fine print

Encode abstraction and application as cells and β-reduction becomes a single constant-time interaction. The difficulty moves to duplication: Lamping's POPL 1990 algorithm answered optimally (never duplicate work in Lévy's sense), and Asperti and Mairson proved in 1998 that full optimality's bookkeeping is unbounded — optimal counts β-steps but does not promise cheap accounting. The HVM line draws the engineering conclusion: duplication is a primitive of the calculus, not transparent substitution, trading Lamping-completeness for constant factors.

In the machine

A cell is a tagged machine word, an active pair is a queue entry, an interaction is a few loads and stores — none of it locked, because disjointness plus confluence keeps every schedule correct. The price is the constant factor: every step is graph surgery against real memory, and grinding it down is what the runtime generations are for. Numbers meet the same wall: a pure net would write 1000 as a thousand cells, so real runtimes store machine integers inside the node word, and the width left after ports and tags sets the range.

B.15 · bend-docs/src/content/notes/optimal-computer.md

Towards an optimal computer · stable · updated 2026-09-05 · canonical /notes/optimal-computer/

Towards an optimal computer

This page distills the founding essay of the Higher Order Company. It is the "why" behind every runtime, language, and proof system in these notes — read it before anything else if you want the motive, not just the mechanism.

1936, twice

Humanity answered "what is computation" twice in the same year. Turing distilled the common components of early machines into one universal device — the ancestor of every processor, and, through the procedural mindset, of C, Fortran, Java, Python. Church, independently, distilled the common components of branches of mathematics into the λ-calculus — the ancestor of Haskell, Clojure, Agda. Both compute everything computable. The choice between them was treated as taste. Taelin's argument: that was the wrong question. The right one is which model wastes less.

What each model gets wrong

The procedural model's parallel primitives — mutexes, atomics — are a contrived solution to synchronization, so programmers still write sequentially by default; global state and loops make whole classes of bugs nearly unavoidable. The functional model handles parallelism and correctness far better in principle — yet functional programs stay mostly single-threaded. Why? Performance: the λ-calculus's fundamental operation, substitution, is not atomic. Substituting an argument can copy an unboundedly large term, so it cannot complete in bounded steps and has no physical mapping. Workarounds only move the problem — shared references inhibit parallelism, garbage collection isn't atomic. The functional paradigm never got its efficient machine, never went mainstream, and its proof tools never caught up.

Annihilation and commutation

In 1997 Lafont proposed the interaction combinators, where substitution breaks into two truly atomic laws: commutation (creates and copies information) and annihilation (observes and destroys it). Unlike SKI — whose K erases and whose S copies unboundedly large structures — every combinator step finishes in constant time with a clear physical mapping, and all of it is inherently parallel. Everything good in the other models survives; the pathologies mostly vanish. Both the Turing machine and the λ-calculus emulate efficiently onto combinators, while the reverse is not true — equivalent in computability, strictly more capable in computation. Perhaps, the essay suggests, machines and substitutions aren't fundamental at all, and some alien civilization does mathematics and computing entirely in annihilation and commutation.

B.16 · bend-docs/src/content/notes/proof-lineage.md

Where the proofs come from · stable · updated 2026-09-05 · canonical /notes/proof-lineage/

Where the proofs come from

Bend2's dependent types did not appear from nowhere. They are the third generation of one author's argument: proofs are a developer-productivity tool, an evolution of types the way TypeScript was an evolution of JavaScript. Understanding the lineage makes Bend2's strangest choices (linear everything, Dead vs Live, synthesis-first) read as conclusions rather than quirks.

Proof-oriented programming

Proofs are not only a way to certify mathematics. In HOC's tradition they are a programming tool: precise specifications make generated programs checkable, so synthesis can propose and the kernel can reject incorrect answers.

Formality: proofs as superpowers

Formality (Taelin, ~2018, "a modern programming language featuring formal proofs — now written in itself") opens with the thesis outright: forget mathematics and security, the boring stuff — adding types to untyped languages already demonstrated the productivity jump, and formal proofs are the next step of that same curve. The language is there to make the developer faster, not the mathematician happier. Every Bend2 proof decision descends from this sentence: in the Lean comparison, the program is the product.

Taelin's essay on proving vs testing makes the mechanism explicit: auditing doesn't scale, tests sample behavior, proofs cover it — and the cheapest proof is one the machine helps write. That is the exact slot SupGen occupies in Bend2: synthesis proposes, the checker disposes.

Kind: the minimal theory

Kind ("a modern proof language") is the visible ancestor of Bend2's type system — and it is deliberately tiny. Its core grammar fits on one screen: dependent function ∀(x:T)U, lambda, application, self-types, datatypes with constructors, pattern matching, holes (?name) for unfinished proofs, and * as the type of types. No tactic language, no standard library ceremony: just enough theory to state and check precise types.

That design moral — the obvious algorithm works if reductions happen in precisely the right order — runs through all of HOC's work, from evaluators to checkers. Bend2 inherits the shape (quantifiers as types, programs as proofs) and adds the linearity discipline plus the Dead/Live mode split that lets it keep Type : Type without letting paradoxes near live code.

What this predicts about Bend2

Three predictions, all checkable at release: proofs will stay term-level (recursion as induction, rewrites as %, no tactic layer — tactics serve mathematicians, and Bend2 serves developers); the standard library will grow specifications first (precise types are SupGen's search targets); and the killer feature will read as productivity, not certainty — proofs replacing test suites rather than chasing foundations. If release-day Bend2 instead ships a tactic engine, this page is wrong in an interesting way, and will say so.

B.17 · bend-docs/src/content/notes/release-status.md

Release status · prerelease · updated 2026-08-27 · verified 2026-09-05 · canonical /notes/release-status/

Release status

No. As of 2026-08-27, Bend2 has not been publicly released. The current estimate is approximately 2026-09-02.

The dated trail

• 2026-03-05: launch-blocker list — HVM4 AOT compiler, HVM4 GPU runtime, Bend2–SupGen integration.
• 2026-07-18: "Bend2 complete"; CUDA backend ported overnight from the Metal reference.
• 2026-08-12: delay post (≈08-28 implied).
• 2026-08-27: launch plan — copiable-kind fix, weekend testing, Monday presentation recording, possible Wednesday launch (≈09-02).

What "released" will mean here

A public compiler (or repository with code), a license, and runnable examples. Until all three exist, every Bend2 sample on this site stays labeled documentation-only. This site is unofficial and not affiliated with Higher Order Company.

B.18 · bend-docs/src/content/notes/search-by-superposition.md

Search by superposition · docs-only · updated 2026-09-05 · canonical /notes/search-by-superposition/

Search by superposition

Superposition is usually introduced as "two values in one location" with a two-line arithmetic demo. Its serious use is different: search without loops. Apply a function to a superposition of its entire domain and you get a superposition of its entire image — with the evaluator sharing work across all guesses at once.

Truth tables for free

Evaluating (And {True False} {True False}) yields the complete truth table — {{True False} {False False}} — because applying a function to a superposed domain produces the superposed image. So brute force stops being written as nested loops:

# instead of this:
for x0 in [T, F]:
    for x1 in [T, F]:
        ...
        print(F(x0, x1, ...))
# write this:
print(F({T,F}, {T,F}, ...))

The second form shares computation across guesses wherever the guesses agree — which, for structured problems, is nearly everywhere.

SAT: 3 minutes in Rust, 1 second in HVM

Taelin's one-line-style SAT solver feeds all 2¹⁶ assignments of a random 16-variable 3-SAT instance as superposed booleans, lets the formula evaluate once across the whole superposition, then collapses per-label results back into the satisfying assignment. A 32-variable instance: ~3 minutes of Rust brute force vs ~1 second superposed. The honest caveat is his own: this was a new observation, asymptotics unknown — but the shape of the win (shared prefixes across guesses) is exactly what the machinery predicts.

Program search: 65,536 candidates, 36k interactions

The Discrete Program Search series pushes the same idea up a level: synthesize the add-carry function from a template with 16 unknown bits. Conventionally that's 65,536 separate runs (~262M interactions at ~4k per call). Superposed — one template holding all candidates, two test cases, collapse — it returns the bit vector [0,1,1,0,1,0,0,1,1,1,1,0,1,0,0,0] in 36k interactions: under one interaction per guess, a ~7200x win that grows with the search space. Enumeration and loops are fully replaced by superposition and collapse; the follow-ups extend it to DSL enumeration and superposed λ-terms.

Why this page exists in Bend2's notes

Bend2's SupGen — synthesis from precise types — is this technique aimed at programs instead of bits: types give the search a target, the checker an acceptance test, and superpositions make each guess cost less than one. The DPS posts even sketch the product shape (examples in, function out). When SupGen ships, re-read this page first.

B.19 · bend-docs/src/content/notes/vs-lean.md

Bend2 vs Lean · prerelease · updated 2026-08-30 · verified 2026-09-05 · canonical /notes/vs-lean/

Bend2 vs Lean

Both live on the propositions-as-types side of Curry–Howard: a specification is a type, a proof is a program, checking is type checking. What differs is which side pays the bills.

Lean: the proof is the product

Lean 4 (de Moura, Lean FRO, Apache 2, self-hosted through C) exists to formalize: mathematics, verified algorithms, specifications. Its center of mass is mathlib — a half-million-item library built by hundreds of contributors, so new proofs import lemmas instead of rebuilding them. Automation means tactics: decision procedures, simp sets, omega, a decade of accumulated machinery. Execution is efficient sequential C with task-level concurrency; nobody chooses Lean because their proof needs a GPU.

Bend2: the program is the product

Bend2's types exist to make machine-generated code checkable: synthesis (SupGen) proposes, the checker disposes. Its ancestor is Kind, Higher Order Company's proof language. The type theory is linear with no hidden exceptions: a plain binder allows at most one live use, duplication is written +x, only Data kinds may be duplicated. The checker splits in two — a Dead mode where specifications live unrestricted and may diverge, and a Live mode where code and proofs are linear and terminating — which keeps paradox-shaped terms on the Dead side despite Type : Type (what Girard's paradox makes inconsistent as a logic; Lean buys the same safety with a universe hierarchy plus termination checker).

The one public proof (addition commutes, August 2026) is term-level, Agda register: the function's own recursion is the induction, lemmas apply as % rewrites, {=} closes goals. No simp, no omega, no visible tactic layer at all.

The same theorem in Lean 4

For comparison, here is how a Lean user proves the same fact today — tactics orchestrating library lemmas, in about four lines:

-- Illustrative: shows the Lean style, not typechecked for this page.
theorem add_comm' (a b : Nat) : a + b = b + a := by
  induction a with
  | zero => rw [Nat.zero_add, Nat.add_zero]
  | succ n ih => rw [Nat.succ_add, Nat.add_succ, ih]

Read the two side by side. Lean's version says how to search: induction picks the principle, rw fires named equations from the library, and the library (Nat.zero_add, Nat.add_succ, hundreds of thousands of siblings in mathlib) does the heavy lifting. Bend2's version is the search result already: the recursion is the induction, each % line is one rewrite step, {=} checks the endpoints match. No search language exists because, in Bend2's story, the machine (SupGen) performs the search and the human reads the trace. Which side of that trade pays off — tactic scripts over a giant library, or machine-found term proofs over precise types — is the open bet.

Watch it run in the infoview, goal by goal — input and output in one transcript, OCaml-toplevel style:

⊢ a + b = b + a
-- induction a with
-- ├─ case zero,  ⊢ 0 + b = b + 0
-- │    rw [Nat.zero_add]   →  ⊢ b = b + 0
-- │    rw [Nat.add_zero]   →  no goals
-- └─ case succ,  ⊢ (n + 1) + b = b + (n + 1)
--      rw [Nat.succ_add]   →  ⊢ (n + b) + 1 = b + (n + 1)
--      rw [Nat.add_succ]   →  ⊢ (n + b) + 1 = (b + n) + 1
--      rw [ih]             →  no goals

A couple of remarks:

• Every rewrite names a lemma that must already exist — in mathlib, or proved just above. Bend2's % lines work the same way over Base.
• The ih in the last step is the induction hypothesis, exactly where Bend2 puts the recursive call %add_comm(p, b). Same proof, two costumes: search script vs. found term.

The default today

Lean, for anything needing a proof now — verified algorithms, formalized specs, mathematics. The library asymmetry is not close: 500,000+ items versus no public Bend2 library. Bend2 joins proofs to programs that run on HVM4 and to synthesis from precise types — a combination nobody else is selling, and nothing you can download.

B.20 · bend-docs/src/content/notes/vs-mojo.md

Bend2 vs Mojo · prerelease · updated 2026-08-30 · verified 2026-09-05 · canonical /notes/vs-mojo/

Bend2 vs Mojo

Both want high-level GPU code. They assign the scheduling job to opposite actors: in Mojo, you schedule; in Bend2, the evaluator does.

Mojo: you are the scheduler

Mojo (Modular, designed under Chris Lattner on MLIR, shipped and pre-1.0 with production users) gives explicit control: you write kernels against a grid/block/device-memory model, manage buffers and synchronization, use explicit SIMD types, and one source compiles to NVIDIA, AMD, and Apple targets. Ownership and borrowing govern values. That control is exactly what makes dense, regular, arithmetic-heavy workloads fast — performance there lives in tiling, layout, and occupancy, and no runtime discovers a tiling for you. If your sentence starts "I would have written CUDA", Mojo is today's answer for a Python-shaped codebase.

Bend2: the evaluator is the scheduler

Bend2 programs are ordinary recursive functions with no kernels, no grids, no memory hierarchy in the programmer's model. Recursion over a tree fans out because the branches are disjoint subgraphs — not because anyone scheduled it. The entire device decision is one character: sum!(24, 0) runs on the GPU where sum(24, 0) would not. Each reduction step still moves graph nodes through memory — the constant factor every graph-reduction benchmark argues about.

Where each wins

Mojo wins anywhere you could name the kernel: inference serving, image pipelines, dense linear algebra, HPC stencils — with full-width IEEE numerics and explicit SIMD today. Bend2's bet is everything irregular and recursive, where writing the kernel is the hard part and the evaluator can find work you never named. Until it ships, that side of the table is a design claim with a runtime (HVM4) behind it, not a benchmark you can run.

B.21 · bend-docs/src/content/notes/what-is-bend2.md

What is Bend2? · prerelease · updated 2026-08-30 · verified 2026-09-05 · canonical /notes/what-is-bend2/

What is Bend2?

Bend2 is an unreleased programming language from Higher Order Company. Its one-sentence idea: write ordinary functional code, get parallelism, proofs, and even synthesized programs for free — because the runtime evaluates your program as a graph where independent pieces cannot interfere, so scheduling needs no annotations from you.

Three pieces combine here. First, functional code that parallelizes automatically: recursion that splits work runs on all cores without threads, locks, or pragmas. Second, a dependent type system in the tradition of Higher Order Company's Kind: types can state properties like "this list is sorted", and the checker rejects code that violates them. Third, program synthesis (called SupGen): types precise enough to pin down behavior give a searcher something to aim at and the checker something to accept or reject.

Why this combination matters

Each piece exists elsewhere on its own. Array languages parallelize; Lean and Kind have dependent types; research languages synthesize code. The bet is that together they multiply: precise types make generated code checkable, so a synthesizer can propose and the checker can dispose — and everything runs on a runtime that parallelizes without being asked. The HVM runtime schedules independent graph rewrites; it never needed annotations and still does not.

What the language looks like

Bend2 reads like Python with types. A function is def with typed parameters and a return type after the arrow. Effects run in do blocks over an explicit IO type. A call runs on the GPU when its name carries !. A theorem is an assert block whose proof is an ordinary def of the same name. Each construct gets its own page under Learn by Example.

Status: what actually exists

As of 2026-08-30: the public VictorTaelin/Bend2 repository is empty — no code, no branches, no binary, no package, no license. What is public: four posted code samples (walked through in Learn by Example) and the HVM4 runtime. Taelin's estimate at last check points around 2026-09-02; track the release status page, which is updated as the public record changes.