Introduction

Bend is a programming language that makes an unusual promise: that you can trust a program you have not read.

The pitch, in Bend’s own words:

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

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

That is a large claim, and a claim about the future, which is hard to test. This book does not try to test the future. It tests the language.

What this book is

A tutorial. It was written by playing with Bend, not by reading its documentation — which turns out to be the right way round, because Bend’s error messages teach faster than its prose does.

Everything here was run. Every number was measured on the machine described below, and the book says how, so you can disagree with it. Where a claim of Bend’s could not be reproduced, or came out backwards, that is in the book too — those parts are usually the most useful.

Who it is for

You can already program, in some language, and you know nothing about Bend. That is the assumption, and it is the only one.

Bend introduces a few ideas that most working programmers have no reference point for: values that can be used at most once, parallel work that needs no locks, and propositions enforced by a compiler. Each of those is built up from nothing when it appears. There will be no sentence of the form “as you know, in dependently typed languages…”.

What is not explained is programming itself: what a function is, what a type is, why a program has an output.

The convention for broken code

Bend’s compiler is precise, and its errors are short. Several of the experiments in this book consist of deliberately writing something wrong and seeing what it says, because that is where the language’s real rules live.

Code that does not work is marked ❌, and the error underneath is quoted verbatim, pasted from a real run. Nothing in this book is an imagined error message.

# ❌ this is wrong on purpose
def f() -> Nat:
  1n + 0n

Error:
- message  : ...what the compiler really said

Code marked ❌ is kept in the repository as runnable files, so you can break it yourself.

The convention for quotes from the guide

Bend ships its own guide, and several chapters quote it. It is not copied into this repository — a copy would be out of date the next time Bend releases, which is often. It is on your machine already, from the same install that gave you the compiler:

bend guide                      # the whole thing, version-matched to your bend
~/.bend/guide/GUIDE.md          # the same file, if you would rather read it here

Those quotes are therefore cited by section name, not by line number:

An example quote from the guide.

— bend guide, Some Section

A line number points at whatever drifts into that position; a section name survives edits around it, and you can check it in one command.

How to read it

The chapters are ordered the way the ideas depend on each other, and they are meant to be read in order. Roughly:

• First contact — a program, and then the one rule that makes Bend unlike anything you have used before. The rule comes second, on purpose: until it lands the rest of the language is a pile of details, and after it most of the language is obvious.
• The language — the syntax and the parts of the standard library this book actually uses.
• Copies and kinds — what the rule costs, when the + mark is refused, and the two kinds of type that decide it.
• Making it fast — parallel work on the CPU, then the GPU, and when each one loses.
• A worked example — Conway’s Life, built four times: naively, then fast, then parallel, then moving. Every number is measured.
• Effects — how a program touches the world outside it, and how to write an effect of your own.
• Laws — turning a belief about your program into something a compiler checks for you.

Each chapter ends with the files it came from, so you can read the code without the book in the way.

What this was built on

Bend is young and it moves quickly, so some of what follows will have moved by the time you read it. Every measurement in this book is re-checked mechanically against whichever version you are running — see the drift directory.

What Bend 2 is, and why this book

Bend’s README makes four claims. They are worth reading carefully, because the rest of this book is arranged around testing them.

The last one is the one everything else serves. If a machine writes your code, you cannot review it by reading — there is too much of it, and you are the slowest component in the loop. So Bend’s answer is not better review. It is to make the intent machine-checkable: you write down a law your program must obey, and the compiler refuses to build the program unless a proof of that law is present.

That is why the other three claims are in the list. Proof checking is normally so slow that nobody does it while coding — if checking took minutes, you would not run it on every edit, and the whole idea collapses. And a language whose proofs are cheap but whose programs are slow does not get used either.

What it looks like

If you have written Python, Swift or Rust, Bend’s syntax will not slow you down:

type Shape is Data:
  Circle{r: U32}
  Square{s: U32}

def area(x: Shape) -> U32:
  match x:
    case Circle{r}:
      (3 * r * r : U32)
    case Square{s}:
      (s * s : U32)

match, braces, def, type annotations. It reads.

What it thinks like is a different matter. Bend is closer to Lean or Haskell than to Python: pure, no mutation, datatypes with real structure, and the same machinery proving your program correct as would prove a theorem. And its resource handling — who may copy a value, who must give it back — is closer to Rust.

So three traditions meet here, and where they disagree, Bend looks strange. Four things in particular are going to surprise you, and each gets a chapter:

• Every value is used at most once, unless you mark it otherwise. Not a safety warning — the memory model. Without this, Bend cannot free memory without a garbage collector, and cannot run two calls in parallel without locks.
• Recursion must be provably terminating, and the parameter that shrinks must be written first. The compiler checks the shape of your function, not its meaning.
• There is no if. Branching is match on a datatype that has True{} and False{} in it.
• There are no tactics. A proposition is a type, a proof is a value of that type, and you write it by hand as an ordinary def.

What this book will and will not settle

It will settle:

• Whether the parallelism is real, and how well it scales, measured on 10 performance cores.
• Whether the GPU path actually wins, on two different workloads — one where it does, one where it does not.
• Whether proof checking is as fast as claimed.
• What it costs you to write the proofs — in lines, in time, and in frustration.

It will not settle the claim about AI-generated code, which is a claim about a workflow and not about a language. What it does do is make the ingredients concrete: by the end, you will have written a law and a proof yourself, and you will have a fair idea of what that would or would not buy you on a real problem.

Where the language is not finished

Two things to know before you invest time, both true as of Bend 2.0.24:

• The compiler is, in the project’s own description, largely AI-written and not fully audited. The Lean formalization of Bend’s theory lags the actual TypeScript implementation.
• The standard library is small, and — as one chapter of this book discovers the hard way — it has almost no lemmas: facts about its own functions that your proofs can reuse. You will write those yourself.

Neither is a reason not to look. Both are reasons to measure rather than assume, which is what the rest of this book does.

Next: getting it installed, including one trap that will cost you ten minutes if nobody tells you about it.

Getting set up

Install

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

Then, in a new shell:

bend --help | head -1

Bend 2.0.24: check, run, build and publish Bend programs.

That is the version this book was written against.

Where it actually goes

The installer puts everything under ${BEND_HOME:-$HOME/.bend} — on a machine that has not set BEND_HOME, that means ~/.bend:

One self-contained file, with no runtime behind it. That is worth knowing before you read any timing in this book: nothing in the numbers is startup cost.

Careful with the repository you downloaded. If you cloned github.com/bendlang/bend to read its source, there is a directory in it named bend/. It is unrelated to ~/.bend/bin/bend. One is the upstream source tree; the other is the thing on your PATH.

The installer does not touch your shell

It prints the line to add, and leaves it to you:

  Add it to your PATH: export PATH="$HOME/.bend/bin:$PATH"

On fish it prints the fish spelling instead:

  Add it to your PATH: fish_add_path $HOME/.bend/bin

Nothing is written to your startup files, so bend resolves only once you have added that line yourself — on any shell, fish included.

The once-a-day version check

Once a day, bend asks bend-lang.com what the latest version is. It sends its own version, the OS and the CPU type, and nothing else — no code, no file names, no timings. If a newer version exists it says so, and that is all: the installed bend never updates itself.

export BEND_NO_TELEMETRY=1

turns the question off. This book sets it everywhere, and so should you if you are going to run the benchmarks in it.

The thing that will waste your afternoon: two backends

Bend has two ways to run your program, and they are not equivalent.

bend hello.bend              # ① the JavaScript target
bend hello.bend -o hello     # ② compiled to a native executable
./hello

① starts instantly and is good for everything in the first half of this book. ② takes a few hundred milliseconds to build and is what you need for the second half.

The difference is parallelism. The guide is blunt about it:

The JavaScript target ignores all that and just runs sequentially.

— bend guide, Parallelism

A fork-join program under ① produces exactly the right answer, at exactly the speed of the non-parallel version. If you measure a Bend program without compiling it, you will find no parallelism anywhere, and conclude the whole thing is marketing.

So:

cd parallel
bend pow2.bend -o pow2
./pow2 --threads 1
./pow2 --threads 8

--threads only exists on the native binary — bend file.bend --threads 8 is refused as an unknown option. It is how you tell the runtime how many cores to spread the work over.

Two kinds of main

A Bend program’s entry point can have either of two shapes, and it is worth knowing both now because the small experiments use the second:

# ① does something, prints it itself
def main() -> IO(Unit):
  do IO<Unit>:
    IO.print("hello, bend 2")

# ② computes a value; the CLI prints it for you
def main() -> Nat:
  mod(9n, 4n, 0n)

The second is what you will reach for constantly while exploring, because it turns a program into a one-line answer:

$ bend exp_mod.bend
1n

Note the trailing n — that is Bend telling you the value is a Nat, and it is the first hint of something this book leans on constantly: Bend almost never infers a type, and says so out loud.

Now that it is installed, let’s write something. Next: a first program.

A first program

Here is the smallest Bend program that does something.

import Base

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print("hello, bend 2")

Save that as hello.bend and run it:

$ bend hello.bend
hello, bend 2

Five lines, and at least three of them are doing something you have not seen before. Let’s take them one at a time.

import Base

The standard library. In Bend 2 the core library is not loaded for you, and it is called Base. You will write this line in every file in this book.

There is no Base. prefix at the call site — import Base brings the names in.

def main(), and a type that means something

def main() -> IO(Unit):

def defines a function. main is the one the runtime calls. The part to slow down on is -> IO(Unit), because it is not decoration — it is the entire answer to “how does this program run”.

Read it as: a program that performs input and output, and produces nothing interesting. Unit is the type with exactly one value in it, the way a Python function returning None has nothing to hand back.

The first idea that is genuinely new: an action is a value

Now look at the body.

  do IO<Unit>:
    IO.print("hello, bend 2")

If you come from Python, Ruby or Go, you will read IO.print("...") as “print this”. It is not that. It is a value — a description of a print — and its type is IO(Unit), the same type main returns.

Nothing has happened when that line is evaluated. IO.print("hello, bend 2") is a recipe, not a meal. The only reason the text appears on your screen is that it is the last thing in the block, so it becomes the value of do IO<Unit>:, which becomes the return value of main, and the runtime — which knows what to do with an IO(Unit) — runs it.

This is why main’s type is IO(Unit) rather than Unit. The type is what tells the runtime “there is something to perform here”. A main returning a plain Nat has nothing to perform; the CLI just prints the number. (You met that in the setup chapter.)

It will feel like ceremony for now. It stops feeling like ceremony the moment you want to know, by looking at a function’s type, whether it can touch the outside world. In Bend, that question has a one-word answer, and it is written down.

do IO<Unit>: runs them, in order, top to bottom — each line’s value flows into the next, and the block’s own value is the last line’s, which becomes main’s return value. That is all you need for now: the block itself is sugar, and what it compiles into is a chapter of its own once the language underneath is in place.

What IO.print actually prints

Run this and look very carefully:

import Base

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print("X")
    IO.print("Y\n")
    IO.print("Z")

X
Y

Z

There is a blank line after Y. Here are the raw bytes:

58 0a 59 0a 0a 5a 0a          X\n  Y\n  \n  Z\n

So IO.print appends a newline of its own. IO.print("X") writes X plus \n; IO.print("Y\n") writes Y\n plus \n, which is your blank line. There is no separate “print without a newline” in what this book uses — and when we get to the animation chapter, that trailing newline is one of the things that decides how the frame is built.

❌ Two things that do not compile

The bracket trap

Bend uses two different kinds of bracket, and they are not interchangeable:

import Base

def main() -> IO<Unit>:
  do IO<Unit>:
    IO.print("hello, bend 2")

Error:
- message  : a declared datatype (unknown: IO)
Location: main
5>| def main() -> IO<Unit>:
6 |   do IO<Unit>:

This one is worth meeting early, because the error message is actively misleading. a declared datatype (unknown: IO) reads like “you forgot to import Base”. What actually happened is the angle brackets in the return type.

The rule, and it is stranger than it looks:

• IO and Chan are functions from a type to a type. Base declares them with def, not type, so they are applied like any function, with parentheses: IO(Unit), Chan(U32).
• everything declared with type — List, Maybe, Array, Result — is applied with angle brackets: List<Nat>, Maybe<U32>. The other direction is an error too, and that one says so plainly: List(Nat) gives expected : a family instance (write List<..>).
• the do block header takes angle brackets by its own grammar — do IO<Unit>: is correct even though IO is a function — and do IO(Unit): is refused with expected : '<'.

The compiler points at the signature line and never mentions the brackets — and for IO<Unit> the message is worse than unhelpful, since it blames a type that was never declared rather than the brackets you got wrong. The same mistake cost this book’s author a bisection session, and it is preserved in the repository as basics/hello_bad.bend.

Chapter one is the wrong place to learn the rule — you meet it here as an error, and the types chapter introduces both brackets properly, with the declarations that make the difference make sense.

42 is not a Nat

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print(42)

Error:
- expected : String
- observed : U32
Location: main
6 |   do IO<Unit>:
7>|     IO.print(42)

Two facts, and only one of them is the obvious one.

The obvious one: IO.print wants a String. The second one: 42 is a U32. Bend’s bare integer literals are 32-bit unsigned integers, and a Nat is written with a trailing n:

IO.print(Nat.show(42n))    # 42
IO.print(U32.show(42))     # 42
IO.print(Nat.show(7n + 5n))  # 12

So there is no silent widening, no “it’s just a number”. Every numeric literal in Bend announces its type in the source, and mixing them is an error — not a conversion. This file is kept as basics/hello_arg.bend.

Why you have to write all this out

You have now written a program that a Python programmer would write in one line, and you had to annotate two types and choose a numeric suffix. Two things are worth knowing about that trade.

Bend does almost no type inference. The documentation says so, and it is not an oversight — it is the mechanism behind the claim that Bend checks faster than any other proof assistant. A checker that never has to search for a type is a checker that never has to search, period.

The errors are local and precise. Look again at both mistakes above: each one names the expected type, the observed type, the enclosing def, and points at a line. Neither one required you to trace through a call stack. You are paying in keystrokes and being repaid in error messages.

That is the deal Bend offers all the way through, and the proof chapters at the end are where it is paid out in full.

The files

Next: affine values — the one rule in Bend that has no counterpart in the language you already know, and the reason everything after it is shaped the way it is.

Affine values: everything is used at most once

Everything up to here would be recognisable in a language you already know. This chapter is not. It is one rule about values, it is stated in a single sentence, and it is the reason Bend exists in the shape it does.

Bend, by default, is affine, meaning variables must be used, at most, once.

— bend guide, Types and Functions

This chapter is the first one to use notation that chapter one did not introduce, so here is what the examples contain, in one place:

x = {3 : U32}      # bind x to 3. The type is written out because Bend will not
                   # infer it -- a bare `x = 3` is refused with `cannot infer`.
(x + x : U32)      # a function's body: an expression with its type stated.
match c:           # look at a value and take the first branch that fits.
  case True{}:     # a branch names a constructor; the `{}` holds its fields,
  case False{}:    # and is empty when it has none.

match gets a chapter of its own later. For now: it takes the branch whose constructor fits, and nothing else.

Here it is failing:

import Base

def main() -> U32:
  x = {3 : U32}
  (x + x : U32)

Error:
- expected : x
- observed : x (consumed more than once)
Location: main
3 | def main() -> U32:
4>|   x = {3 : U32}
5 |   (x + x : U32)

That error message — consumed more than once — is the one you will see most often in Bend. Not “undefined variable”, not “type mismatch”. Consumed.

The word “used” is doing something specific here

x + x does not read x twice. It consumes it twice. In Bend a value is less like a number sitting in memory and more like a key: to use it you hand it over, and once handed over you no longer have it.

Two experiments bracket the rule, and each is surprising in a different direction. One you have already seen — affine_bad.bend, used twice, refused. Here is the other:

You may not use a value at all.

import Base
# x is declared, and then never used
def main() -> U32:
  x = {3 : U32}
  7

$ bend t1_drop.bend
7

x is declared and then never used, and Bend is perfectly happy. This is the detail that separates affine from linear, and it is the one most people get backwards on first contact. “At most once” is not “exactly once”.

And “once” is counted per execution path, not per appearance.

import Base
# x appears in BOTH branches, but no single path takes both
def describe(c: Bool, x: U32) -> U32:
  match c:
    case True{}:
      (x + 1 : U32)
    case False{}:
      (x + 2 : U32)

def main() -> U32:
  describe(True{}, 10)

$ bend t7_paths.bend
11

x appears in two branches — twice in the source — and Bend accepts it, because no single run of that match takes both branches. The rule is about the paths a value’s life can take, not about how many times a name is typed.

Where the name comes from, because it is not arbitrary

Bend is built on a substructural type system, which is a two-hundred-year detour through logic that pays off here. The classical rules of logic let you do three things to an assumption you have been handed:

Ordinary programming languages have all three, and never think about it. If you throw them away one at a time you get a family:

exactly once   linear       (no weakening, no contraction)
at most once   affine       (weakening back, no contraction)   <-- Bend, and Rust
at least once  relevant     (contraction back, no weakening)
any number     unrestricted (everything)                        <-- most languages

Bend sits at at most once: you may drop a value (weakening is back), you may not duplicate it (contraction is gone). That is the whole of it. The word “affine” comes from affine geometry by the same analogy — an affine combination is a linear one that is allowed a coefficient of zero, so one term may be dropped.

If you want the real thing rather than this sketch: David Walker, Substructural Type Systems, chapter 1 of Pierce (ed.), Advanced Topics in Types and Programming Languages, MIT Press, 2005. The lineage starts with Girard’s linear logic in 1987.

Why anyone would do this

Read the rule again as a statement about ownership rather than usage:

A value has exactly one owner at a time.

Every headline feature of Bend is a consequence of that sentence, and they are not three features. They are one feature seen from three sides.

You get memory management for free, with no collector.

There is no garbage collector. Since values are affine, a match frees the node it opens on the spot, and only + values carry a reference count.

— bend guide, Under the Hood

If nobody else can be holding the value, then the moment you take it apart there is nothing left to do with it — so taking it apart is freeing it. That is why Bend forces you to match on things instead of reading fields out of them. It is not a style rule. It is the only way the language has to free memory.

You get parallelism that cannot race.

A parallel call promises the compiler two things: 1. The calls are independent. 2. They run in roughly the same time. Since Bend is pure and affine, the first point always holds.

— bend guide, Parallelism

The first promise is not something you assert. It is something the type system has already made true: if x has one owner, it cannot be in two parallel branches at once, so there is no way to write a race. Notice which promise is left for you — the second one. Load balancing is the entire human job.

It is worth seeing how strong this is. The one type in Base that can be mutated in place is Array, and Array is not copyable, so there is no syntax in the language that hands the same array to two parallel calls. Racing on it is not forbidden; it is unspellable.

You get proofs that cost nothing at runtime.

The third payoff is set up here and cashed in at the end of the book. There is a third quantity, -x, meaning erased: the checker can see the value, the compiler deletes it. Nothing you prove about your program needs to exist when the program runs.

What it costs

• Function arguments are consumed. After f(xs), xs is gone. This is the single biggest source of friction when adapting code you already know.
• There is no borrowing. Rust’s &x has no counterpart here. This is not an omission — search the whole guide and borrow appears zero times. Bend answers “I want to use it twice” with +x, which is a different and heavier answer, and it does not answer “let me look without taking” at all. Read the mark, for now, as this one may be used more than once. It is a request rather than a permission, so it does not always get granted — copies and kinds is where that story lands.
• Closures are affine and cannot be marked otherwise. The chapter on copies is largely about that, because the workaround is one of the more elegant things in the language.

The comparison with Rust is worth making explicit, since Rust is where most readers will have met “affine” before:

The files

Next: numbers and patterns — back to the surface of the language, where Bend’s most load-bearing syntax, the n suffix on a match pattern, makes a promise about termination.

Numbers and patterns

There are two numeric types in the part of Bend this book uses: Nat — the natural numbers, unbounded — and U32, a 32-bit unsigned integer. The suffix is what picks:

42      # a U32
42n     # a Nat

Mixing them is an error rather than a conversion, which you already met in chapter one. This chapter is about the stranger half: how you are allowed to look at a Nat.

Nat is not a machine word

Nat in Bend is a datatype with two constructors, and the pattern you write to match it is a shorthand for them. Every Nat match has this shape:

match n:
  case 0n:
    ...
  case 1n+p:
    ...

1n+p is not “equals one”. It is one or more, and it binds p to the predecessor. If you have seen x :: xs for lists, this is the same idea: the pattern takes the number apart and hands you the rest.

That is the whole reason recursion over a Nat terminates: p is genuinely smaller than 1n+p, so a self-call on p walks downhill.

❌ The pattern that swallows everything, silently

Because 1n+p means “one or more” and not “one”, the natural way to branch on a small number does not work:

import Base

# A probe, kept on purpose: this COMPILES, RUNS, and gives the wrong answer.
# `1n+p` is not "equals 1" -- it is "one or more", and it swallows 2n before
# the next case is ever considered. f(2n) is 1, not 2. See src/basics-numbers.md.
def f(x: Nat) -> Nat:
  match x:
    case 0n:
      0n
    case 1n+p:
      1n
    case 2n+p:
      2n

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print(Nat.show(f(2n)))

$ bend pat_bad.bend
1

It compiles. It runs. It invents an answer. f(2n) is 1, because the second case caught the 2n before the third case was ever considered, and Bend does not warn you that the third case is unreachable.

This file is kept in the repository as basics/pat_bad.bend, and it is the most dangerous kind of example in this book: not one that fails loudly, but one that passes.

When you want to branch on the value of a number — “is this equal to 1?” — you do not reach for match. You reach for Bool.pick, which you will meet below.

The rule you will trip over most: recursion must walk downhill

Bend requires every recursive call to be demonstrably closer to the ground. Not “closer in fact” — closer by the shape of the arguments. Here is a function that is obviously going to stop, and that Bend refuses:

import Base

# A probe, kept on purpose: this does not compile.
# p really is smaller than 1n+p -- but the checker reads arguments left to
# right, and Nat.add(p, 1n) is not *syntactically* p. See src/basics-numbers.md.
def loop(x: Nat) -> Nat:
  match x:
    case 0n:
      0n
    case 1n+p:
      loop(Nat.add(p, 1n))

Error:
- expected : a decreasing self-call (arguments are read left to right: each passed unchanged until one shrinks)
- observed : loop
Context:
- p : Nat
Location: loop
10 |     case 1n+p:
11>|       loop(Nat.add(p, 1n))

Read the error carefully, because Bend told you the whole rule in one line:

arguments are read left to right: each passed unchanged until one shrinks

So a self-call is allowed when, walking the arguments in order, everything is passed through untouched until you reach one that is the shrinking thing — usually p from the pattern, passed bare. Nat.add(p, 1n) is not p, and the checker does not evaluate it to find out.

Which gives the second half of the rule, and it is the one that bit this book’s author while writing Conway’s Life at two in the morning:

import Base

# A probe, kept on purpose: this does not compile.
# gens is the argument that shrinks, but it is not the leftmost one, and g --
# which sits to its left -- is replaced by a computed value on the way past.
# See src/basics-numbers.md.
def step(g: Nat) -> Nat:
  Nat.add(g, 1n)

def evolve(g: Nat, gens: Nat) -> Nat:
  match gens:
    case 0n:
      g
    case 1n+q:
      evolve(step(g), q)

Error:
- expected : a decreasing self-call (arguments are read left to right: each passed unchanged until one shrinks)
- observed : evolve
Context:
- g : Nat
- q : Nat
Location: evolve
14 |     case 1n+q:
15>|       evolve(step(g), q)

gens cannot be last. The shrinking argument has to come before anything that changes, because the checker stops reading at the first argument that is not the shrinking one. evolve(g, gens) is rejected; evolve(gens, g) is fine — same function, same termination, one reordered parameter list.

Why Bend is this strict

It is not paranoia about infinite loops. It is the price of the last third of this book. Bend’s theory keeps two checking modes apart:

Code that runs is checked live; types, erased arguments and equations are checked dead. Dead code may loop forever or inhabit Empty, but nothing dead ever counts as live evidence, and live recursion must terminate.

A language where a live recursion might not terminate is a language where a value of any type can be produced by running forever — including a value of the type “this program is correct”. So the proof system only works on top of a running language that provably stops. You pay in parameter order.

What you do instead: accumulate

The tools are still enough to write everything you want. basics/exp_mod.bend computes x mod n, which is not structurally recursive in any obvious way, by making the recursion structural anyway:

import Base

# A probe, kept on purpose: x mod n is not structurally recursive in any obvious
# way, so it is written as one -- recurse on the shrinking x, accumulate in k.
def bump(+k: Nat, n: Nat) -> Nat:
  Bool.pick(Nat, Nat.is_lt(k, Nat.sub(n, 1n)), 1n+k, 0n)

def mod(x: Nat, +n: Nat, k: Nat) -> Nat:
  match x:
    case 0n:
      k
    case 1n+p:
      mod(p, n, bump(k, n))

def main() -> Nat:
  mod(9n, 4n, 0n)

mod recurses on x — always downhill, always p — and carries the running remainder in k. The check passes because the checker looks at the parameters, not at the meaning. bump is where the arithmetic lives, and it is not recursive at all.

Two of those parameters carry a + — +k in bump, +n in mod — and they are there because of the rule from chapter two: both are used twice on the same path, and the mark is how you ask to be allowed that. The mark is not always granted — copies and kinds is about what decides, and about why most of this book’s code manages without it.

That shape — recurse structurally on whatever shrinks, accumulate the real work in an argument — is the standard way to get non-structural loops past the termination checker. You will see it again in the Life chapters, where it is load-bearing.

Branching on a value: Bool.pick

Since match cannot inspect a computed value, and since 1n+p is a terrible way to test equality, Bend provides a combinator:

Bool.pick(Nat, Nat.is_lt(k, Nat.sub(n, 1n)), 1n + k, 0n)

Read it as: pick a Nat; if the condition holds take the third argument, otherwise the fourth. The first argument is the type of what you are picking, which is the annotation you now expect Bend to demand everywhere.

You will use Bool.pick constantly. It is how you write if.

Small things about the arithmetic that are worth knowing early

Measured, not read:

Nat.sub(0n, 1n)   # 0     -- Nat.sub saturates at zero, it never goes negative
Nat.sub(3n, 5n)   # 0
Nat.mod(0n, 4n)   # 0

Nat.sub saturating is what makes the ring arithmetic in the Life chapters work without special-casing the edges: Nat.sub(Nat.add(x, w), 1n) is x - 1 for every x except 0, where it is 0 — which is exactly the wrap-around a torus wants.

The files

Next: types, quantities, and the two brackets — the first type declaration in the book. Then lists, where a one-line function turns out to be the reason the second half of this book exists.

Types, quantities, and the two brackets

Four chapters in, you have written types in every file — IO(Unit), Nat, String — and never declared one. This chapter is the type declaration: what it states, what the compiler refuses to let you leave out, and what the two kinds of bracket in that declaration are doing.

It exists because the next chapter’s first line is this:

type List<a, -A: Kind(a)> is Kind(a):

By the end of this chapter you can read every piece of that line. The one question it opens and this chapter does not close — why the language makes copyability part of a type at all — belongs to copies and kinds.

Your first type

The smallest useful declaration has no parameters at all:

import Base

# The no-parameter shape: every type declaration carries `is`, even
# when there is nothing to parameterise.

type Shape is Data:
  Circle{+r: Nat}
  Square{+s: Nat}

def area(x: Shape) -> Nat:
  match x:
    case Circle{r}:  (r * r : Nat)
    case Square{s}:  (s * s : Nat)

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print(Nat.show(area(Square{5n})))

$ bend exp_type.bend
25

Read it as you would read a Rust or Haskell enum, because it is one. type names the type — Shape. The indented lines are its constructors, the values the type has: a Circle or a Square. The braces are the constructor’s fields — the data each value carries — and a constructor with no fields, like Nil{} in the next chapter, carries none.

is Data is the clause this chapter keeps coming back to: it says values of this type may be copied. That is a statement about the type, not about a particular value, and it is mandatory — the next section shows the compiler refusing a declaration that leaves it out. What Data means at runtime is the copies chapter’s subject; for now it is one word of vocabulary: Data = copyable, Type = not copyable.

One more thing in that file is doing real work: the + in Circle{+r: Nat}. Fields are affine like everything else, and this area multiplies a field by itself — two uses. Remove the + from the declaration and the same function is refused:

import Base

# ❌ Fields are affine too. This `Shape` is the same as `exp_type.bend`
# minus the `+` on the two fields, and `area` multiplies a field by
# itself -- two uses of one affine value. The fix is not at the call
# site: the field must be marked `+` where the type declares it.

type Shape is Data:
  Circle{r: Nat}
  Square{s: Nat}

def area(x: Shape) -> Nat:
  match x:
    case Circle{r}:  (r * r : Nat)
    case Square{s}:  (s * s : Nat)

Error:
- expected : r
- observed : r (consumed more than once)
Location: area
13 |   match x:
14>|     case Circle{r}:  (r * r : Nat)
15 |     case Square{s}:  (s * s : Nat)

The fix is not at the call site and not in area: the field must be marked + where the type declares it. A match hands out the marks the constructor carries, so the decision belongs to the declaration — which is where a type decides what its values are allowed to do.

The clause you cannot leave out

Drop the is clause and see what the compiler says:

import Base

# ❌ The `is` clause is not optional decoration. Every type declaration
# carries one, because it is where the type says how often its values
# may be used -- and a checker that never searches needs it stated.

type Tree<a>:
  Leaf{value: a}
  Node{left: Tree<a>, right: Tree<a>}

Error:
- expected : 'is'
- observed : ':'
Location:
7>| type Tree<a>:

Read it slowly: it explains the shape of every type declaration in this book, including the ones that look decorated for no reason. The is clause is where a type says how often its values may be used — is Data for copyable, is Type for single-use, and, further down this chapter, is Kind(a) for “depends on the element”. A checker that never searches for a type also never searches for a permission: the declaration has to carry it. So a bare type Tree<a>: is not a declaration in Bend at all — it does not parse.

The first parameter is a quantity

Parameterise the type, and the natural first mistake is to type the field with the parameter itself:

import Base

# ❌ `Cell`'s field is typed `a`, the header's quantity parameter, instead
# of the element type `A`. A count of uses cannot type a field; the
# chapter takes the compiler's answer apart just below. `exp_chain.bend`
# is this same declaration with the field fixed.

type Chain<a, -A: Kind(a)> is Kind(a):
  End{}
  Cell{head: a, tail: Chain<a, A>}

Error:
- expected : Kind(a)
- observed : Quant
Context:
- a : Quant
- A : Kind(a)
Location: Cell
10>|   Cell{head: a, tail: Chain<a, A>}

The line to read is a : Quant. The guide states the rule that produces it in one line: a bare a in a parameter list is short for -a: Quant — so a is not a type, it is a quantity: a number saying how many times a value may be used. The - is the affinity chapter’s erased mark, because a quantity exists for the checker and is gone before anything runs. There are three of them, and you have been reading two of them as words:

&0   zero uses              nothing may use the value
&1   at most once           the affine default -- what `Type` means
&2   as often as you like   copyable -- what `Data` means

Type is short for Kind(&1) and Data for Kind(&2). So the is Data on Shape was &2 all along, and every List<&2, Nat> in the lists chapter is a list whose elements may be copied. The three are ordered, and combining two of them keeps the smaller — that is the <&> in the ladder below.

&0 is the bottom of that scale: zero uses, nothing may use this. It is a mark to read rather than one to write. base.bend contains no &0 at all, and the guide mentions it only in a comment and in its grammar table; &1 and &2 are the two you will write, mostly in the shorthand List<Nat> for List<&1, Nat> and +List<U32> for List<&2, U32>.

That leaves the error itself. A quantity is a number and a field carries a type: head: a asks the checker to treat a count of uses as data. The element type therefore needs a parameter of its own, A — and Kind(a) is what states which kind of type A is allowed to be.

Why IO(Unit) and List<Nat>

Two spellings of the same idea sit one line apart in the declaration that failed above: A : Kind(a) in the error’s context, Chain<a, A> in its last line. Angle brackets belong to declared datatypes and to nothing else: everything else that takes a parameter — a def like IO, a builtin kind like Kind — is applied with parentheses.

So IO(Unit) is a call whose result is a type (bend base shows def IO(A):), and List<Nat> is a datatype fixed at its parameter, with no call and nothing computed. A name declared with type — in Base or in your own file — takes <>; anything else that takes parameters takes ().

The one place that looks violated is every main:

def main() -> IO(Unit):     # a call: IO is a def, applied with ()
  do IO<Unit>:              # the header's own grammar: always <>

The do header is neither a call nor an instantiation; it has a grammar of its own and always takes <>. It gets a chapter later: Inside a do block.

The element type is its own parameter

With the quantity and both brackets in hand, the corrected header reads one piece at a time:

type Chain<a, -A: Kind(a)> is Kind(a):

• a — a quantity parameter: the &0/&1/&2 from above. Erased, but still passed at the call site, because the checker reads it.
• -A: Kind(a) — the element type. The - is the affinity chapter’s erased mark again, and Kind(a) is its annotation: a type whose values may be used a times.
• is Kind(a) — the Chain itself may be used a times. A chain is exactly as reusable as its elements, and the header says so.

The corrected declaration checks, and so does a function over it:

import Base

# The smallest parameterised type that checks. Read the header as:
# "Chain is parameterised by a quantity `a` and by an element type `A`
# whose values may be used `a` times; the Chain itself may be used
# `a` times -- a chain is exactly as reusable as its elements."
# Fields are typed `A`. The self-reference passes both parameters.

type Chain<a, -A: Kind(a)> is Kind(a):
  End{}
  Cell{head: A, tail: Chain<a, A>}

def len(a, -A: Kind(a), xs: Chain<a, A>) -> Nat:
  match xs:
    case End{}:      0n
    case Cell{h, t}: (1n + len(a, A, t) : Nat)

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print(Nat.show(len(&2, Nat, Cell{1n, Cell{2n, End{}}}))
)

$ bend exp_chain.bend
2

Note what len’s signature looks like — the same two leading parameters, in the same order, at every call site:

def len(a, -A: Kind(a), xs: Chain<a, A>) -> Nat:
    ...
    len(&2, Nat, xs)

&2 fills a, Nat fills A. You are passing a number and a type as arguments, before the list itself. This is not Chain being exotic — it is the minimum shape of every parameterised type in Bend, and the next section shows Base using it four times in a row.

The ladder in Base

bend base --types prints every type declaration in the standard library. It is one short ladder, and each rung is a shape this chapter has now introduced:

type Nat is Data:                                  # no parameters
  Zero{}
  Succ{pred: Nat}                                  # self-reference, no kind to pass

type Maybe<a, -A: Kind(a)> is Kind(a):             # one element type
  None{}
  Some{value: A}

type Either<a, b, -A: Kind(a), -B: Kind(b)> is Kind(a <&> b):
  Inl{value: A}
  Inr{value: B}

type List<a, -A: Kind(a)> is Kind(a):
  Nil{}
  Con{head: A, tail: List<a, A>}

type Array<-T: Type> is Type:                      # the contrast
  ALeaf{value: T}
  ANode{xs: Array<T>, ys: Array<T>}

Four things in that ladder, in order of strangeness:

String-style self-reference needs no kind parameter. A type with no element type — Nat, String — has a fixed kind and says it once: type String is Data: ... tail: String. The recursion is as plain as the type.

Maybe, List carry one a/A pair. The field is typed A — the element type — never a, which is a quantity. (List here is Base’s real declaration, straight from bend base --types; if you have seen this line with head: a, that version does not compile — the checker’s a : Quant error above is what it produces.)

Either carries two, and the two kinds combine with <&>: Kind(a <&> b) — the smaller of the two quantities, so an Either is as reusable as its least reusable element.

Array is the counterexample. It is is Type — never copyable, whatever it holds — so it does not need the kind as a parameter, only the fixed annotation <-T: Type>. A handle’s copyability does not follow its contents; that is exactly what makes it a handle, and it is the whole story of the arrays chapter.

At the use site

Three spellings, one meaning:

List<Nat>          # the checker fills in the quantity: List<&1, Nat>
List<&1, Nat>      # spelled out: affine elements, affine list
List<&2, Nat>      # copyable elements
+List<U32>         # the + spelling, same as List<&2, U32>

A list literal is written with the quantity it gets: [1n, 2n, 3n] is a List<&2, Nat> — the numbers are freely copyable and the list does not promise otherwise. That is why Base’s functions announce it:

List.length(&2, Nat, [1n, 2n, 3n])    # 3

and it is why a List<Nat> — a promise to use the list at most once — gladly accepts a List<&2, Nat>: a value that may be used many times may certainly be used one. The useful direction is free; the reverse is the checker’s business, and the copies chapter’s.

What this chapter leaves open

You can now read every type declaration in this book. What you cannot yet answer is the question the machinery keeps asking: why does copyability travel with the value, and what does &2 cost at runtime? That is the subject of copies and kinds — two chapters from here, and the single most consequential idea in the language.

The files

Next: lists — the declaration you can now read in full, and the one-line function that turns out to be the reason the second half of this book exists.

Lists

A List in Bend is what it is in every functional language: a chain of cells, each holding one value and a pointer to the rest, ending in an empty cell.

type List<a, -A: Kind(a)> is Kind(a):
  Nil{}
  Con{head: A, tail: List<a, A>}

Every piece of that header was introduced in the types chapter: a is a quantity parameter, A the element type, is Kind(a) says a list is exactly as reusable as its elements. (The field is typed A, not a — an earlier edition of this book printed head: a, which does not compile: a is a quantity, and the checker refuses a field typed with one.) What that header means at runtime — why copyability decides anything — is the subject of copies and kinds, three chapters from here.

There is also an infix spelling. h <> t builds or matches a cell, and Base uses it; Con{h, t} is the same thing. Both work.

Walking a list is the only way to read it

There is no indexing. To get at element i you walk i cells:

import Base

def nth(xs: List<Nat>, i: Nat) -> Nat:
  match xs:
    case Nil{}:
      0n
    case Con{h, t}:
      match i:
        case 0n:
          h
        case 1n+p:
          nth(t, p)

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print(Nat.show(nth([1n, 2n, 3n], 1n)))

$ bend exp_list.bend
2

Correct — [1, 2, 3][1] is 2 — and it cost two steps. That cost is O(i), and it is worth pausing on, because this five-line function is the reason the second half of this book exists.

Here is the arithmetic. Suppose you keep a w × h grid as one flat list of w*h cells, and you want to compute the next generation. Each cell needs its eight neighbours, and each neighbour lookup is a walk to that index — so one generation is O((w·h)²). At 64×64 that is 4096 cells and about 4096 steps per neighbour lookup. Nothing looks wrong; the program is short and correct.

That is exactly the trap the Life chapters walk into, measure, and then climb out of — and the climb is not “use a better data structure” in the abstract. It is a specific rewrite that turns O(n²) into O(n) while keeping the same output. Keeping this chapter’s nth in mind makes that chapter much easier to follow.

List.range, and the quantity on its return type

Base gives you a few list functions. The useful one here is range, which produces the numbers from 0 to n-1:

List.range(4n)    # [0n, 1n, 2n, 3n]

Its return type is written List<&2, Nat> rather than List<Nat>, and that &2 means this list may be used more than once. It is a small detail with large consequences: it is why range is the natural starting point for building a grid, and why some other functions are not.

The oddest signature in the standard library

Here is List.append as Base declares it:

def List.append(a, -A: Kind(a), xs: List<a, A>, ys: List<a, A>) -> List<a, A>

The first argument is not a list. It is a quantity — the &2 from the line above, passed at the call site:

List.append(&2, Nat, xs, ys)

and the second is the element type. Base’s own source writes it both ways, because inside the library the quantity is usually a parameter that is already in scope.

You met this shape in the types chapter, on a hand-written Chain; here it is in Base, where you cannot avoid it. It is Bend being honest about something most languages hide: the “may this be copied?” question is part of a list’s type, so a function that takes lists cannot ignore it. If you have ever wondered why Bend’s type annotations feel like they leak, this is the leak. copies and kinds explains where it comes from and why the language considers it a feature.

A note on the direction of travel. While writing the Life chapters, this book’s author eventually wrote a four-line app rather than call List.append, purely to stop threading &2 and Nat through every call site. Both work. If you find yourself doing the same, that is a fair reading of the language and not a mistake.

Lists versus arrays

Bend has an Array type as well, with real random access. It is not a drop-in replacement, because an array is not copyable — the type system refuses to duplicate one. That is what buys in-place mutation without giving up purity, and it is why the Life chapters end up using lists for the grid even though an array would be faster to index.

Hold on to that tension. It is the same tension as &2, seen from the other side, and the chapters on copies and arrays are about resolving it.

The files

Next: strings and characters — another linked list, wearing a friendlier face, and a trap that produces the wrong bytes without complaining.

Strings and characters

A String in Bend is a linked list of characters — the same shape as the list you just met, with one element type:

type String is Data:
  SNil{}
  SCon{head: Char, tail: String}

So everything you know about the cost of lists applies here, and one more thing does not: text goes through this structure one character at a time.

Char is a character

Not a byte. Measured:

String.length("█")    # 1
String.length("██")   # 2
String.length("😀")   # 1

This is worth stating explicitly because it will matter later, and because it is the sort of thing that differs between languages and silently ruins programs. A Char is a Unicode scalar value. So a string is a sequence of characters, and String.reverse reverses characters — which is a precise statement you will need in the chapter about the animation frame, where the whole renderer hangs off it.

Escapes, and the trap with no name

The list of legal escapes is short, and the compiler will recite it at you if you guess. This is not a made-up error message — it is what Bend answers to "\e":

import Base
def main() -> IO(Unit):
  do IO<Unit>:
    IO.print("\e")

Error:
- expected : an escape (\n \t \r \0 \\ \' \" \u{1F600})
- observed : '"'
Location:
3 |   do IO<Unit>:
4>|     IO.print("\e")

Eight forms. \n, \t, \r, \0, a backslash, a quote, a double quote, and \u{...}. That is all.

There is no \e and no \x1b. For a terminal escape you write \u{1B}:

IO.print("\u{1B}[H")    # ESC [ H -- cursor to the top-left corner

Which brings us to the one that will cost you an afternoon, because it does not produce an error at all:

import Base

# A probe, kept on purpose: this COMPILES, RUNS, and emits the wrong bytes.
# There is no octal escape. "\033" is "\0" (NUL) followed by the two literal
# characters 3 and 3. The bytes are 00 33 33 -- not 1B. For an escape you want
# \u{1B}. See src/basics-strings.md.
def main() -> IO(Unit):
  do IO<Unit>:
    IO.print("\033")

$ bend esc_bad.bend | xxd
00000000: 0033 330a                                .33.

00 33 33 0a. Not 1B. Here is what happened: there is no octal escape, and \0 is a perfectly legal one. So "\033" parses as \0 — a NUL byte — followed by the two literal characters 3 and 3. The program compiles, runs, and emits something that is not the escape you wanted.

Kept as basics/esc_bad.bend. This one is worth remembering in the abstract, because the shape recurs: Bend’s error messages are excellent right up until you write something legal but unintended, and then there is no message at all.

The cost of text

Two functions, both O(n), and neither is a problem by itself:

String.append(a: String, b: String) -> String
String.length(s: String) -> Nat

Note that append takes no quantity argument, unlike List.append. Strings are Data — freely copyable — so nothing has to be threaded through.

The cost that is a problem is the one you build by accident:

# O(n^2): each append walks its first argument to find the end
String.append(String.append(String.append(a, b), c), d)

Every one of those calls copies the accumulated left side. Building a long string this way is quadratic in its length, and nothing in the program looks wrong.

There is a standard fix, and it is the one this book’s animation uses: build the string backwards, then reverse once at the end. Reversing is O(n), so the whole construction becomes O(n). Base itself uses this idiom — String.reverse is an accumulator loop internally:

def String.reverse.go(s: String, acc: String) -> String:
  match s:
    case SNil{}:
      acc
    case SCon{h, t}:
      String.reverse.go(t, SCon{h, acc})

def String.reverse(s: String) -> String:
  String.reverse.go(s, SNil{})

A shape to remember, and one to beware of. That reverse is a helper with an accumulator, and the public function calls it with SNil{}. It is a good design and it will come back to bite the proof chapters: a function written this way is stuck on a variable — the checker cannot look inside it without knowing what acc is. When we get there, that is why three of the lemmas in the second proof exist at all.

The files

That is the language’s surface: the syntax, the numbers, the lists, the strings. The one rule from chapter two has been running in the background of all of it — every function here consumed its arguments, and nothing complained.

The two chapters that follow are about the machinery behind that rule: the quantity marks that ask permission to copy, and the types that refuse it.

Next: copies, kinds and the + mark — where the &2 on List.range finally gets its explanation.

Copies, kinds, and the + mark

The chapter on affine values left a promise unkept: there is a way to use a value twice — write +x — but it is refused for some types and not others. This chapter is about what decides that, and about the loose end from the lists chapter, where List.range returned a List<&2, Nat> and nobody said what the &2 was.

Three quantities

A value can be bound three ways. The mark goes on the variable, at the point where it is introduced:

-x = ...     # erased     -- the checker sees it, the compiler deletes it
 x = ...     # affine     -- at most once. the default
+x = ...     # reusable   -- as many times as you like

-x is the one for proofs and type-level arguments: it exists so the checker can reason about something that has no runtime representation at all. You will meet it properly in the laws chapters.

+x is the interesting one, and it does not always work:

import Base
# trying to mark an array as reusable
def main() -> U32:
  +a = [0 : U32*4n]
  b = a[0]
  c = a[1]
  (b + c : U32)

Error:
- expected : Data
- observed : Type
Location: main
4>|   +a = [0 : U32*4n]

Bend is telling you that + is not a permission you grant. It is a property you ask for, and the type has to already have it. An Array does not.

Kinds: the property lives on the type

The types chapter introduced Kind(a) as machinery every parameterised type is forced to carry. This section is what the machinery is for: the kind is where the copy permission lives, and + is how a function asks for it.

Types themselves are sorted into two kinds, and the kind is part of a type’s declaration:

type Array<-T: Type> is Type:      # <- not copyable
type List<a, -A: Kind(a)> is Kind(a)   # <- copyable when A is

Type = Kind(&1)   may be used at most once -- a thing with identity
Data = Kind(&2)   may be copied           -- a thing without identity

So Data is not a different sort of value; it is a type that carries a permission. +x demands Data because you cannot copy a thing that cannot be copied, and that is the whole content of the error message above.

Base declares 22 types. 13 are is Data and exactly 3 are is Type. The other 6 — List, Maybe, Either, Result, Map, Sigma — are parameterised by their own kind, which is the subject of the next section. The three Types are worth reading as a list, because they are not arbitrary:

Array      a block of mutable memory
IO.OP      one IO operation
App        an application window

All three are handles. Copying a block of mutable memory would break the guarantee that in-place rewriting does not need to copy — two names for one block means the rewrite is visible through both, which is precisely what the Type/Data split exists to prevent. Copying an IO operation would forge a resource that was never created.

And List<U32> is Data, because copying a list just copies a structure. So this is accepted:

import Base
def main() -> Nat:
  +xs = {[1, 2, 3] : +List<U32>}
  Nat.add(List.length(&2, U32, xs), List.length(&2, U32, xs))

$ bend t8_listplus.bend
6n

while the same shape without + is refused:

import Base
def main() -> Nat:
  xs = {[1, 2, 3] : List<U32>}
  Nat.add(List.length(&1, U32, xs), List.length(&1, U32, xs))

Error:
- expected : xs
- observed : xs (consumed more than once)

The loose end from the lists chapter

Now the loose end — not how to read the header, which the types chapter covered, but why the kind has to be a parameter at all:

type List<a, -A: Kind(a)> is Kind(a)

A is the list’s own kind, threaded through as a type parameter — so a list’s declaration says whether it may be copied, and List.range returns List<&2, Nat> because the numbers it builds are freely copyable.

It also explains the oddest signature in the standard library, which the lists chapter flagged:

def List.append(a, -A: Kind(a), xs: List<a, A>, ys: List<a, A>) -> List<a, A>

The quantity is the first argument because a list is parameterised by its kind, and a function that takes lists cannot ignore that. You thread it through at the call site:

List.append(&2, Nat, xs, ys)

Bend is not hiding the copy question. It is making you answer it, at every call site, forever.

What + actually costs

It is not free, and the guide says why in the same breath as the no-GC claim:

Since values are affine, a match frees the node it opens on the spot, and only + values carry a reference count.

— bend guide, Under the Hood

So the price of +x is a runtime reference count — a real increment, decrement and check, on every use. When you write +x you are trading the thing that makes Bend fast for the convenience of not restructuring your code. Do it when the restructure is worse, not by default.

Closures, and a restriction that made the language faster

One more type refuses +, and the refusal is the same one:

import Base
# can the closure itself be called twice? t5 again, plus one +
def main() -> U32:
  +f = {x => (x + 1 : U32) : U32 -> U32}
  (f(1) + f(2) : U32)

Error:
- expected : Data
- observed : Type
Location: main
4>|   +f = {x => (x + 1 : U32) : U32 -> U32}

A closure is Type, so it can be called exactly once, and there is no way to mark it otherwise. + does not open this door.

This looks like a real limitation, and for a while it is. Then you find the answer, and the answer is better than the thing it replaced:

import Base

# ~f is a *template* parameter: the argument is substituted at compile time,
# not passed at runtime, so f can be called as many times as you like.
#
# The parameter-side ~ makes f a template. The call-site mark is optional;
# t11_template_implicit.bend shows the same call without it.
def twice(~f: U32 -> U32, x: U32) -> U32:
  f(f(x))

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

$ bend t10_template.bend
42

The checker adds nothing on stderr: a template instance is not disclosed as unsafe. The gate chapter is where the unsafe disclosure gets taken apart.

The ~ on the parameter means template. At the call site the mark is optional: the compiler specializes the argument with or without it. twice is inlined at compile time, and each distinct argument compiles its own copy of the function — so f can be called as many times as the body likes, because at runtime there is no closure there at all. Not a function pointer, not a reference-counted box. Inlined, and free.

Bend’s type system refuses to let you copy a closure. The answer the language arrived at is not “write more code” — it is “inline the function”, which is faster than the version that would have been allowed.

Hold on to that shape. It recurs throughout this book: a restriction that looks like a wall turns out to be the reason the thing is fast.

The files

Next: arrays — where the two kinds collide, and a read hands you back more than you asked for.

Arrays: a read hands you a pair

Everything in this chapter comes from one type signature:

a[i]  ::  Sigma<&1, &1, Array<U32>, _ => U32>

Reading an element out of an array does not give you the element. It gives you the array and the element, together. This is the single most surprising thing in Bend’s surface syntax, and it is not a quirk — it is forced, and the chapter is mostly about seeing why.

Watch it happen

The clearest demonstration is to just print what you get back:

import Base
def main() -> Array<U32> & U32:
  a = [0 : U32*8n]
  a[5] <- 42       # an in-place rewrite, not a copy
  a[5]             # returns the array AND the element

$ bend e_post1.bend
([0, 0, 0, 0, 0, 42, 0, 0], 42)

A pair. On the left, the whole array with the write visible in it; on the right, the element that was asked for.

Why it is forced

From the previous chapter: Array is Type. It is the one thing in the language you may rewrite in place, and it is not copyable — that is exactly the trade that makes in-place rewriting need no copy.

Now suppose a read gave you just the U32. Where would the array go? The read has to hold the array to look inside it, and since the array may not be duplicated, the read cannot keep a copy and hand you the value. It must give the array back. So the return type is a pair, and there is no version of this design that returns a bare element.

This is the affinity rule from chapter two, arriving at the syntax you actually type.

Four ways to try to get the value out

The obvious attempts do not work, and the errors are worth reading in full because together they draw a precise line.

Try to assert the type. a[5] : U32:

import Base

# A probe: how an array read feels. a[i] returns Array<U32> & U32 (a Sigma).
#
# The binding carries its type because an array is `Type`, not `Data`: in a
# `do` block a bare `a = [..]` is read as a pattern, and the checker refuses it
# with `expected : a pattern (a binder or a constructor)`. The read below is
# what this probe is about, and it is refused too.
def main() -> IO(Unit):
  do IO<Unit>:
    a : Array<U32> = [0 : U32*8n]
    a[5] <- 42
    IO.print(U32.show(a[5] : U32))

Error:
- expected : a term
- observed : ':'

The ascription is not even parsed here. A pair is not a U32 and saying so does not make it one.

The binding above carries : Array<U32> for a reason worth knowing, since you will hit it: an array is Type, and in a do block a bare a = [..] is read as a pattern, which the checker refuses. Write the type on the binder and it is a binding again.

Try to destructure it where it is written. (a2, v) = a[5]:

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

Try to name it first, then destructure. p = a[5] then (a2, b) = p:

import Base
def main() -> U32:
  a = [0 : U32*4n]
  p = a[5] <- 42
  (a2, b) = p
  (b + 42 : U32)

Error:
- message  : a parameter or field scrutinee (a match cannot scrutinize a local binder: give it its own def)

Notice that those two messages are the same rule with two different subjects: a computed value, and a local binder. Bend will only take a pair apart where it is already a thing you were handed — a parameter, or a field. In between, you are not allowed to hold it and look at it.

And notice what the compiler does about it: it tells you the workaround. Give it its own def. That instruction is not a hint, it is the whole solution, and it is the same shape as the nth trap in the chapters ahead.

The two ways that work

Give it its own def, and destructure in the parameter position:

import Base

# the pair may only be destructured where it is a parameter or a field
def unzip(p: Array<U32> & U32) -> Array<U32>:
  (arr, _) = p
  arr

def value(p: Array<U32> & U32) -> U32:
  (_, v) = p
  v

def main() -> U32:
  a = [0 : U32*4n]
  a[5] <- 42              # in-place write; rebinds a
  b = unzip(a[0])         # read idx 0 (0), keep the array half
  U32.add(value(b[5]), 1) # read idx 5 from the returned array -> 42

$ bend b_ok.bend
43

Running unzip and value as separate functions is not stylistic padding. Those two functions exist because that is the only place a pair may be opened.

Or use the projections that Base ships, which are typed by the pair’s own two halves:

import Base

# Base ships the projections: Pair.fst / Pair.snd, typed by the pair's own halves.
def main() -> U32:
  a = [0 : U32*8n]
  a[5] <- 42                              # in-place write; rebinds a
  b = Pair.fst(Array<U32>, U32, a[5])     # the array half, unchanged
  Pair.snd(Array<U32>, U32, b[5])         # the element half -> the write survived

$ bend c_base.bend
42

Pair.fst and Pair.snd take the two half-types as their first two arguments and then the pair. They exist precisely so that you do not have to write a def per read.

What a write returns

A write, a[i] <- v, is a different thing, and its type is easy to guess wrong. Asking for the wrong half makes Bend print both:

import Base
# What exactly does a write return? Its second half, printed.
def main() -> U32:
  a = [0 : U32*8n]
  a[5] <- 42
  Pair.snd(Array<U32>, U32, a[9] <- 7)    # write idx 9, look at the second half

Error:
- expected : Sigma<&1, &1, Array<U32>, _ => U32>
- observed : Array<U32>

Those two lines are the answer. A read returns Sigma<&1, &1, Array<U32>, _ => U32> — a pair. A write returns the bare Array<U32>, because there is no element to hand back; you supplied it.

And on its own line, a write rebinds:

a[5] <- 42      # this is sugar for:  a = a[5] <- 42

which is why the pattern in every probe above is a write followed by reads against the same name.

The files

That is the whole idea. Affinity, kinds, and the pair — one mechanism, spread over three chapters, and at this point you have seen everything in Bend that is genuinely unlike other languages.

The rest of the book is what that mechanism buys: parallelism that cannot race, a GPU path where the compiler does the memory management, and finally proofs the compiler checks.

Parallel by default: fork-join

Bend’s parallelism primitive is an ordinary assignment. There is no keyword, no annotation, no runtime to configure:

a b = f(x) g(y)      # two calls, each becomes a task, then they join

That is the whole language surface. Everything else in this chapter is about what it does and does not buy you.

Two promises, and only one of them is yours

The guide states the contract:

A parallel call promises the compiler two things: 1. The calls are independent. 2. They run in roughly the same time.

— bend guide, Parallelism

The first promise is not something you assert. It is something the type system has already made true, and this is the payoff from the affinity chapters arriving in earnest. A value has one owner. If x is owned by the call on the left, the call on the right cannot be touching it — not “should not be”, cannot, because there is no second name for it to hold. So f(x) g(y) cannot race, and you did not have to prove it.

It goes further than “no locks needed”. The one type in Base that can be rewritten in place is Array, and Array is Type — not copyable. So there is no syntax in the language that hands the same array to both sides of a parallel call. Racing on an array is not forbidden; it is unspellable.

The second promise is the entire human job.

Bend’s scheduler is a binary fork-join machine, in the words of the guide, contention-free: every task is handed to a core exactly once and never migrates afterwards. That is what makes it fast, and it is also what makes load balancing your problem. If one side of your fork takes ten times as long as the other, no amount of cores helps — one core does everything while the rest wait at the join.

What it looks like when it works

Here is a function whose body is a balanced binary tree, which is the shape the scheduler likes:

import Base

# A divide-and-conquer example over parallel calls: pow2(n) = 2^n
def pow2(+n: Nat) -> U32:
  match n:
    case 0n:
      1
    case 1n+p:
      a b = pow2(p) pow2(p)
      (a + b : U32)

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print(U32.show(pow2(26n)))

pow2(26n) is 2^26 = 67,108,864 additions, arranged as a complete binary tree of forks. Native-compiled, three runs per configuration:

Read the two columns against each other, because that is the evidence. user barely moves while real falls by nearly five times. The total work is the same; the wall clock got shorter. That is what real parallelism looks like, and it is the only way to tell it from a machine that is simply fast.

Scaling saturates at 8. This machine is 10 performance cores and 4 efficiency cores, so past 8 there is nothing left to give except scheduling overhead.

Where the numbers come from

Every number in this chapter, and in the rest of this book, was measured on a compiled binary:

bend pow2_26.bend -o pow2_26     # compile
./pow2_26 --threads 1            # then time the binary, not the interpreter
./pow2_26 --threads 8

bend pow2_26.bend interprets instead, and the interpreter is sequential: no call forks, and the wall clock is identical at every thread count. Getting set up has the two backends in full; what this chapter needs from them is one line — a performance number means nothing unless it came from a compiled binary.

That is worth a section of its own because the difference is invisible in the output. A sequential run looks exactly like a parallel run that does not scale: the right answer, user about equal to real, and no speedup at any thread count.

The files

Next: the GPU, and the ! mark — where ! turns out to mean the GPU rather than more cores, and a fixed cost turns out to decide who wins.

The GPU, and the ! mark

Putting ! after a function name hands that call — and every parallel call inside it — to the GPU:

pow2!(26n)     # the GPU
pow2(26n)      # the CPU, still multi-core

That is the entire syntax. This chapter is about what it costs, and the cost is not where you would expect.

What a ! call builds

bend file.bend -o file writes two things:

file        the host program
file.gpu    a MetalLib kernel

The host binary loads the kernel and drives it. The compilation path is Bend → C → clang, and the interesting part is that it is one C program: gpu/mandelbrot/main.c is 4,174 lines generated from a 6,427-byte .bend, and it contains #ifdef __METAL_VERSION__, so the same source builds both the CPU binary and the Metal kernel.

You will see this line on stderr whenever the kernel is missing or out of date:

bend: compiling the GPU program (... .gpu is missing or stale)

It is not an error, and it is not free.

The numbers, which are not what they look like

Three workloads, native-compiled, three runs each. The checksums all match the values recorded in the sources, so this is the same computation on two pieces of hardware and not a mistake in a loop bound.

Read at face value: the GPU wins at mandelbrot by about 6×, loses at pow2 by about 2×, and loses at queens by about 1.6×. That is the story this repository recorded the first time round, and it is the story the guide’s one sentence predicts:

The GPU shines on uniform numeric work like mandelbrot or nbody; divergent work like n-queens stays faster on the CPU.

But face value is wrong, and here is how it was caught.

The entry cost

Every GPU run takes about 85 ms before it does anything. That was not obvious; it had to be measured, by writing a ! program that computes almost nothing — the same fork-join tree as pow2, asked for pow2!(2n), which is 4.

import Base

# The floor cost of one `!` call: the same shape as pow2, but it computes
# almost nothing. Whatever this takes is overhead, not work.
def pow2(+n: Nat) -> U32:
  match n:
    case 0n:
      1
    case 1n+p:
      a b = pow2(p) pow2(p)
      (a + b : U32)

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print(U32.show(pow2!(2n)))

gpu_floor   pow2!(2n)          = 4        82 – 91 ms
pow2_gpu    pow2!(26n)   = 67108864       89 – 96 ms

Sixty-seven million additions cost about the same as four. So essentially all of that time is entry, not work. And two ! calls in one process cost about the same as one:

gpu_twice   pow2!(25n) + pow2!(26n)       97 – 114 ms

So it is a per-process cost, paid once — not a per-call tax.

It is also not the kernel compilation, which is what the stderr line suggests. gpu_floor’s kernel is trivial and it costs the same as mandelbrot’s, which is much larger. What you are paying for is the Metal runtime: device, command queue, pipeline state.

What the table says once you subtract it

Take ~85 ms off every GPU number:

Every conclusion changes shape:

• pow2 is not a case of the GPU losing at arithmetic. The GPU does 2^26 additions in less time than the measurement can resolve. What makes pow2!(26n) slower end-to-end is the 85 ms door. The earlier note in this repository — that the overhead is all in fork-join scheduling — was wrong, and gpu_floor is what disproves it: fork-join is exactly what the CPU does well, and a program with no fork-join left in it still pays the 85 ms.
• mandelbrot’s win is far larger than it looks. The often-quoted “7.6×” understates the hardware and overstates the price. The honest pair of numbers is: ~30 ms of GPU work against 722 ms of 10-core CPU work, plus a fixed door charge that a real application pays once.
• queens genuinely loses. Its GPU work is about 1.29 s against 0.855 s on ten cores. This is the one place where the guide’s divergence sentence is doing real work rather than being a truism.

The one-line lesson

A wall-clock number for a GPU path is not a statement about the GPU. It is a statement about the GPU plus a fixed cost that does not shrink when the work does. To find out which of the two you are measuring, write the program that does nothing and time that.

Building either target

There is no --gpu flag. The two paths are separate:

# GPU: the default build, produces both the host program and the kernel
bend main.bend -o gpu            # -> gpu and gpu.gpu

# CPU only: let bend emit C, then compile it yourself so nothing links Metal
bend main.bend -o main.c
clang -O2 main.c -o cpu -lm

The files

Next: the two workloads, one at a time — why the GPU loses at n-queens, and why it wins at mandelbrot.

When the GPU loses: n-queens

gpu/queens is N-queens by parallel exhaustive backtracking, N = 17, ported verbatim from upstream. Its main.bend is byte-identical to bend/bench/runtime/queens/main.bend, and its comments are unusually good, which is why this chapter can quote the source rather than guess at it. The code below is that file, quoted by line number.

The shape of the work

The whole bookkeeping is two counters, and a zero for the case where a subtree contributed nothing:

type Stats is Data:
  Stat0{}
  Stats{sols: U32, nodes: U32}

Rows 0–3 are placed up front. batch forks the flat (c0, c1, c2, c3) prefix index space 0..2^d into a balanced tree — a perfectly uniform fork, exactly the shape the previous chapter said the scheduler likes:

def batch(+d: Nat, +i: U32, +m: U32, +nn: U32, +full: U32,
          +bound: U32) -> Stats:
  match d:
    case 0n:
      pfx(i, m, nn, full, bound)
    case 1n+p:
      a b = batch(p, i, m, nn, full, bound) batch(p, U32.add(i, U32.shln(1, p)), m, nn, full, bound)
      smerge(a, b)

smerge adds two Stats pairwise, so the whole tree reduces to one value. Each leaf then decodes its own column quadruple and runs the classic bitmask backtracker over the remaining 13 rows:

def pfx.s3(t: Bool, +nn2: U32, +full: U32, +b3: U32, +c3: U32, +l3: U32,
           +r3: U32) -> Stats:
  match t:
    case False{}:
      Stats{0, 0}
    case True{}:
      +c4 = U32.or(c3, b3)
      +l4 = U32.shl(U32.or(l3, b3))
      +r4 = U32.shr(U32.or(r3, b3))
      +cc = U32.and(full, U32.not(U32.or(c4, U32.or(l4, r4))))
      +cb = U32.and(cc, U32.sub(0, cc))
      +cn = U32.or(c4, cb)
      solve(U32.to_nat(nn2), U32.is_zero(cc), U32.is_eq(cn, full), U32.sub(cc, cb), cn,
        U32.shl(U32.or(l4, cb)), U32.shr(U32.or(r4, cb)),
        c4, l4, r4, full, Stat0{}, 0, 0)

And that second half is where the uniformity ends. solve is the backtracker: one def, fourteen arguments.

def solve(+f: Nat, z: Bool, e: Bool, +sib: U32, +nc: U32, +nl: U32, +nr: U32,
          +cols: U32, +ld: U32, +rd: U32, +full: U32, ret: Stats, sols: U32,
          nodes: U32) -> Stats:

Read them in groups. f, z, e and ret are what the match scrutinizes: a fuel count, two precomputed booleans, and the accumulator. sib is the set of candidate bits this row has not tried yet. nc, nl, nr are the three attack masks for the child row — columns taken, and the two diagonals — and cols, ld, rd are the same three masks one row up, which is what stepping to a sibling needs. full is the row-complete mask, and sols/nodes are the counters. Why the argument list doubles up like that — two sets of three masks, one row apart — is the last section of this chapter.

The case that does the searching:

    case 1n+g False{} False{} Stat0{}:
      +cc = U32.and(full, U32.not(U32.or(nc, U32.or(nl, nr))))
      +cb = U32.and(cc, U32.sub(0, cc))
      +cn = U32.or(nc, cb)
      +b2 = U32.and(sib, U32.sub(0, sib))
      +n2 = U32.or(cols, b2)
      solve(g, U32.is_zero(sib), U32.is_eq(n2, full), U32.sub(sib, b2), n2,
        U32.shl(U32.or(ld, b2)), U32.shr(U32.or(rd, b2)),
        cols, ld, rd, full,
        solve(g, U32.is_zero(cc), U32.is_eq(cn, full), U32.sub(cc, cb), cn,
          U32.shl(U32.or(nl, cb)), U32.shr(U32.or(nr, cb)),
          nc, nl, nr, full, Stat0{}, sols, U32.inc(nodes)), 0, 0)

Two calls to solve, the second one nested inside the first’s argument list. The inner call descends — one candidate bit, cb, peeled off the child’s word cc — and the outer one steps to the sibling set, the bits of sib that are left. That is

the classic bitmask backtracker: descend on the child candidate word (the natural non-tail call), then tail-loop on the sibling set

A branch that gets pruned early returns almost immediately. A branch that does not go deep. Nobody can know in advance which is which, because knowing is the search.

q: Why is this bad on a GPU, when a balanced fork tree is good?

Because the fork is only the entry to the work, not the work. The GPU issues one instruction across many lanes at once, so lanes doing different things serialize — which is exactly what upstream means by divergent work. A CPU core is built for this: it predicts, reorders, and caches its way through irregular control flow. The GPU has no such machinery, because it was designed to never need it.

The numbers

Three runs each, checksum 2063750025 in every configuration — the same computation on both devices.

Subtracting the ~85 ms entry cost from the previous chapter, the GPU spends about 1.29 s on the search itself against 0.855 s on ten cores.

The GPU is genuinely slower here, by a factor of about 1.5, and unlike the pow2 result this is not an artefact of the door charge. It is the one workload in this repository where the guide’s sentence —

divergent work like n-queens stays faster on the CPU

— is doing real work rather than being a truism.

Note also what eleven cores do for the CPU side: 6.09 s down to 0.855 s is a 7.1× speedup on 10 cores. A branchy search is what fork-join is for.

What this program had to do to be writable at all

The source’s header comment documents three Bend-level workarounds, and all three are consequences of the chapters before this one. Look again at that nested call — all three are visible in those twelve lines, which is what makes this the best place in the book to watch those limits operating on real code rather than on a probe.

Every decision boolean is computed by the caller.

a match scrutinizes only a parameter, so every decision bool is computed by the CALLER and passed as an argument: solve receives z = is_zero(cand) and e = is_eq(nc, full) with the peeled words, and each self-call site precomputes the next level’s words

The inner call’s second and third arguments are U32.is_zero(cc) and U32.is_eq(cn, full). Both are the answers a match would like to compute for itself, and neither is computed inside solve — they arrive as values, because this is the arrays chapter’s rule — a match cannot scrutinize a computed value — showing up as a calling convention. Note the cost: the arguments are threaded one level ahead of where they are used, so the code reads inside-out.

No call result is ever destructured in place.

the child’s Stats result rides into the sibling call as the acc argument, so no call result is ever destructured in place

That nesting is the rule in action. solve wants to add up the Stats{sols, nodes} from a child call and from a sibling call. Taking the child’s result apart to read its two fields is exactly what Bend refuses, so instead the inner call’s result is passed whole as the outer call’s ret argument, and the counters ride in as ordinary arguments — 0, 0 at the bottom of the descent, and accumulated back up through the recursion.

The recursion rides on a fuel argument.

solve is ONE def and its recursion is structural: the shrinking candidate word is not a structure the checker can see, so a Nat fuel rides ahead of every self-call (match f, recurse on its pred g)

The numbers chapter’s rule. The search does terminate, but it does not shrink a structural argument — a bitmask is not a structure the termination checker can follow. So solve carries a Nat that the checker can watch go down: case 1n+g is the pattern, and every self-call passes g. The comment goes to the trouble of proving the fuel is never exhausted (the initial call seeds n², which exceeds the true frame bound (n-3)(n-2)+1 for every n ≥ 5). The fuel is not there for the algorithm. It is there for the type checker — and the cost is a parameter that exists only to be decremented.

Three different chapters’ rules, in one real program, each written down by whoever ported it because they had to.

Sizes

main calls run!(17n, size(), limit()) — N = 17, limit = 11730:

def run(+d: Nat, +n: U32, +lim: U32) -> U32:
  +nnnn = sq(sq(n))
  full = U32.sub(U32.shln(1, U32.to_nat(n)), 1)
  # bound = min-like clamp: lim when lim < n^4, else n^4
  run.fin(batch(d, 0, U32.sub(U32.shln(1, d), 1), n, full,
    sel(b2u(U32.is_lt(lim, nnnn)), nnnn, lim)))

# small: run!(10n, 5, 625) expect 774553824; big expect 2063750025
def main() -> IO(Unit):
  IO.print(U32.show(run!(17n, size(), limit())))

The prefix mask is 2^d - 1 where d is the first argument, so lowering d shrinks the prefix space. Upstream hard-codes 131071; here it is threaded through batch, which is what makes the small configuration (d = 10, n = 5, limit = 625, expected checksum 774553824) reachable.

The files, and how to build them

bend main.bend -o gpu            # -> gpu and gpu.gpu
bend main.bend -o main.c
clang -O2 main.c -o cpu -lm      # CPU only, no Metal linked

Next: the workload where the GPU wins.

When the GPU wins: mandelbrot

gpu/mandelbrot renders the Mandelbrot set at 4096² with histogram equalisation. Its main.bend is byte-identical to upstream’s benchmark, and it is the mirror image of the previous chapter: the same balanced fork tree, but the work at the leaves is uniform, and that turns out to be the whole difference. The code below is that file, quoted by line number.

Why the leaves are uniform

The set is drawn by iterating z ↦ z² + c a fixed number of times per pixel and recording when z escapes. The obvious implementation breaks out of the loop when it escapes — and that is a branch, which makes pixels take different amounts of time, which is the thing that kills the GPU.

So it does not break out. Upstream’s own header says it in a line:

every pixel runs ITERS iterations with no branches (once escaped, sel freezes z rather than jumping out), so the instruction stream is identical for every pixel

The loop that does that is mit — one iteration per match step, ending when the counter runs out rather than when the point escapes:

def mit(n: Nat, +cr: U32, +ci: U32, +zr: U32, +zi: U32, esc: U32,
        it: U32) -> U32:
  match n:
    case 0n:
      it
    case 1n+p:
      +r2 = asr8(U32.mul(zr, zr))
      +i2 = asr8(U32.mul(zi, zi))
      +e2 = U32.or(esc, b2u(U32.is_gt(U32.add(r2, i2), 1024)))
      nzr = U32.add(U32.sub(r2, i2), cr)
      nzi = U32.add(asr8(U32.mul(2, U32.mul(zr, zi))), ci)
      sr = sel(e2, nzr, zr)
      si = sel(e2, nzi, zi)
      mit(p, cr, ci, sr, si, e2, U32.add(it, b2u(U32.is_zero(e2))))

Follow e2: once the escape test |z|² > 1024 has fired, esc stays set forever, because it is or-ed into itself on the next iteration. And e2 never appears in a case, so nothing branches on it. It only decides values:

def sel.go(x: U32, y: U32, z: Bool) -> U32:
  match z:
    case True{}:
      x
    case False{}:
      y

def sel(t: U32, x: U32, y: U32) -> U32:
  sel.go(x, y, U32.is_zero(t))

sel is a select — a conditional value, not a conditional jump. sr and si are the new or the old z, chosen without a jump, and a frozen z stops changing. Every pixel takes the same path through the same instructions; only the data differs.

The escape count is still correct, because the iterations after the escape are wasted work — and wasted work costs nothing to a machine built to run many lanes in lockstep. That is the exact inverse of n-queens. There, the search tree could not be made uniform. Here, it can be made uniform by spending more arithmetic.

The two passes

The render is not one fork. It is two, plus something in between, and each pass has a type of its own:

type Hs is Data:
  Hl{h0: U32, h1: U32, h2: U32, h3: U32, h4: U32, h5: U32, h6: U32, h7: U32}

type Lut is Data:
  Lut{k0: U32, k1: U32, k2: U32, k3: U32, k4: U32, k5: U32, k6: U32, k7: U32}

Hs is one histogram — eight scalar buckets, one per eighth of the iteration budget:

# escape time -> one of 8 buckets, knob-stable: (it*8)/ITERS clamped
def bkt(it: U32, tn: Nat) -> U32:
  +bq = U32.div(U32.mul(it, 8), U32.from_nat(tn))
  sel(b2u(U32.is_gt(bq, 7)), bq, 7)

1. Histogram. Fork 2^18 blocks of 64 pixels; each block sorts its escape counts into those 8 buckets and the buckets are merged pairwise up the fork tree:

def hfold(+d: Nat, +i: U32, +tn: Nat) -> Hs:
  match d:
    case 0n:
      hchunk(64n, i, tn, 0, 0, 0, 0, 0, 0, 0, 0)
    case 1n+p:
      a b = hfold(p, i, tn) hfold(p, U32.add(i, U32.shln(64, p)), tn)
      hzip(a, b)

hfold is the same depth-d fork as batch in the previous chapter, and hzip is its smerge: one bucket set added to another, pairwise, all the way up.

2. The CDF. A serial pass turning the root histogram into an equalisation lookup table. Small, sequential, unavoidable — and worth reading, because it is the one piece of this program with no fork in it at all:

# histogram equalization: LUT k = cdf(k) scaled to 0..255
def cdf(h: Hs) -> Lut:
  match h:
    case Hl{+h0, h1, h2, h3, h4, h5, h6, h7}:
      +c1 = U32.add(h0, h1)
      +c2 = U32.add(c1, h2)
      +c3 = U32.add(c2, h3)
      +c4 = U32.add(c3, h4)
      +c5 = U32.add(c4, h5)
      +c6 = U32.add(c5, h6)
      +c7 = U32.add(c6, h7)
      Lut{U32.div(U32.mul(h0, 255), c7), U32.div(U32.mul(c1, 255), c7), U32.div(U32.mul(c2, 255), c7), U32.div(U32.mul(c3, 255), c7),
          U32.div(U32.mul(c4, 255), c7), U32.div(U32.mul(c5, 255), c7), U32.div(U32.mul(c6, 255), c7), U32.div(U32.mul(c7, 255), c7)}

3. Recolour. Fork again, one leaf per pixel this time, running each pixel back through the lookup table and summing by position:

def rcol(+d: Nat, +i: U32, +tn: Nat, +k0: U32, +k1: U32, +k2: U32, +k3: U32,
         +k4: U32, +k5: U32, +k6: U32, +k7: U32) -> U32:
  match d:
    case 0n:
      rpix(i, tn, k0, k1, k2, k3, k4, k5, k6, k7)
    case 1n+p:
      a b = rcol(p, i, tn, k0, k1, k2, k3, k4, k5, k6, k7) rcol(p, U32.add(i, U32.shln(1, p)), tn, k0, k1, k2, k3, k4, k5, k6, k7)
      U32.add(a, b)

The checksum mixes the lookup table and the recoloured result, so it is sensitive to both passes. That matters — it means a GPU build that silently skipped the recolour would not produce the recorded value.

The numbers

Three runs each, checksum 3101455856 everywhere.

Wall clock says the GPU is about 6× faster than ten cores. That understates it badly, because roughly 85 ms of every GPU run is the entry cost measured in the GPU chapter, and it does not shrink when the work does.

Subtract it and the picture is:

This is the largest GPU win in the repository, and it is worth being precise about why it is not reported as 20×: because a wall-clock number for a program that runs once has to include the door. A real renderer loops over many frames or many scenes and pays it once — at which point this becomes the 20× number.

Two things to know before timing it yourself

The first run is slow. The first measurement of this binary here was 0.226 s, which settled to 0.108 s on repetition — a factor of two. Every GPU number in this book is three runs, and the first is discarded in spirit even where it is printed.

The stderr line is not an error, and you must not filter it out.

bend: compiling the GPU program (... .gpu is missing or stale)

The host binary checks for a kernel and rebuilds it when it cannot find one. If you grep -v that line away while timing, you are timing a different program. The cost is real and it belongs in the number.

Sizes

The source records two configurations:

Both are one call apart:

# small: rend!(2n, 7n) expect 887240761; big rend!(18n, its()) expect 3101455856
def main() -> IO(Unit):
  IO.print(U32.show(rend!(18n, its())))

The two binaries in this directory are the big one. The small one is useful for checking a rebuild — it finishes quickly and still verifies.

The files, and how to build them

bend main.bend -o gpu            # the GPU path, plus a .gpu Metal kernel
bend main.bend -o main.c
clang -O2 main.c -o cpu -lm      # CPU only

A useful sanity check: build the CPU binary yourself and compare. The result here was 70,696 bytes with the same checksum and the same 5.15 s as the committed cpu, which is a decent sign that the generated C is deterministic and that nothing about the measurement depends on which clang invocation you used.

That closes the performance half of the book. What is left is a worked example — Conway’s Life, built slowly enough to see every piece of the machinery, affinity, kinds and the fork included, earn its place — and then the same machinery pointed at a different question: not how fast, but how do you know it is right, without reading the code.

Next: Life the obvious way, and the trap in it.

Life the obvious way, and the trap in it

Time to build something. Conway’s Game of Life is a good choice because everyone already understands it, so all the difficulty is in the language rather than the problem — and because the obvious implementation has a trap in it that does not show up until you measure.

The rules, for completeness: a cell’s eight neighbours are summed. The cell is alive next generation if that sum is 3; it stays as it was if the sum is 2; it dies otherwise.

The world

The grid is a flat List<&2, Nat> of length w × h, holding 0 or 1. Coordinates become an index with y*w + x, and wrapping is done with Nat.mod, so the world is a torus — walk off the right edge and you arrive at the left.

The whole program is here, 120 lines. Four of them are the interesting part:

def nth(+xs: List<&2, Nat>, +i: Nat) -> Nat:
  match xs:
    case Nil{}:
      0n
    case Con{h, t}:
      match i:
        case 0n:
          h
        case 1n+p:
          nth(t, p)

def at(+g: List<&2, Nat>, +w: Nat, +h: Nat, +x: Nat, +y: Nat) -> Nat:
  nth(g, Nat.add(Nat.mul(Nat.mod(y, h), w), Nat.mod(x, w)))

nth walks a list i steps and returns the element. at turns a coordinate into an index and calls it. Then nb calls at eight times, and step calls both at and nb for each cell in the grid.

Run it and you get a glider, which is the standard check that the rules are right:

generation 0        generation 4
.#......            ........
..#.....            ..#.....
###.....            ...#....
........            .###....

Generation 4 is the canonical glider shape, one cell down and to the right of where it started. The logic is correct.

❌ The trap

Look again at at:

nth(g, Nat.add(Nat.mul(Nat.mod(y, h), w), Nat.mod(x, w)))
    #  ^ nth walks, one step per index. Its cost IS the index.

Reading element number 4000 costs 4000 steps. There is no array here, no pointer arithmetic, no skip — a list is a chain and you follow it.

So the cost of computing one cell grows with the size of the grid, and computing the whole grid makes it quadratic. The numbers, sixteen generations on one thread, from ./life_par --threads 1:

The grid grew fourfold and the per-cell cost grew fourfold too. That is the signature: a fixed amount of work per cell would have left the right-hand column flat. The right-hand column doubling with each dimension is the O(n²).

It is worth being precise about what is slow here, because the usual instinct is wrong. It is not the rule, and it is not the neighbour sum. rule is two comparisons. What is slow is finding the cell — and we are doing it eight times per cell, each time from the head of the list.

Why a list and not an array

A reasonable objection: Bend has arrays, arrays have O(1) indexing, so why is this written with a list?

Because each cell needs to read eight neighbours, and the arrays chapter established what that requires: the grid must be reusable, which means Data-kinded, which means List<&2, Nat> — or nothing.

type Array<-T: Type> is Type:        # Type: not copyable
type List<a, -A: Kind(a)> is Kind(a) # &2: copyable

Array is Type, and that is the price it pays for in-place rewrite without copying. In Bend the choice is not “which is faster” but “do I need to read this more than once” — and here the answer is eight times per cell, three generations running.

So this chapter’s code is not a mistake. It is what the type system leaves you when you need random access to something reusable.

Two roads out

The trap is not “lists are slow”. It is that we are indexing at all.

Every cell reads its eight neighbours, and neighbours are exactly the cells adjacent in the layout. If the grid were walked in order, carrying the rows we need instead of jumping to them, no index would ever be computed.

There are two roads out of the trap, and they are not equal. One is cheap to try: keep the engine, throw cores at it. The other changes the work itself. The cheap road is next.

The whole file

import Base

# ============================================================
# Conway's Game of Life
# The grid is a flat List<&2, Nat> of length w*h, holding 0 or 1.
# Coordinate (x,y) -> index y*w + x; out of bounds wraps, so the world is a torus.
# ============================================================

# ---- element i; walking past the end returns 0n ----
def nth(+xs: List<&2, Nat>, +i: Nat) -> Nat:
  match xs:
    case Nil{}:
      0n
    case Con{h, t}:
      match i:
        case 0n:
          h
        case 1n+p:
          nth(t, p)

# ---- coordinate -> value, wrapping ----
def at(+g: List<&2, Nat>, +w: Nat, +h: Nat, +x: Nat, +y: Nat) -> Nat:
  nth(g, Nat.add(Nat.mul(Nat.mod(y, h), w), Nat.mod(x, w)))

# ---- the sum of the eight neighbours ----
def nb(+g: List<&2, Nat>, +w: Nat, +h: Nat, +x: Nat, +y: Nat) -> Nat:
  +xm = Nat.sub(Nat.add(x, w), 1n)
  +ym = Nat.sub(Nat.add(y, h), 1n)
  +xp = Nat.add(x, 1n)
  +yp = Nat.add(y, 1n)
  Nat.add(at(g, w, h, xm, ym),
  Nat.add(at(g, w, h, x, ym),
  Nat.add(at(g, w, h, xp, ym),
  Nat.add(at(g, w, h, xm, y),
  Nat.add(at(g, w, h, xp, y),
  Nat.add(at(g, w, h, xm, yp),
  Nat.add(at(g, w, h, x, yp),
          at(g, w, h, xp, yp))))))))

# ---- the survival rule ----
# exactly 3 neighbours -> alive (whatever it was); exactly 2 -> unchanged; else dead
def rule(+alive: Nat, +n: Nat) -> Nat:
  Bool.pick(Nat, Nat.is_eq(n, 3n), 1n,
    Bool.pick(Nat, Nat.is_eq(n, 2n), alive, 0n))

# ---- the next generation: n cells, starting at index k ----
def step(+g: List<&2, Nat>, +w: Nat, +h: Nat, +n: Nat, +k: Nat) -> List<&2, Nat>:
  match n:
    case 0n:
      Nil{}
    case 1n+p:
      +x = Nat.mod(k, w)
      +y = Nat.div(k, w)
      v = rule(at(g, w, h, x, y), nb(g, w, h, x, y))
      Con{v, step(g, w, h, p, Nat.add(k, 1n))}

# ---- the seed: one glider, at (1,0) (2,1) (0,2) (1,2) (2,2) ----
def hit(+x: Nat, +y: Nat, +a: Nat, +b: Nat) -> Bool:
  Bool.and(Nat.is_eq(x, a), Nat.is_eq(y, b))

def cell0(+w: Nat, +k: Nat) -> Nat:
  +x = Nat.mod(k, w)
  +y = Nat.div(k, w)
  Bool.pick(Nat,
    Bool.or(hit(x, y, 1n, 0n),
    Bool.or(hit(x, y, 2n, 1n),
    Bool.or(hit(x, y, 0n, 2n),
    Bool.or(hit(x, y, 1n, 2n),
            hit(x, y, 2n, 2n))))),
    1n, 0n)

def seed(+w: Nat, +n: Nat, +k: Nat) -> List<&2, Nat>:
  match n:
    case 0n:
      Nil{}
    case 1n+p:
      Con{cell0(w, k), seed(w, p, Nat.add(k, 1n))}

# ---- render as a string, w characters per line ----
def one(+c: U32) -> String:
  SCon{Char.from_u32(c), SNil{}}

def nl() -> String:
  one(10)

def wrap_nl(+k: Nat, +w: Nat) -> String:
  Bool.pick(String, Bool.and(Nat.is_ne(k, 0n), Nat.is_eq(Nat.mod(k, w), 0n)), nl(), SNil{})

def render(+g: List<&2, Nat>, +w: Nat, +k: Nat) -> String:
  match g:
    case Nil{}:
      SNil{}
    case Con{h, t}:
      c = Bool.pick(U32, Nat.is_eq(h, 0n), 46, 35)
      String.append(wrap_nl(k, w), String.append(one(c), render(t, w, Nat.add(k, 1n))))

# ---- evolve gens generations. gens stays leftmost: the checker wants the shrinking arg first ----
def evolve(
  +gens: Nat, +g: List<&2, Nat>, +w: Nat, +h: Nat, +n: Nat, +k: Nat
) -> List<&2, Nat>:
  match gens:
    case 0n:
      g
    case 1n+q:
      evolve(q, step(g, w, h, n, k), w, h, n, k)

def gen_n(+w: Nat, +h: Nat, +gens: Nat) -> String:
  render(evolve(gens, seed(w, Nat.mul(w, h), 0n), w, h, Nat.mul(w, h), 0n), w, 0n)

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print("generation 0\n")
    IO.print(gen_n(8n, 8n, 0n))
    IO.print("\ngeneration 1\n")
    IO.print(gen_n(8n, 8n, 1n))
    IO.print("\ngeneration 2\n")
    IO.print(gen_n(8n, 8n, 2n))
    IO.print("\ngeneration 4\n")
    IO.print(gen_n(8n, 8n, 4n))
    IO.print("\n")

bend life.bend        # the interpreter is enough; this one prints, it does not benchmark

Next: the obvious engine on ten cores.

Life on ten cores

The previous chapter measured the obvious engine and found the trap: every cell pays eight list walks, each as long as the cell’s position, and the whole engine is quadratic. Before changing anything about the algorithm, there is an obvious move left. You have read how Bend forks, and the machine has more than one core. Keep the engine, add cores.

This chapter does that, and it is really about two questions that sound easier than they are: what did the cores buy, and how do you know.

You cannot tell by reading it. A parallel let that never gets scheduled and a parallel let that runs perfectly look identical in the source. You cannot tell from the wall clock either. A millisecond count answers the question you asked, and two parts of that question are easy to ask wrong: what went into the window, and which implementation was running.

The shape

The naive engine gets parallelised by renaming its step function to block and using it as a leaf — one task computes blk consecutive cells — then hanging a balanced binary tree over the leaves:

def tree_cells(+d: Nat, +g: List<&2, Nat>, +w: Nat, +h: Nat, +blk: Nat, +k: Nat) -> List<&2, Nat>:
  match d:
    case 0n:
      block(g, w, h, blk, k)
    case 1n+p:
      a b = tree_cells(p, g, w, h, blk, k) tree_cells(p, g, w, h, blk, Nat.add(k, cells_in(p, blk)))
      app(a, b)

cells_in(d, blk) is 2^d × blk, by the same recursion the tree uses, so 2^d × blk = w × h covers the grid: blk is a granularity knob and everything else stays fixed. The a b = ... line is the fork; app(a, b) is the join.

The evidence

Here is the honest signature of real parallelism: watch user while real falls.

user goes up while real goes down. The total work is unchanged — the same additions, the same comparisons — but it is being spent on more cores at once, so the wall clock is shorter and the CPU total is larger (the extra is scheduling overhead). A program that is not parallel shows user ≈ real at every thread count. The fork-join chapter showed this signature on a toy; this is the same read on our own engine.

This is the check to reach for, and it is cheap: time ./binary --threads 1 and time ./binary --threads 10, then compare the two columns. It asks one thing of you first — a window that contains the parallel work and nothing else — and that is the next section.

What to time

Time only the region you are claiming is parallel. Nothing else belongs in the window.

./life_par is a good test of that habit, because one command runs five benchmarks and only three of them fork. The two naive, no fork cases are depth-zero — one leaf for the whole grid — so they cannot parallelise at all, and their own output says so: 7,940 ms at one thread, 7,745 ms at ten.

Both readings below are of the same five benchmarks, and both are correct:

That is /usr/bin/time -p ./life_par --threads 1 against --threads 10. The gap between the two rows is the two serial cases: 8.4 s of the process, and 8.2 s of it at ten threads. A benchmark that measures two things reports neither, and the fix is not a better benchmark but a narrower one.

So the rest of this chapter measures in that narrow window. blk=1 on its own is 2.6× at ten threads; the process it lives in is 1.35×.

Granularity

With the window narrowed to the fork-join work, here is the knob. 64×64, four generations, one thread and ten:

At one thread the three settings sit within about 15% of each other. At ten they spread by more than half a second, and the direction is the opposite of the usual advice: fewer, larger tasks win — blk=16 beats blk=1 by 48 ms at ten threads.

The reason is the join. app is serial work — concatenating two lists is one thread’s job — and every internal node of the tree is a join. blk=1 makes a 4096-leaf tree, which means 4,095 joins; blk=16 makes 255. At ten threads, each join parks one worker while its partner concatenates, so every join is a small stretch of the schedule where a core idles. At one thread there are no partners to park, the joins are just work, and the knob barely matters. The knob only matters in the regime it was invented for.

This is the guide’s second promise doing its work:

The calls are independent. They run in roughly the same time. […] if one call finishes before the other, the speedup will be sub-ideal.

And it leaves a rule worth keeping verbatim:

A parallel number is a property of an implementation, not of a language. Record them together or you will attribute the next one to the wrong cause.

This exact tree — tree_cells, block, cells_in — is the one the last part of this book proves equal to a plain serial scan. The shape you just measured is the shape that gets proved.

So: is it actually parallel?

Yes — 3.1× on ten cores, and user climbing from 5.6 s to 12.4 s says so independently of the wall clock. But 3.1× out of 10 is about 31% efficiency, and both reasons are now visible rather than mysterious. The joins are serial. And the leaves are unbalanceable: the work behind every cell is a walk whose length is the cell’s position, so “roughly the same time” — the guide’s second promise — is broken in every leaf at once. The cores multiply what the algorithm hands them, and this algorithm hands them walks of a thousand different lengths.

There is another road out of the trap, besides cores: make every cell cost the same, small, constant amount of work, with no walk to a position at all. That is the next chapter, and it is worth about a factor of 1,600.

Running it

bend life_par.bend -o life_par
./life_par --threads 1
./life_par --threads 10

The binary also prints the naive no-fork baseline and the row-window head-to-head, so the whole comparison is reproducible from one command.

Next: the same game in O(n).

Life in O(n), by rows

Life the obvious way measured where the time goes: not the rule, and not the neighbour sum, but reaching a cell at all — eight walks per cell, each as long as the cell’s position. Life on ten cores kept that engine and threw cores at it: 3.1×, and the ceiling was visible — the joins are serial, and no scheduler can balance walks of a thousand different lengths.

The other road out of the trap is to change the shape of the work. This chapter removes the index, and it is worth stating up front what shape it is aiming at, because every choice below follows from it:

• no position is ever computed — the walk is the position, so nothing costs what an index costs;
• every cell costs the same constant number of steps — a fixed tax per cell is what makes a generation O(n) instead of O(n²);
• the work is uniform — every cell costing the same is exactly what a fork needs: split the board, get equal halves. The eight different-length walks were the one property the scheduler could not use.

The first two are the speedup. The third is what makes the engine parallelisable — and at the end of this chapter the cores are put back on, to measure what uniformity is worth.

The plan: two passes, not one box

The neighbours are the 3×3 box around the cell, minus the centre: nine cells to account for.

A box does not have to be summed in one go. It is three columns, and it is also three rows, and either way it comes apart into two one-dimensional passes — first collapse three rows into one number per column, then add three neighbouring numbers:

    3×3 box   ──▶   3 numbers   ──▶   1 number
              three rows per     three columns,
              column              one window

Each pass is a walk: position by position, no jumps. That is the whole idea, and the rest of this chapter is the two passes and what they need at the edges.

One consequence is worth stating before any of it, because it is the thing that looks wrong at first: the intermediate row holds one number per column — w of them, not w × h. By the time the second pass runs, each column has already collapsed into a sum, and a sum is all the second pass wants.

The order is bookkeeping, not correctness. Rows first needs one scratch row; columns first would need three.

Pass one: three rows into one

The cell is (x, y), with x counting along a row and y counting rows. This chapter builds one output row at a time — call it y — so y is fixed and x ranges along the row. Doing it for every row is the row rotation, later on.

Only three rows can matter, because a neighbour is never further than one row away:

row y-2  ────────────────  no neighbour of row y lives here
row y-1  ┐
row y    ├─  every neighbour of a cell in row y is in these three rows
row y+1  ┘
row y+2  ────────────────  no neighbour of row y lives here

So the height of the board never comes up again. Not because the trick avoids h, but because h was never part of the question: a cell has eight neighbours whether the grid is 17 rows tall or 17,000.

Add those three rows, position by position, into a scratch row s_y:

s_y[x] = prev[x] + cur[x] + next[x]

• prev, cur and next are rows y-1, y and y+1 — three different rows, the same column. They differ in y, not in x, and each is a List<Nat> of length w.
• s_y is a List<Nat> of length w: one entry per column.
• s_y[x] is a single Nat — three cells added into one number.

Six columns, so the whole window fits on the page. The boards measured below are far bigger; the width changes nothing:

          x=0  x=1  x=2  x=3  x=4  x=5
prev        0    1    0    0    1    0
cur         1    0    1    1    0    0
next        0    0    1    0    1    1
            │    │    │    │    │    │      one column at a time:
            ▼    ▼    ▼    ▼    ▼    ▼      0+1+0, 1+0+0, 0+1+1, ...
s_1         1    1    2    1    2    1

s_1[2] = prev[2] + cur[2] + next[2] = 0 + 1 + 1 = 2. No entry can exceed 3, because three cells go into it.

There is one s_y per output row, and the inputs change with the row, so every entry changes with it. Add a fourth row to the same board:

   row 0   0 1 0 0 1 0        s_1 = 1 1 2 1 2 1      from rows 0+1+2
   row 1   1 0 1 1 0 0        s_2 = 2 1 2 2 1 2      from rows 1+2+3
   row 2   0 0 1 0 1 1
   row 3   1 1 0 1 0 1

Two different lists, both correct, each the three-row window of its own row. The code names it s, because inside one call to newrow there is only ever one; this chapter writes s_y because it looks at more than one.

colsum is that formula written as the walk it has to be:

def colsum(
  +p: List<&2, Nat>, +c: List<&2, Nat>, +n: List<&2, Nat>, +acc: List<&2, Nat>
) -> List<&2, Nat>:
  match p:
    case Nil{}:
      rev(acc, Nil{})
    case Con{hp, tp}:
      match c:
        case Nil{}:
          rev(acc, Nil{})
        case Con{hc, tc}:
          match n:
            case Nil{}:
              rev(acc, Nil{})
            case Con{hn, tn}:
              colsum(tp, tc, tn, Con{Nat.add(hp, Nat.add(hc, hn)), acc})

All three rows are matched at once, so the three lists are consumed in lockstep: hp, hc and hn are the three cells at the current position, and the recursive line appends one entry — hp + hc + hn — per position. No position is ever computed; the position is wherever the walk has got to.

Pass two: a three-wide window

Same output row, so still the same s_y. The block’s three columns are x-1, x and x+1, and each of them is already one entry:

   s_y[x-1]  =  prev[x-1] + cur[x-1] + next[x-1]     the block's left column
   s_y[x]    =  prev[x]   + cur[x]   + next[x]       the middle column
   s_y[x+1]  =  prev[x+1] + cur[x+1] + next[x+1]     the right column

A 3×3 block is three columns and nothing else, so those three entries are the whole block. Exactly one of the nine cells is the cell itself — cur[x], which sits inside s_y[x] and in neither of the others — so it comes off once:

s_y[x-1] + s_y[x] + s_y[x+1]              =   all nine cells of the block
s_y[x-1] + s_y[x] + s_y[x+1] - cur[x]     =   the eight neighbours

On the same example, for the cell at x = 2:

   column 1:  prev[1]=1  cur[1]=0  next[1]=0     s_1[1] = 1
   column 2:  prev[2]=0  cur[2]=1  next[2]=1     s_1[2] = 2     ← cur[2] is the cell
   column 3:  prev[3]=0  cur[3]=1  next[3]=0     s_1[3] = 1
                                              ─────────────
                                nine cells  =  1 + 2 + 1  =  4
                 minus the cell itself, cur[2] = 1   →   3 neighbours

That is the neighbour count. Turning the count into the next state is the rule, three lines:

def rule(+alive: Nat, +n: Nat) -> Nat:
  Bool.pick(Nat, Nat.is_eq(n, 3n), 1n,
    Bool.pick(Nat, Nat.is_eq(n, 2n), alive, 0n))

and the whole of pass two is one line of rowstep, which walks a row applying it:

                case Con{hc, tc}:
                  +alive = hc
                  +nb = Nat.sub(Nat.add(hl, Nat.add(hs, hr)), alive)
                  rowstep(tl, ts, tr, tc, Con{rule(alive, nb), acc})

hl, hs and hr are the three heads of the three window lists — that is s_y[x-1], s_y[x] and s_y[x+1] — and hc is cur[x].

Nine cells, three additions and a subtraction, and the board’s size never entered it: eight neighbour offsets always fall in three rows and three columns, whatever w and h are. Size decides only where those columns land once the board wraps — which is what the rest of this chapter is about.

Why the passes have to be walks

nth costs one step per position, which is why the naive engine is quadratic: eight walks per cell, each up to w × h steps long. Count what this version does instead. colsum visits every cell once and adds it. rowstep visits every cell once and does four operations there. So a cell costs a constant number of list steps rather than a walk to its position:

naive    n cells × 8 walks of up to n steps    →  O(n²)
this     n cells × a constant number of steps  →  O(n)

That is why both passes are written as walks rather than as index arithmetic. Neither of them computes a position — they advance three or four lists together, and the position is wherever the walk has got to. And every cell pays the same constant: no cell’s work depends on where it sits, which is the uniformity the last chapter’s scheduler could not find. A fork that splits this work splits it into equal pieces by construction.

The rotations below are what it costs, and they are the honest part of the trade. Each traverses a whole row, so a generation pays O(w) per row — O(n) across the grid, the same order as the pass it enables. Buying an O(n) pass with an O(n) pass is a good trade; the alternative was an O(n) walk inside every cell, once per neighbour.

Walking in circles

The world wraps, so the window has to slide round the end of a row and back to the start. Rotating a list by one position is cheap — move the head to the end:

def rot_l(+xs: List<&2, Nat>) -> List<&2, Nat>:
  match xs:
    case Nil{}:
      Nil{}
    case Con{h, t}:
      app(t, Con{h, Nil{}})

def rot_r(+xs: List<&2, Nat>) -> List<&2, Nat>:
  rev(rot_l(rev(xs, Nil{})), Nil{})

rot_r is defined as reverse, rotate left, reverse again rather than as its own recursion: one rotation primitive to get right, and both are O(w).

newrow is one output row’s worth of work, and it is the two passes in four lines:

def newrow(+p: List<&2, Nat>, +c: List<&2, Nat>, +n: List<&2, Nat>) -> List<&2, Nat>:
  +s = colsum(p, c, n, Nil{})
  rowstep(rot_r(s), s, rot_l(s), c, Nil{})

Build s, then hand rowstep three staggered copies of it: rot_r(s) holds s_y[x-1] at position x, rot_l(s) holds s_y[x+1]. Four lists of the same length — the three window lists and cur — walked in lockstep, so the three terms of the formula are simply the three heads. The window slides by walking; no rotation is ever undone and no position is ever computed.

Rows themselves rotate

The same problem one level up. To produce row y you need rows y-1, y and y+1, and the grid is a list of rows — so the row list rotates too:

def gen(+a: Rows) -> Rows:
  zip3(rows_rotm1(a), a, rows_rot1(a))

zip3 is what walks them:

def zip3(+P: Rows, +C: Rows, +N: Rows) -> Rows:
  match P:
    case RNil{}:
      RNil{}
    case RCons{p, pt}:
      match C:
        case RNil{}:
          RNil{}
        case RCons{c, ct}:
          match N:
            case RNil{}:
              RNil{}
            case RCons{n, nt}:
              RCons{newrow(p, c, n), zip3(pt, ct, nt)}

It takes one row from each of the three staggered lists per step and calls newrow — one call, and therefore one s_y, per output row. The grid is never indexed, at either level: not horizontally within a row, not vertically across rows. A whole generation is two walks of structures that are already in the right order.

Rows is its own type, because a list of lists needs a name:

type Rows is Data:
  RNil{}
  RCons{row: List<&2, Nat>, tail: Rows}

The result

Sixty-four generations, single thread:

Compare the last column with the previous chapter’s:

The naive column multiplies by four when the grid does. This one does not move. Sixty-four times more cells for sixty-four times more time — that is what O(n) looks like, and the flat right-hand column is the evidence.

The head-to-head

Both versions, 64×64, sixteen generations, one thread each:

Roughly sixteen hundred times. Neither version used more than one core.

A caveat on that ratio, since it is the headline number of this chapter. IO.now() has one-millisecond resolution, so the divisor — 5 ms, and sometimes 4 — is three or four ticks wide. Measured across sessions the row-window side reads 4 or 5 ms and the ratio moves between about 1,600× and 2,000×. The order of magnitude is solid; the third significant figure is not. Every ms column in this chapter is subject to the same thing, which is why the 32×32 row is the least trustworthy one — it is four ticks total.

And now the ordering the whole part has been building to is unambiguous. The parallel naive engine, on ten cores, at its best granularity, is still 628 ms for four generations of 64×64. The serial row-window version does sixteen generations in 5 ms. Parallelism is a multiplier on an algorithm. It does not choose one for you.

And the cores

The uniformity promised at the top of this chapter is a claim about shape, and claims about shape are checkable: fork the engine and measure. life_rowpar.bend hangs the same fork-join tree over the row engine, one level up. The leaf is a run of consecutive output rows, the join is rows_app, and blk is rows per leaf — the same knob as the last chapter, turned one level coarser:

# the tree: a leaf is rows3 (blk output rows), the fork is the parallel let,
# the join is rows_app
def tree3(+d: Nat, +P: Row.Rows, +C: Row.Rows, +N: Row.Rows, +blk: Nat) -> Row.Rows:
  match d:
    case 0n:
      rows3(P, C, N, blk)
    case 1n+p:
      a b = tree3(p, P, C, N, blk) tree3(p, rdrop(P, P, rows_in(p, blk)), rdrop(C, C, rows_in(p, blk)), rdrop(N, N, rows_in(p, blk)), blk)
      Row.rows_app(a, b)

def gen_par(+a: Row.Rows, +d: Nat, +blk: Nat) -> Row.Rows:
  tree3(d, Row.rows_rotm1(a), a, Row.rows_rot1(a), blk)

Two details are worth their space. The right half of each fork skips the rows the left half consumed, and rdrop takes its list twice — one copy to walk, one to hand back when the count runs out — because a name cannot be both matched and returned bare. And the clock wraps evolve only: the grid is built and the cells counted outside it, which is the last chapter’s window-narrowing lesson applied to this book’s own benchmark.

256×256, the largest board in the tables above, and 512×512, four times that — sixty-four generations each, two to three runs per cell of the table:

Three findings, all measured:

Four cores buy 1.4×, and it is real. At both sizes, the four-leaf tree on four threads beats the walk on the same thread count by a stable 1.4× (210 against 292 ms; about 1,140 against about 1,560 ms). /usr/bin/time -p over the whole run agrees independently of the internal clock: real falls from 8.9 s to 5.9 s while user rises from 8.9 s to 9.2 s — more CPU spent, less wall clock, the signature from the fork-join chapter.

Ten cores buy nothing over four. Four leaves per generation can keep four cores busy; the other six contend for what is left, and at 256×256 the ten-thread tree is slower than the four-thread one (258-328 ms against 210 ms). Finer trees never win: at 512×512 the 8- and 16-leaf trees lose to the 4-leaf one outright on one and four threads, and on ten the ranges overlap without anything getting ahead. Leaves cost — on one thread the tree is about a third slower than the plain walk, because the fork, the drop walks and the joins are real work — and here the cost outruns the width long before ten cores. The knob has an optimum, and it is narrow.

The multiplier has little left to act on. The performance part of this book as one ladder, same machine, same afternoon: ten cores on the naive engine — 3.1×. The algorithm change — about 1,600×, serial. Four cores on top of that — 1.4×. Every rung is measured, and the order is not negotiable: fix the work first, because afterwards there is almost nothing left for the cores to multiply.

A note on what was traded

The row-window version is not free. It is longer, it needs Rows and its own append and reverse, and it depends on a mathematical identity that is not obvious at a glance. Someone reading colsum for the first time will not see Life in it.

That is the honest cost of the 2,000×: the fast version is a rewrite, not a tuning pass. What makes it defensible is that the rewrite is checkable — the equality of this engine with the naive one is a law with a proof, in the last part of this book.

The file

bend life_row.bend -o life_row
./life_row --threads 1

bend life_rowpar.bend -o life_rowpar
./life_rowpar --threads 4

Next: a bug that type-checks.

A bug that type-checks

The O(n) engine renders a 40×16 grid in well under a millisecond, so the last thing the Life example does with it is none of Life’s business: it wraps the engine in a loop that writes a frame and sleeps. The animation is not the point. The loop is the first time this book calls IO for real, and the renderer goes wrong in a way that nothing between your edit and your terminal objects to — the types pass, the program runs, the output is garbage. One of the two failures this chapter walks into is worth more than the animation it came from.

The loop

def loop(+left: Nat, +k: Nat, +rs: Rows) -> IO(Unit):
  match left:
    case 0n:
      IO.write("\u{1B}[?25h\n")
    case 1n+p:
      do IO<Unit>:
        IO.write(frame(rs))
        IO.sleep(70)
        loop(p, Nat.add(k, 1n), gen(rs))

Write a frame, sleep 70 ms, compute the next generation, repeat. This is the recursion shape every earlier chapter used — match on the shrinking parameter, recurse on the rest — with one difference: the result is no longer a value, it is an effect, IO(Unit), a program that touches the world. The shrinking parameter — generations remaining — is leftmost, as the termination checker requires. IO.write writes exactly the string; IO.print would append a newline, which for a frame you have already ended with one is a stray blank line per generation.

The Effects part picks this up and takes it apart. Here it only has to be recognisable.

There is no \e

The frame is text, and text on a terminal starts with escape characters. Bend’s string escapes are:

\n  \t  \r  \0  \\  \'  \"  \u{...}

There is no \e and no \x1b. ESC is \u{1B}. And \033 does not error — it parses as \0 followed by a literal 33, giving you a NUL byte and the characters “33” in your output, which is a much worse failure than a rejected program.

The rendering strategy itself needs one sentence: the first frame hides the cursor, and every frame prepends \u{1B}[H — cursor to the top-left — and overwrites in place. Clearing the whole screen each frame repaints it and flickers; overwriting does not.

The bug

Building a frame by appending cell by cell would be O(frame²) — each append copies its left argument, and the left argument keeps growing. So the renderer builds backwards and reverses once at the end:

framerev:  accumulate each row onto the front of the accumulator
frame:     String.reverse once, then prepend the cursor-home escape

One reversal, O(frame) total. But String.reverse reverses characters, and a cell is two characters ("██" or " ").

The first version reversed at two levels — once per row and once for the whole frame — so every row was flipped twice and the result came out mirrored:

y coordinates all correct, x became 39 - x

That signature is what gave it away. A whole-grid mirror with one axis intact points at per-row reversal, not at the pattern or the neighbour logic.

The cost of fixing it is a constraint that now has to hold forever: every cell must be a palindrome. "██" and " " both are, so reversing the character stream reverses the cell order correctly. Change a cell to "▐█" — a perfectly reasonable thing to do — and each row flips internally. That was measured: a 4×4 glider renders as

OXOX][][          instead of     []XO[][]
][][OX][                         [][]XO[]

Both are String, both type-check, both run. The type system has nothing to say about it.

The mechanism, written out because it is easy to get backwards: rowrev appends cell(h) before the accumulator, so it reverses the order of cells and never touches the inside of one. The single reverse in frame flips characters. Composing them gives

reverse (rowrev r)  ==  map reverse (map cell r)

so a row only comes out right when each cell equals its own character-reversal. The palindrome property is not a style note. It is the precondition of the O(frame) optimisation, and in the last part of this book it stops being a comment and becomes a theorem: LIFE_ANIM_PROOF.bend has a lemma called cell_pal, and without it the law does not hold.

Checking it without eyes

“It looks right” is not a check, and a 22-second animation is not something to re-run to compare. So the three patterns in the grid were chosen because each has a distinguishable behaviour — the glider moves one cell diagonally every four generations, the blinker alternates horizontal and vertical, the block does nothing — and the frames were decoded and measured, not watched. The glider’s live cells did shift by exactly (+1,+1) across four generations.

Running it

cd life && bend life_anim.bend

320 generations × 70 ms ≈ 22 seconds. Both backends work; the compiled one is smoother. One thing was confirmed before the animation was worth writing: the output streams — bytes appear from the first seconds and grow roughly linearly, measured, native-compiled. If the runtime buffered, the first 21 seconds would be a blank screen and the last second a mess; that would have killed the whole idea, so it was checked rather than suspected.

To change the length or speed, two numbers at the end of life_anim.bend: loop(320n, ...) and IO.sleep(70).

Next: Inside a do block.

Inside a do block

You have been writing do IO<Unit>: since the first chapter, and the book told you to read it as “a block of actions, run in order” and left it there. This chapter is where that is taken apart — not because you need it to write Bend (you do not; the sugar works with no theory behind it), but because the whole design of effects in Bend fits in one page once you see it: there is no sequencing primitive in the language at all, and do is a small amount of sugar over two ordinary defs.

Recall the idea from the first program: an action is a value. IO.print("hi") does not print; it is a recipe whose type is IO(Unit). The question that chapter deferred is: what consumes a recipe? Two defs in Base are the entire answer.

The two defs that run everything

Ask bend base for them:

def IO.pure(-A: Type, x: A) -> IO(A):
  R => k => k(x)

def IO.bind(-A: Type, -B: Type, m: IO(A), f: A -> IO(B)) -> IO(B):
  R => k => m(R, x => f(x, R, k))

Read IO.bind in imperative terms, ignoring the odd shape of its body for a moment: it takes an action m, a function f from the action’s result to the next action, and delivers the result of running m, fed into f. That is sequencing. IO.pure is even simpler: it wraps an ordinary value in an action that, when run, produces it.

Now the odd shape. An IO(A) is a function that takes two arguments:

• R — the type the whole program ultimately produces;
• k — the rest of the program, as a function from the action’s value to that rest.

So IO.bind’s body R => k => m(R, x => f(x, R, k)) says: run m with the same R and a continuation x => f(x, R, k) — that is, hand m’s result to f, and give the result of f the continuation that was meant for us. “Hand this action what comes next” is the whole trick, and it is why a sequence of steps runs top to bottom: the next line literally is the continuation of the previous one. Bend has no sequencing primitive underneath; the appearance of one is manufactured by this plumbing.

What the block compiles into

With those two defs in place, the block syntax can be defined as pure rewriting. From the guide, verified against the compiler by running both sides:

A do M<xs.., R>: block desugars each x : A <- v into M.bind(xs.., A, R, v, x => ..) and each return e into M.pure(xs.., R, e), so any type with those two defs works: IO, Maybe, Result, or your own.

Concretely, this block:

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

means exactly:

def greet(name: String) -> IO(String):
  IO.bind(Unit, String, IO.sleep(1000), _ => IO.pure(String, "Hello, " ++ name))

Two rules, and nothing else in do is magic:

• x : A <- v — run the action v, bind its result to x for the rest of the block. Compiles to IO.bind.
• return e — produce the plain value e as the block’s result. Compiles to IO.pure.

A line that is neither — a bare step like IO.sleep(1000) — binds to a name nobody uses, which is why the block reads as “statements”.

The header’s arguments

do IO<Unit>: — three things in that header, none of them decoration:

• IO names the family: it fixes which .bind and .pure the block desugars to.
• Unit, the last argument, is R — the block’s own result type. It is what a return in the block must produce, and the desugaring passes it as the last argument of every bind it generates.
• any leading arguments (xs..) are passed along to both, unchanged.

That last rule is not decoration either; Maybe uses it. This def, which reads two strings as numbers and short-circuits on the first failure:

import Base

# The do-block from src/do-blocks.md, with the call the chapter quotes in
# main.  add_strs_bad.bend is the same def on input that will not parse.

def add_strs(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() -> IO(Unit):
  do IO<Unit>:
    IO.print(Maybe.show(~&2, ~U32, ~U32.show, add_strs("42", "0")))

runs as Maybe.bind(&2, U32, U32, U32.read(a), x => ...) — the quantity &2 rides along into both calls because the header carries it. The successful and failing runs, measured — the second is basics/add_strs_bad.bend, the same def called with a string that is not a number:

$ bend add_strs.bend
Some(42)
$ bend add_strs_bad.bend
None

The empty result came from Maybe.bind’s own definition — its case None{}: None{} skips the continuation entirely, which is the whole of “fail fast” in one line of match.

What the header is not

Two negative facts, both probed, both worth knowing because each one looks like the opposite from the outside:

• The header is not instantiating a datatype. IO is a function, not a datatype, and there is nothing to instantiate — yet do IO<Unit>: is correct, and do IO(Unit): is refused with expected : '<'. The <> here is the header’s own grammar, the same for every monad; it does not make the header a datatype application. This is the one place the two brackets of the types chapter genuinely part ways.

• The header is not type-checked against the body. When a block has no <- and no return, the desugaring has nothing to emit and the header is erased entirely — this compiles and runs:

  def main() -> IO(Unit):
    do List<Unit>:      # List is a datatype with no .bind
      IO.print("x")
  

  Add one bind and it fails — expected : a defined name, on List.bind — naming the missing def, not the brackets (kept as basics/do_list_bind.bend). The error will tell you exactly what a do-block header is: a name for a .bind/.pure pair, plus arguments for them.

Why the book made you wait for this

Because the two ideas it rests on had to exist first. “An action is a value” is the first chapter’s job, and the machinery that runs those values — the event loop that interleaves computations without threads — is the next chapter’s subject. The desugaring is the seam between them: do manufactures the chain of continuations, and the loop is what drives it. With both ends in place, effects.md can talk about timing instead of syntax.

Next: Effects, and the event loop.

Effects, and the event loop

Every program in this book so far computed a value. This chapter is about programs that do things — print, wait, read a file, open a socket — and about the machine that lets them do those things without threads. Bend calls it IO.

One honest note before starting. The guide’s prose on IO is thin, and its own effects note (bend guide effects) says of itself that an AI wrote it and a human will revise it. So this part of the book came from probes rather than from reading: fx/ in this repository holds them, and its READMEs are the full tables. What follows is what they measured.

The shape at the seam

You have written do IO<Unit>: blocks since the first chapter; this is where their rules were pinned down. Each is a corner where the pure language meets the loop, and each one cost a compile cycle while the probes were written:

None of these is deep. The fourth is the one that generalises: an effectful call is not a value, so it can never be an argument. Every IO needs its own line.

The event loop

The guide states the model in one sentence:

A Bend program is a set of computations interleaved by one event loop, as in Node.js: each runs its pure code (in parallel, on every core) up to its next effect, and one that waits on a socket, a sleep or a channel steps aside for the others.

The probes give that sentence numbers. Two computations, each sleeping 700 ms, forked and joined:

c1 : Chan(U32) <- IO.fork(U32, nap(700))
c2 : Chan(U32) <- IO.fork(U32, nap(700))
r1 : U32 <- IO.join(U32, c1)
r2 : U32 <- IO.join(U32, c2)

Measured: total ms=709. One sleep’s worth of wall clock, two sleeps’ worth of work — the loop really does overlap them, with no threads in sight.

Then the sentence’s second half — “the program ends when every computation is done, or reports a deadlock when the remaining ones all wait” — has a case the guide does not spell out. Main returning is not the program ending.

The second one is the surprise worth keeping: a leftover task turns the whole exit into a deadlock report — the runtime refuses to exit quietly while someone is still waiting. And it prints the same line when everyone is stuck; the two situations are not distinguished. Both exit 1.

Channels

Fork and join are built on channels, and the whole state table is small enough to pin down completely:

Two rows deserve a second look. A full room blocks; it does not refuse. The probe sends twice into a room-1 channel with nobody receiving; the first send answers true, the second never returns, and the program ends as the deadlock above. And closed is not an error: send on a closed channel answers false, recv answers None, and the program continues.

IO.join is the pair done for you: one recv, one close. That makes it sharper than it first looks.

+ch : Chan(U32) <- IO.fork(U32, one())
r1 : U32 <- IO.join(U32, ch)
r2 : U32 <- IO.join(U32, ch)     # the channel is closed now

With the channel marked +, both joins compile, and the second one dies at runtime: IO.join: the channel was closed, exit 1. Without the +, it does not even compile — consumed more than once — which is the affine rule from earlier chapters arriving on schedule. A join consumes the channel; a consumer that wants more values uses Chan.recv directly.

Things that fail

An effect can fail, and Bend makes that a value: the effect answers Result<&1, &1, U32 & String, A> — an error code and message, or the answer. IO.try unwraps it or exits with the error. The exit codes are the machine’s:

The message is strerror and the code is the errno — an exit code is the interface a shell sees, so it is the one the runtime keeps exact. When you want your own, IO.die(A, code, msg) exits with your code and prints your message:

$ bend die.bend
before die
$ echo $?        # 7
custom failure message          # on stderr

and the statements after the die do not run.

A file, up close

File is the effect family worth reading closely, because every fallible effect works the same way: the handle is affine, so every effect on it hands the handle back beside its result. A read is (File & Result<&1, &1, U32 & String, String>) — the file, and what happened.

The unwrap worth memorising, because it is the shape you will write a dozen times:

def r_done(m: File & Result<&1, &1, U32 & String, String>) -> IO(Unit):
  (f, r) = m
  do IO<Unit>:
    s : String <- IO.pass(String, r)
    IO.print("read back: " ++ s)
    File.close(f)

Destructure the pair in a parameter position; IO.pass the Result. This is the same bargain as arrays, for the same reason — one owner at a time — and it buys the same thing: the compiler catches handle misuse. A read after close is not a runtime surprise; it does not compile.

The full roundtrip — write, size, close, reopen, read — is one probe, and it prints size=11, read back: hello, file. The errors are probes too: opening a missing file exits 2; that is the whole File story that matters before you write your own effects.

Two loose ends

IO.args answers the command line, minus the runtime’s own options — and -- is how you draw that line yourself. bend args.bend alpha beta -- gamma passes alpha, beta, gamma: the -- stops Bend’s own option parsing and is not itself passed. argc=3.

The window, audio and graphics effects (App.run and friends) are out of scope here: this book’s probes all run headless. They are the one branch of the effect tree left untested by it, and they are honest about why.

Running it

cd fx/io
bend deadlock.bend          # ❌ the deadlock message, rc 1
bend sleep_par.bend         # ✅ total ms=709
bend close_recv.bend        # ✅ send/recv/close semantics
bend join_twice.bend        # ❌ IO.join: the channel was closed, rc 1

Next: writing an effect of your own.

Writing an effect

Nothing in the previous chapter was privileged. Every effect in Base — the printing, the sleeping, the sockets — is a def whose body is two imports, and effects you write yourself have exactly the same shape. The compiler treats them identically. This chapter writes two from scratch, breaks them on purpose in two different ways, and measures what happens.

The def, and the two files

def Clock.now() -> IO(U32):
  import "./clock.c"
  import "./clock.js"

That is the whole declaration. The .c file serves the compiled lanes, the .js file serves run mode, and the host functions are named after the def — lowercased, dots to underscores. So Clock.now is clock_now in both files. Run it, and it answers:

$ bend clock.bend
ms since boot: 53
$ bend clock.bend -o clock && ./clock
ms since boot: 264817041

Both lanes print a number and call it “ms since boot”. Only one of them means it. The native side calls io_tick(), the machine’s uptime clock — 264817041 milliseconds is the three-odd days this Mac has been up. The run-mode side is JavaScript at heart, and performance.now() counts from the process start, 53 ms ago. Same def, same words in the output, two different quantities.

Here is the part to sit with: nothing checks that the two host files agree. The compiler reads the .c into the native build and the .js into run mode, and never compares them. The delta across a sleeping program matches in both lanes (303 ms for a 300 ms sleep) — they agree about rate and disagree about origin, and the only thing that ever noticed was a probe that printed both.

The C side

Term clock_now_run(Env e, Term* f, IoWork* w) {
  return (Term)(uint32_t)(io_tick() / 1000000ull);
}

static void __attribute__((constructor)) clock_now_use(void) {
  io_eff(CID_CLOCK_NOW, clock_now_run, 0);
}

The compiler splices your .c into the program’s C source after the runtime, so the runtime’s symbols are in scope. The def’s arguments arrive in f in order — a U32 is (u32)f[0], a String is taken with io_cstr(e, f[0], &n) and must be freed, a handle comes back with io_hand_v. The answer is a term: a number is (Term)n, Unit is term_pak(CID_UNIT, 0), a string is io_str(e, p, n), and a fallible answer is io_done(e, v) or io_fail(e, code, NULL). The constructor registers everything with one line — CID_CLOCK_NOW is the def’s name uppercased, dots to underscores — and the last argument of io_eff is the need: 0 runs the call at once, IO_TIME parks it for f[0] milliseconds, IO_READ until a handle is readable.

Two probes beyond clock show this is not a toy interface: Shout.upper and Str.repeat2, effects that exist nowhere in Base, work in all three lanes (run mode, native, and -o x.js plus bun), and strings cross the boundary byte-exact — héllo·世界 in, identical bytes out, in both lanes.

The JS side

function clock_now() {
  return Math.floor(performance.now()) >>> 0;
}

The compiler finds the function by name. A need is a second function, clock_now_need, returning {time: true} or {read: true}; a blocking call takes one more argument and parks with io_park_on. libc is reachable through bun:ffi for the cases that need it (io_sys(): read, recv, poll, errno).

Blocking without stalling

The loop is single and sacred: an effect that blocks it stops every other computation. The runtime’s answer is io_work — run the waiting on a helper thread, come back on the loop when it is done. The probe is a 1000 ms busy call, with a ticker forked beside it:

tick 300
tick 600
tick 900
busy done after 1010 ms

The ticks fire during the work. A custom blocking effect, written by hand in twenty lines of C, does not stall the event loop; the JS lane gets the same behavior from a need. That is the mechanism to reach for whenever an effect would otherwise wait — and the reason file_read.c and tcp_recv.c in bend2/effs/ are worth reading before writing anything slower than a think.

Two ways to get it wrong

Both lanes have their own host file, so both have their own way to be wrong, and the mistakes are invisible from the other side:

Neither error is caught by the compiler, and neither can be: the host files are outside the language. The practical rule is the same one the races chapter gave for threads — test both lanes for anything with a custom effect, because each one is someone else’s program.

What the compiler still will not do for you

Three more edges, from the same probes and from upstream’s own list:

• No ABI. “The C side tracks the exact compiler version: the names above are the runtime’s internals, and a release may rename any of them. There is no ABI promise. Rebuild your effects with every update.” (the guide’s effects note, about itself.)

• No custom handle types. File, Socket, Window are handle types that only Base may declare; a custom effect speaks through them but cannot introduce its own (WONTFIX.txt, under DESIGN). The reason is consistency of the affine story: a handle is a one-owner value, and the language is not yet ready to let user code mint one.

• An output name may not collide with the program’s own files:

  $ bend shout_repeat.bend -o shout_upper.c
  bend: -o shout_upper.c is a file the program reads, or a directory
  

  — refused, and the file is left untouched.

Lazy, and strict

One last measurement, because it is about everything above. Upstream keeps it as WONTFIX #775: bend file.bend runs a pure main lazily, compiled lanes are strict. Put a 200-million-step computation in a dead argument — one the callee never uses:

Same value, different cost. The rule that generalises past this probe: run mode is for correctness, a compiled binary is the truth about cost — a distinction the parallel chapters met from the other side.

Running it

cd fx/custom
bend shout_repeat.bend    # ✅ two effects that are not in Base, three lanes green
bend busy.bend            # ✅ watch the ticks land during the work
bend clock.bend           # ✅ then: bend clock.bend -o clock && ./clock

The effect, all three files

import Base

# The effect from the guide's EFFECTS.md, as written there.  Measured: the C
# side returns milliseconds since boot, the JS side milliseconds since the
# process started -- the same def, two lanes, two different quantities.
def Clock.now() -> IO(U32):
  import "./clock.c"
  import "./clock.js"

def main() -> IO(Unit):
  do IO<Unit>:
    t : U32 <- Clock.now()
    IO.print("ms since boot: " ++ U32.show(t))

Term clock_now_run(Env e, Term* f, IoWork* w) {
  return (Term)(uint32_t)(io_tick() / 1000000ull);
}

static void __attribute__((constructor)) clock_now_use(void) {
  io_eff(CID_CLOCK_NOW, clock_now_run, 0);
}

function clock_now() {
  return Math.floor(performance.now()) >>> 0;
}

Next: turning a belief into a compiler check.

Your first law and proof

The last chapters left two claims dangling.

The first is from Life on ten cores. We said the fork-join tree computes the same cells as the sequential loop. Our evidence was running both and counting live cells — live=5 every time. That is evidence about the handful of grids we happened to try. It is not a statement about the code.

The second is from A bug that type-checks. The renderer only works if every cell is a palindrome, and that fact lives in a comment above cell. Change "██" to "▐█" some day — the chapter’s own words, “a perfectly reasonable thing to do” — and each row flips internally. Nothing between your edit and your terminal will object.

Both claims are real, both are load-bearing, and both are the kind that break silently. Bend has a facility for exactly them: you write the claim down in a form the compiler reads, the compiler refuses to build until the claim is proved, and it refuses again the moment an edit makes the proof stop working.

That facility is also the reason this language exists. What Bend 2 is quotes the pitch: code written by machines, which you will not read, and which therefore has to be checked instead of reviewed. The type checker already covers one half of that — a machine writes a program, and the types hold. Laws and proofs are the other half: a machine writes a program, and the fact that it computes what you asked holds too. That bet is about a future this book does not try to test. What it tests is the mechanism — and the mechanism starts here, on claims you have already made yourself.

One thing to say before the first definition, because it is the question a tutorial owes you: no law is required to write a Bend program. Every chapter so far ran without one, and the compiler never asked. You reach for a law when a claim has three properties at once:

• it is load-bearing — the program is wrong, not merely different, if it breaks;
• it is not already held by a type — “this function returns a String” is a claim too, and the type checker has that one;
• a test can only sample it — three grids out of infinitely many, one rendering run out of a million.

The palindrome constraint and the parallel-tree equality are both that shape, and they are what the rest of this part is spent on. Three chapters: how to write a law and a proof (this one), what they cost (the next), and what the gate actually guarantees (the last).

The words, first

Four words carry everything below, and they are worth pinning down before anything else is said.

A proposition is a claim. Here is one about a number x:

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

Read it as a sentence: the value of Nat.add(x, 0n) is the value x. It looks like a boolean test; it is not one. It is a type — the type “these two terms are the same Nat”. Hold that thought for one paragraph.

A proof is a value of that type. So writing a proof is not a separate activity with its own language: because the claim is a type, a proof is an ordinary def — checked exactly the way every def in this book was checked, against its type. No tactics, no separate proof editor.

A law is a proposition that has been given a name and declared as an obligation:

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

The for line introduces the variable the claim is about — for x: Nat reads “for every x of type Nat”. While no proof exists, the law is an open claim, and the compiler reports it as one when you run the file.

A lemma is a proof whose job is to be quoted inside other proofs. The word names a role, not a mechanism: any proof can be quoted, and the small facts that get quoted are the ones everyone calls lemmas.

(The propositions in this book are all equations. A proposition can be any type at all; equations are what these claims needed.)

Why any of this works is an idea borrowed from proof assistants — Lean, Rocq — and you are not expected to have met one. One paragraph. In that tradition a claim and a type are the same notion: a proposition is a type, and a proof is a term of that type. Bend takes the idea as its own, which is why the machinery checking your claims is the same type checker that has been checking your programs all along — and why checking here is as fast as type checking here, rather than the minutes a dedicated proof assistant might take.

The smallest law

A law with no variables at all. Two plus two is four:

import Base

law two_plus_two:
  {Nat.add(2n, 2n) == 4n : Nat}

Put the claim on its own in a file and run it. The compiler says precisely what is missing:

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

That is what “open claim” means mechanically: the file does not compile until a proof exists. Here is the proof. It is one line.

def two_plus_two():
  {==}

Nothing connects the two blocks except the name. A def with no return type whose name is a law is the proof of that law — no import, annotation or registration. The connection is strict enough that the reverse is enforced too: a def named after a law may not carry a return type at all, because the law already supplies it.

# ❌ a fill with its own return type -- rejected
def two_plus_two() -> {Nat.add(2n, 2n) == 4n : Nat}:

Error:
- expected : ':'
- observed : '-'

(This rejection and the {==} refusal further down are kept as runnable files under laws/ — the errors are indexed in the appendix.) The open claim is a file too: laws/two_plus_two_open.bend, which is two_plus_two.bend before the proof line is added.

Put the two lines in one file — as laws/two_plus_two.bend is — and the open claim is closed:

$ bend two_plus_two.bend
All terms check.

{==} is the proof of {x == x}: “both sides are the same term”. It closes this goal because the checker computes — Nat.add(2n, 2n) reduces to 4n, the goal becomes {4n == 4n}, and the two sides are literally identical. When a goal is not closing and you want to see exactly what the checker is looking at, replace the body with ?anything:

def two_plus_two():
  ?goal

Error:
- expected : {4n == 4n : Nat}
- observed : ?goal

The expected line is the goal in the form it has right now — note that it reads 4n == 4n: the computation already happened, and this is what remains to be said. Keep this instrument nearby; it answers “what do I owe?” at any point in a proof. The second instrument is ?TODO, a hole that reports itself as 1 TODO found — the same message as an unfilled law.

The first proof with a variable

two_plus_two proves nothing interesting, because the checker can compute both of its sides. Interesting claims have variables in them — like the first fact the Life proof needed, which you can now derive for yourself:

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

For every x: x + 0 is x. Try the one-liner:

def add_zero(x):
  {==}

❌ The compiler refuses:

Error:
- expected : Nat.add(x, 0n)
- observed : x

Read the complaint: {==} demanded that the two sides be the same term, and they are not, because one of them cannot even run. Nat.add matches on its first argument, and that argument is the unknown x — there is nothing to match, so the addition is stuck and sits in the goal unevaluated. (Note also that the fill takes the law’s binder as its parameter, left untyped: the law already says x: Nat, and the def does not have to say it again.)

That one mechanical fact — which argument a function matches on decides when it can compute — matters more than any other in this part of the book.

To prove a claim “for every x”, you look at how the value can be built. Nat has two ways to be: zero, or one-plus-something-smaller. So the proof has two cases, and “look at how the value is built” is spelled match:

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

Case 0n. Both sides compute — Nat.add(0n, 0n) is 0n — so {==} closes it.

Case 1n+p. Here x is one more than a smaller number p, and the goal is now {1n+Nat.add(p, 0n) == 1n+p}: the + 0 is still stuck, this time on p. The move to look at twice is the line quoting add_zero itself, at p:

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

Calling the proof you are currently writing, on a smaller value, is induction — and the “smaller” requirement is not new: it is the decreasing argument rule from Numbers and patterns, applied to the proof’s own recursive call. p is what 1n+p is made of, so it shrinks, and the compiler is satisfied for the same reason it was satisfied by every recursive function in this book.

What the line does: add_zero(p) is the statement “p + 0 is p”, and the rewrite uses it to replace the p on the goal’s right — the spot marked _ — with Nat.add(p, 0n). The right side becomes 1n+Nat.add(p, 0n), identical to the left, and {==} closes the case.

Dwell on that direction for a second, because it is the one thing in the mechanics that surprises everyone: the rewrite made the goal bigger, not smaller. % does not simplify. It moves the goal toward a shape you choose when you write the lemma. The rule is stated in full below, but you have now seen it work.

And that is the whole toolkit. {==} is the only axiom; % is the only rule; every proof in this book, however long, is those two moves repeated — move one side until it equals the other, one lemma at a time.

Two containers for a proof

A proof can be kept in two ways, and the difference is when you commit to the claim, not how the proof is checked.

The law form — the claim is declared, and the proof fills it in:

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

def add_zero(x):
  ...           # the match you just wrote

The claim is an obligation from the moment it is written: while the proof is missing, the file reports 1 TODO found.

The plain-def form — no law anywhere, just a fact:

def add_zero(a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
  ...           # same match, same two cases

Same proof, one line different: the proposition appears as the def’s return type and has no name in the file. Nothing fails while it does not exist — and once it exists, it can be quoted with % like any law’s proof.

The law form is for claims that must not be forgotten: requirements, stated up front, that fail the build until they are filled. The plain-def form is for facts discovered while proving something else — which is what the word lemma is for in practice. The Life proof files use both, and the division is visible in them: tree_is_serial is a law, while add_zero and add_assoc are plain defs, written on the spot when the proof needed them.

Bend’s convention for a project puts the two forms in two files at the root: LAWS.bend states the laws — written when the requirement is stated, the human’s file — and PROOF.bend imports it and holds the fills plus any helper lemmas. bend PROOF.bend is the gate: it answers All terms check. only when every law is filled and every proof holds. (The Life files follow the convention with a subject prefix — LIFE_PAR_LAWS.bend, LIFE_PAR_PROOF.bend — because this repository proves things about more than one subject.)

The claim we actually made

Now the dangling claim from the parallel chapter, written as a law:

law tree_is_serial:
  for +d: Nat
  for +g: List<&2, Nat>
  for +w: Nat
  for +h: Nat
  for +blk: Nat
  for +k: Nat
  {Par.tree_cells(d, g, w, h, blk, k) == Par.block(g, w, h, Par.cells_in(d, blk), k) : List<&2, Nat>}

Read it as a sentence. For any depth, grid, width, height, block size and start index: the fork-join tree produces exactly the list that one sequential loop over the same range produces.

(The binders carry the same quantity marks as anywhere else — for +d says that the proof may consume d more than once; choosing them is the next chapter’s subject, so write them as the example does until then.)

(A note for later, because it is a trap: Base uses the same law keyword 72 times to declare type families rather than propositions. In user code those are written with def — def Tree(d: Nat) -> Data:. Both uses are the same idea, a declaration you fill in, but the mechanism is not interchangeable. See What Base does not give you.)

And the proof begins the way the small one did — a def named after the law, with the law’s binders as parameters:

def Laws.tree_is_serial(d, g, w, h, blk, k):
  match d:
    case 0n:
      {==}
    case 1n+p:
      ...

(The Laws. prefix is the module: the law is declared inside LAWS.bend, imported under the alias Laws, and a fill is named after the law including the module it came from.)

Depth zero needs no work — a tree of depth zero is one leaf, and one leaf is the loop, so {==} closes that case. At depth p + 1 the tree is two depth-p trees joined, while the spec is still one undecomposed loop. Something has to split that loop in two. That is the first non-trivial lemma.

%: one rule, and how to aim it

You have used % once — the self-quote inside add_zero. Here is the rule stated once, in full, because every remaining step of every proof is it:

A lemma e : {a == b} applied as %e(...) : P replaces b with a in the goal. P is the goal written out with the occurrence of b replaced by _.

So _ sits exactly where the lemma’s right-hand side was. Which gives the working rule for writing lemmas:

Write a lemma as {what you want == what is there now}.

The right side is what the goal currently contains; the left side is what replaces it. Getting this backwards gives an error that says so plainly — expected and observed, with the two terms — and the fix is to swap them.

In the proof, the needed lemma splits a sequential loop in two:

%cells_add(g, w, h, Par.cells_in(p, blk), Par.cells_in(p, blk), k) : {Par.tree_cells(1n+p, g, w, h, blk, k) == _ : List<&2, Nat>}

cells_add(...) has conclusion {app(block(n,k), block(m,k+n)) == block(n+m,k)}, so its right side is the combined loop block(..., n+m, k). The goal’s second component is block(g, w, h, cells_in(p,blk) + cells_in(p,blk), k) — the same form. The _ marks it, and after the rewrite the spec’s single loop has become two loops, which is exactly the shape of tree_cells at depth p+1.

Then two more rewrites — the induction hypothesis, applied once to each half — and the case is done:

%Laws.tree_is_serial(p, g, w, h, blk, k) : {Par.tree_cells(1n+p, g, w, h, blk, k) == Par.app(_, Par.block(g, w, h, Par.cells_in(p, blk), Nat.add(k, Par.cells_in(p, blk)))) : List<&2, Nat>}
%Laws.tree_is_serial(p, g, w, h, blk, Nat.add(k, Par.cells_in(p, blk))) : {Par.tree_cells(1n+p, g, w, h, blk, k) == Par.app(Par.tree_cells(p, g, w, h, blk, k), _) : List<&2, Nat>}
{==}

Three rewrites for the inductive case, and {==} to close. The first is the structural fact; the other two are the induction hypothesis. The function you are proving is available inside its own proof, because the recursion of the proof follows the recursion of the term.

The library tax

Two lemmas in the proof file exist for reasons that have nothing to do with Life:

def add_zero(a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
def add_assoc(a: Nat, -b: Nat, -c: Nat) -> {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}:

You have met add_zero already — it is the fact you derived above, and the reason it exists is the one you watched fail: Nat.add is stuck when its first argument is a variable, so an equation containing Nat.add(k, 0n) for a variable k cannot be closed by computation, only by a lemma. add_assoc is the same diagnosis one level deeper: the offsets in the proof meet as (k + 1) + q, and no amount of computation turns that into k + (1 + q).

Both are plain defs, not laws, because they were needs, not requirements — the distinction from “Two containers” doing its work.

This is worth naming because it recurses through everything below. Base has no library of the facts you need. There is no Nat.add_zero to import; there are no standard facts about Nat.add, Nat.mul, Nat.mod or Nat.cmp. Every proof that touches arithmetic brings its own small arithmetic with it. For this law that was two lemmas, both easy. For the law we did not write — index safety — the same beginning leads into Nat.cmp and iterated induction on two variables at once, and that is a different order of work. We will come back to that.

Running it

cd life && bend LIFE_PAR_PROOF.bend

All terms check.

The law is in life/LIFE_PAR_LAWS.bend, the proof — lemmas included — in life/LIFE_PAR_PROOF.bend; both are printed in full at the end of this chapter.

Measured, on this machine:

Under a tenth of a second, including startup, re-measured while this part was revised (the appendix’s own re-run read a few hundredths higher — the order, as it warns, is the finding). This is the “several orders of magnitude” claim from the introduction, made concrete: a proof the size of a small paper is checked between keystrokes. The tradeoff is the one the language states openly — Bend does almost no type inference, so you annotate everything and the checker never has to search. The proof is verbose and the checking is free.

⚠️ “All terms check” is not evidence

A passing proof means the compiler verified your proof of the type you wrote. It says nothing about whether that type is the thing you meant. Prove a false law and it will happily check.

So the only evidence that the law is real is the other direction: break the implementation and watch the gate close. All three breaks below are made in the implementation file life_par.bend — never in the law:

That table is the actual content of this chapter. The law is a claim; the break test is what makes the claim mean something.

And it has to be done carefully, because a break test that does not break anything passes. During this book’s own writing, one such test replaced the string "██" in the animation — and the file also contains that string in a comment above the code, so the replacement landed in the comment, the code was unchanged, and the gate reported success. A no-op is indistinguishable from a working gate. Every break test from here on asserts that the text it replaces occurs exactly once before it writes:

assert s.count(old) == 1

The law and its proof

# The law of the parallel Life step.
#
# The parallel step is a fork/join tree: a leaf serially computes `blk` cells,
# a join concatenates the two halves. The law says the tree produces exactly
# the cells that one plain sequential loop over the same range would produce,
# in the same order. It is the same claim demos/pure_par_sum makes about its
# parallel sum, with a list of cells in place of a number.
#
# Written by hand, not by the AI. LIFE_PAR_PROOF.bend proves it.
import Base
import ./life_par.bend as Par

# LAW: for any depth d, grid g of width w and height h, block size blk and
# starting cell k, the tree covers the cells_in(d, blk) cells from k on and
# yields them in order. (cells_in(d, blk) is 2^d * blk, computed by the same
# recursion the tree uses rather than by a multiplication.)
law tree_is_serial:
  for +d: Nat
  for +g: List<&2, Nat>
  for +w: Nat
  for +h: Nat
  for +blk: Nat
  for +k: Nat
  {Par.tree_cells(d, g, w, h, blk, k) == Par.block(g, w, h, Par.cells_in(d, blk), k) : List<&2, Nat>}

# The proof of LIFE_PAR_LAWS.bend's tree_is_serial: induction on the depth d.
#
# The shape follows demos/pure_par_sum. The goal is {tree == loop}, and every
# rewrite moves the *right* side -- the spec -- into the implementation's
# shape, until both sides are the same term. `%e : P` rewrites with
# e : {a == b}, where P is the goal with `_` marking b, and the goal gets a
# there: a lemma is written with the form you want to eliminate on the RIGHT.
import Base
import ./life_par.bend as Par
import ./LIFE_PAR_LAWS.bend as Laws

# Nat.add recurses on its first argument, so Nat.add(k, 0n) is stuck when k is
# a variable. That is the only reason this lemma exists.
def add_zero(a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
      {==}

# (a + b) + c == a + (b + c). This is the direction the offsets need: the
# right subtree starts at k + 2^p * blk, which has to be seen as (k + 1) + q
# before the induction hypothesis on cells_add applies.
def add_assoc(a: Nat, -b: Nat, -c: Nat) -> {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      %add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
      {==}

# Splitting a sequential loop: n cells from k, then m cells from k + n, is the
# same list as n + m cells from k.
def cells_add(
  +g: List<&2, Nat>, +w: Nat, +h: Nat, +n: Nat, +m: Nat, +k: Nat
) -> {Par.app(Par.block(g, w, h, n, k), Par.block(g, w, h, m, Nat.add(k, n))) == Par.block(g, w, h, Nat.add(n, m), k) : List<&2, Nat>}:
  match n:
    case 0n:
      %add_zero(k) : {Par.block(g, w, h, m, Nat.add(k, 0n)) == Par.block(g, w, h, m, _) : List<&2, Nat>}
      {==}
    case 1n+q:
      %add_assoc(k, 1n, q) : {Par.app(Par.block(g, w, h, 1n+q, k), Par.block(g, w, h, m, _)) == Par.block(g, w, h, Nat.add(1n+q, m), k) : List<&2, Nat>}
      %cells_add(g, w, h, q, m, Nat.add(k, 1n)) : {Par.app(Par.block(g, w, h, 1n+q, k), Par.block(g, w, h, m, Nat.add(Nat.add(k, 1n), q))) == Con{Par.cellnext(g, w, h, k), _} : List<&2, Nat>}
      {==}

# The law itself. Depth 0 is one leaf, which is already the loop. At depth
# p + 1 the tree is two depth-p trees concatenated; cells_add splits the
# spec's single loop into those same two loops, and the two induction
# hypotheses turn each half of the spec into the tree that computes it.
def Laws.tree_is_serial(d, g, w, h, blk, k):
  match d:
    case 0n:
      {==}
    case 1n+p:
      %cells_add(g, w, h, Par.cells_in(p, blk), Par.cells_in(p, blk), k) : {Par.tree_cells(1n+p, g, w, h, blk, k) == _ : List<&2, Nat>}
      %Laws.tree_is_serial(p, g, w, h, blk, k) : {Par.tree_cells(1n+p, g, w, h, blk, k) == Par.app(_, Par.block(g, w, h, Par.cells_in(p, blk), Nat.add(k, Par.cells_in(p, blk)))) : List<&2, Nat>}
      %Laws.tree_is_serial(p, g, w, h, blk, Nat.add(k, Par.cells_in(p, blk))) : {Par.tree_cells(1n+p, g, w, h, blk, k) == Par.app(Par.tree_cells(p, g, w, h, blk, k), _) : List<&2, Nat>}
      {==}

Next: a second law, and the wall underneath.

A second law, and the wall underneath

The last chapter built the machinery on claims small enough to watch. This one points it at the second claim the Life work needed — the renderer’s — and it is also where the cost of proving shows up. The claim itself compares two functions that both compute a string, and the thing being proved is not an optimisation detail: it is a constraint discovered the hard way.

The setup

The animation’s renderer builds a frame backwards and reverses once at the end, because appending cell by cell in order would be O(frame²). Two levels are reversed in that one pass: the order of rows, and within a row the order of cells.

The law has to compare that against something. So the first job is to write the spec — the same frame, written the slow and obvious way, with no cleverness to get wrong:

def spec_row(+r: List<&2, Nat>) -> String:
  match r:
    case Nil{}:
      SNil{}
    case Con{h, t}:
      String.append(Anim.cell(h), spec_row(t))

def spec_rows(+rs: Anim.Rows) -> String:
  match rs:
    case Anim.RNil{}:
      SNil{}
    case Anim.RCons{r, t}:
      String.append(spec_row(r), String.append("\n", spec_rows(t)))

Two structural recursions, appended in order. Nobody would use this — it is quadratic — and that is exactly what makes it a good specification. It is obviously right.

Then the law is one line:

law frame_is_spec:
  for +rs: Anim.Rows
  {Anim.frame(rs) == String.append("\u{1B}[H", spec_rows(rs)) : String}

Fast renderer equals cursor-home escape followed by the slow renderer. This is the same shape as every law in this part: implementation on the left, obvious specification on the right.

The palindrome constraint is a theorem

Look again at the comment in life_anim.bend:

every cell must be a palindrome. "██" and " " both are; change to "▐█" and every row flips internally (measured).

Until now that was a note in the source and a paragraph in the animation chapter. Here it is a lemma:

def pick_pal(b: Bool)
  -> {Bool.pick(String, b, "██", "  ") == String.reverse(Bool.pick(String, b, "██", "  ")) : String}:
  match b:
    case False{}:
      {==}
    case True{}:
      {==}

def cell_pal(v: Nat) -> {Anim.cell(v) == String.reverse(Anim.cell(v)) : String}:
  %pick_pal(Nat.is_eq(v, 1n)) : {Anim.cell(v) == _ : String}
  {==}

A cell is equal to its own character-reversal. The proof is two cases and both are {==}, because "██" and " " are each their own reverse — the checker just looks.

Note what this buys. Change cell to return "▐█" and cell_pal no longer holds, so frame_is_spec no longer goes through, and the program fails to prove. The constraint that was a comment for two chapters is now a compile-time obligation. It is not decoration: the break test at the end of this chapter changes exactly that one string and the gate closes.

Five of the seven lemmas are not about Life

Only two of the seven are about frames. The rest is standard library that does not exist yet, re-derived here because there was no import to reach for.

That is the honest cost of proving in Bend today, and it should be counted before choosing what to prove. The Bend README says its Lean formalisation lags the TypeScript implementation; this is what that looks like from the outside. It is not a flaw in the design — it is a young language whose lemma library has not been written.

Two things to know when writing the proofs

Accumulator functions need the accumulator spelled out. String.reverse is not a structural recursion — it calls reverse.go(s, acc), and a goal containing reverse(x) for a variable x is stuck on it. Induction will not go through until the claim is strengthened: instead of proving the goal as written, you prove something that also says what is true of the accumulator at every step, and which gives the goal back when the accumulator is empty. For reverse that stronger statement is “reverse.go(s, acc) equals the reverse of s, followed by acc” — the invariant of the accumulator. Hence reverse_go_spec(s, +acc), and rowrev_spec(r, +acc), and inner(rs, +acc), which is this law’s own invariant:

def inner(rs: Anim.Rows, +acc: String)
  -> {String.append(String.reverse(acc), Laws.spec_rows(rs)) == String.reverse(Anim.framerev(rs, acc)) : String}:

The law is then inner(rs, SNil{}) with the accumulator at empty, which is one line of proof.

The marks are decided by use, and the checker is the judge. A law’s binders, a proof def’s parameters, and the binders inside a case pattern all carry the same optional marks, answering one question: how often may this proof consume the value? The smallest case settles how to choose them, and it is a runnable file (laws/use_twice.bend) — one law, whose proof hands its variable to two rewrite steps:

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

def use_twice(x):
  %add_zero_r(x) : {Nat.add(_, 0n) == x : Nat}
  %add_zero_r(x) : {_ == x : Nat}
  {==}

(add_zero_r : {a == Nat.add(a, 0n)} sits above it — add_zero’s reverse orientation, which is the direction these rewrites want.) Three marks, three answers, all measured:

So the working rule is the one the checker teaches, not one you can reason out in advance: write nothing first, and where it says consumed more than once, add a + — the message names the value. And - (erased) is not a short form of +: it says the value disappears at run time and may only flow through erased positions. This chapter’s own proofs show the verdict is not obvious from the shape — reverse_go_spec’s accumulator checks as -acc, while rowrev_spec’s and inner’s are refused with expected : -acc / observed : acc — which is exactly why the last word belongs to the compiler.

Two more measured details, both time-savers. The marks cannot be copied between proofs: in LIFE_ANIM_PROOF.bend, two of the four case SCon{+h, +t} cases check fine with their marks removed; the other two stop with expected : t / observed : t (consumed more than once), because those proofs consume the tail more than once. And a pattern binder cannot be marked erased at all: case SCon{-h, -t} is a parse error (expected : a term), not a quantity complaint.

Reading a failed proof

When a rewrite does not apply, the error prints expected and observed as fully unfolded terms. cellnext alone unfolds to thousands of characters, so the part that actually differs is somewhere in a wall of text. Measured, on a deliberately miscalled lemma:

The script in the directory folds those runs down to CELL:

bend LIFE_PAR_PROOF.bend 2>&1 | python3 elide_errors.py

This is a papercut rather than a language feature — the error is complete and correct, it is just rendered in a form no human can diff. Worth knowing before you spend an hour staring at one.

The break tests

Every one of these is a change to the implementation life_anim.bend:

The second entry is the one to look at twice. The bug that was found by eye, after it had already shipped into a working animation, is now caught at compile time — by a law whose proof takes 0.06 seconds.

That is the whole claim of this part of the book, and it is worth stating without inflation: the law does not make the renderer correct. It makes one specific property of it something you cannot break by accident and not notice.

Why we stopped here

The obvious next law was index safety for at() — “every index stays within 0 .. w*h”. It is a good law, it is the kind the Bend README advertises (array_set() may never be called out-of-bounds), and we did not write it.

Here is the wall. Both laws needed library lemmas that Base does not have. But the difficulty of the two taxes is not comparable:

The String lemmas were all structural: append matches on its first argument, so induction over that argument closes the proof. The arithmetic lemmas have to go through Nat.cmp, whose recursion compares two numbers and therefore needs induction over a pair. Same wall, two different heights — one is an afternoon, the other is not obviously finishable in one.

So the choice of which law to prove is not free, and it is not about how interesting the law is. It is about how far the lemma you need is from a structural recursion. Prefer laws whose proof obligation reduces to structural induction.

The law and its proof

# The law of the animated frame.
#
# `frame` builds the whole screen with ONE String.reverse at the end: rows are
# accumulated backwards (framerev), each row's *cells* backwards (rowrev), and
# the single char-level reverse undoes both at once. That is what makes it
# O(frame length) instead of O(n^2) with an append chain.
#
# The spec below is the same frame written the slow, obvious, append-heavy
# way. The law says the fast one equals it.
#
# The catch -- and the reason this law is not just a restatement -- is that
# the two levels disagree about what a "unit" is. rowrev reverses CELLS and
# leaves each cell's characters alone; String.reverse reverses CHARACTERS.
# Composing them gives
#
#     reverse (rowrev r) == map reverse (map cell r)
#
# so a row only comes out right if every cell is its own character-reversal,
# i.e. a palindrome. `cell` returns "██" or "  ", and both are. Change it to
# "▐█" and every row comes out mirrored -- measured, not reasoned: the 4x4
# glider renders as `OXOX][][` / `][][OX][` instead of `[]XO[][]` / `[][]XO[]`.
# That is the exact shape of the bug this repository already hit once.
#
# Written by hand, not by the AI. LIFE_ANIM_PROOF.bend proves it.
import Base
import ./life_anim.bend as Anim

# ---- the spec: what a frame should be, written the slow obvious way ----
def spec_row(+r: List<&2, Nat>) -> String:
  match r:
    case Nil{}:
      SNil{}
    case Con{h, t}:
      String.append(Anim.cell(h), spec_row(t))

def spec_rows(+rs: Anim.Rows) -> String:
  match rs:
    case Anim.RNil{}:
      SNil{}
    case Anim.RCons{r, t}:
      String.append(spec_row(r), String.append("\n", spec_rows(t)))

# LAW: the frame is the cursor-home escape, then the rows in order, each row's
# cells in order, each row followed by a newline.
law frame_is_spec:
  for +rs: Anim.Rows
  {Anim.frame(rs) == String.append("\u{1B}[H", spec_rows(rs)) : String}

# The proof of LIFE_ANIM_LAWS.bend's frame_is_spec.
#
# Same shape as LIFE_PAR_PROOF.bend: the goal is {impl == spec}, and every
# `%lem(args) : P` moves one side into the other's shape. P is the goal AFTER
# the rewrite, with `_` at the position the lemma's LEFT side was put in. So a
# lemma is written {target == what-is-there-now}: its right side is the form
# the goal currently holds, its left side is the form that replaces it.
#
# The first five lemmas are library gaps -- Base has no String lemmas at all.
import Base
import ./life_anim.bend as Anim
import ./LIFE_ANIM_LAWS.bend as Laws

# ---- library: append ----

# String.append matches on its FIRST argument, so append(a, SNil{}) is stuck
# when a is a variable. This is the only reason the lemma exists.
def append_nil2(a: String) -> {a == String.append(a, SNil{}) : String}:
  match a:
    case SNil{}:
      {==}
    case SCon{+h, +t}:
      %append_nil2(t) : {SCon{h, t} == SCon{h, _} : String}
      {==}

def append_assoc2(a: String, -b: String, -c: String)
  -> {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}:
  match a:
    case SNil{}:
      {==}
    case SCon{+h, +t}:
      %append_assoc2(t, b, c) : {SCon{h, String.append(t, String.append(b, c))} == SCon{h, _} : String}
      {==}

# ---- library: reverse ----

# reverse.go carries an accumulator, so it is stuck on a variable. Its
# invariant: the reversed prefix comes first, then the accumulator.
def reverse_go_spec(s: String, +acc: String)
  -> {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}:
  match s:
    case SNil{}:
      {==}
    case SCon{+h, +t}:
      %reverse_go_spec(t, SCon{h, SNil{}}) : {String.append(_, acc) == String.reverse.go(t, SCon{h, acc}) : String}
      %append_assoc2(String.reverse(t), SCon{h, SNil{}}, acc) : {_ == String.reverse.go(t, SCon{h, acc}) : String}
      %reverse_go_spec(t, SCon{h, acc}) : {String.append(String.reverse(t), SCon{h, acc}) == _ : String}
      {==}

# reverse(append(a, b)) == append(reverse(b), reverse(a)).
def reverse_append2(a: String, +b: String)
  -> {String.append(String.reverse(b), String.reverse(a)) == String.reverse(String.append(a, b)) : String}:
  match a:
    case SNil{}:
      %append_nil2(String.reverse(b)) : {_ == String.reverse(b) : String}
      {==}
    case SCon{+h, +t}:
      %reverse_go_spec(t, SCon{h, SNil{}}) : {String.append(String.reverse(b), _) == String.reverse.go(String.append(t, b), SCon{h, SNil{}}) : String}
      %reverse_go_spec(String.append(t, b), SCon{h, SNil{}}) : {String.append(String.reverse(b), String.append(String.reverse(t), SCon{h, SNil{}})) == _ : String}
      %reverse_append2(t, b) : {String.append(String.reverse(b), String.append(String.reverse(t), SCon{h, SNil{}})) == String.append(_, SCon{h, SNil{}}) : String}
      %append_assoc2(String.reverse(b), String.reverse(t), SCon{h, SNil{}}) : {String.append(String.reverse(b), String.append(String.reverse(t), SCon{h, SNil{}})) == _ : String}
      {==}

# ---- library: cell ----

# WHY THIS LEMMA IS THE WHOLE POINT. rowrev reverses CELLS; String.reverse
# reverses CHARACTERS. A row survives the one-reverse trick only because each
# cell is restored by a character reversal, i.e. is a palindrome.
def pick_pal(b: Bool)
  -> {Bool.pick(String, b, "██", "  ") == String.reverse(Bool.pick(String, b, "██", "  ")) : String}:
  match b:
    case False{}:
      {==}
    case True{}:
      {==}

def cell_pal(v: Nat) -> {Anim.cell(v) == String.reverse(Anim.cell(v)) : String}:
  %pick_pal(Nat.is_eq(v, 1n)) : {Anim.cell(v) == _ : String}
  {==}

# ---- the row ----

# reverse(rowrev(r, acc)) is the row's cells in order, then the reversed acc.
# Inducting on r needs the accumulator spelled out, hence the -acc.
def rowrev_spec(r: List<&2, Nat>, +acc: String)
  -> {String.append(String.reverse(acc), Laws.spec_row(r)) == String.reverse(Anim.rowrev(r, acc)) : String}:
  match r:
    case Nil{}:
      %append_nil2(String.reverse(acc)) : {_ == String.reverse(acc) : String}
      {==}
    case Con{+h, +t}:
      %rowrev_spec(t, String.append(Anim.cell(h), acc)) : {String.append(String.reverse(acc), String.append(Anim.cell(h), Laws.spec_row(t))) == _ : String}
      %reverse_append2(Anim.cell(h), acc) : {String.append(String.reverse(acc), String.append(Anim.cell(h), Laws.spec_row(t))) == String.append(_, Laws.spec_row(t)) : String}
      %cell_pal(h) : {String.append(String.reverse(acc), String.append(Anim.cell(h), Laws.spec_row(t))) == String.append(String.append(String.reverse(acc), _), Laws.spec_row(t)) : String}
      %append_assoc2(String.reverse(acc), Anim.cell(h), Laws.spec_row(t)) : {String.append(String.reverse(acc), String.append(Anim.cell(h), Laws.spec_row(t))) == _ : String}
      {==}

# ---- the frame ----

# The accumulator invariant over Rows: reverse(framerev(rs, acc)) is the
# reversed acc, then the spec's frame. At acc = SNil that is exactly the law.
def inner(rs: Anim.Rows, +acc: String)
  -> {String.append(String.reverse(acc), Laws.spec_rows(rs)) == String.reverse(Anim.framerev(rs, acc)) : String}:
  match rs:
    case Anim.RNil{}:
      %append_nil2(String.reverse(acc)) : {_ == String.reverse(acc) : String}
      {==}
    case Anim.RCons{+r, +t}:
      %inner(t, String.append("\n", String.append(Anim.rowrev(r, SNil{}), acc))) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == _ : String}
      %reverse_append2("\n", String.append(Anim.rowrev(r, SNil{}), acc)) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == String.append(_, Laws.spec_rows(t)) : String}
      %reverse_append2(Anim.rowrev(r, SNil{}), acc) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == String.append(String.append(_, "\n"), Laws.spec_rows(t)) : String}
      %rowrev_spec(r, SNil{}) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == String.append(String.append(String.append(String.reverse(acc), _), "\n"), Laws.spec_rows(t)) : String}
      %append_assoc2(String.reverse(acc), Laws.spec_row(r), "\n") : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == String.append(_, Laws.spec_rows(t)) : String}
      %append_assoc2(String.reverse(acc), String.append(Laws.spec_row(r), "\n"), Laws.spec_rows(t)) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == _ : String}
      %append_assoc2(Laws.spec_row(r), "\n", Laws.spec_rows(t)) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == String.append(String.reverse(acc), _) : String}
      {==}

# ---- the law ----

def Laws.frame_is_spec(rs):
  %inner(rs, SNil{}) : {String.append("\u{1B}[H", _) == String.append("\u{1B}[H", Laws.spec_rows(rs)) : String}
  {==}

Next: the gate, and its edges.

The gate, and its edges

The last two chapters showed how to write a law and a proof, and what they cost. This one is about the gate itself — bend PROOF.bend, the command that returns the verdict — and about what that verdict is worth. Both chapters came back to the same small print, and this is where it gets exact: “All terms check.” is the only evidence, and it is not evidence at all. Every output below is pasted from a real run of tools/drift/gate_matrix.sh.

The distance between two sentences

What a CI job would like to say is: this property cannot regress. What the gate can honestly say is: this proof checks. The distance between the two sentences has three shapes, and each one is a small file.

The escape hatch

Start with a law that is false — not subtly, plainly:

law false_law:
  for x: Nat
  {x == 1n : Nat}

No proof of this exists, so here is an “implementation”:

@unsafe
def Laws.false_law(x):
  Laws.false_law(x)

@unsafe is the guide’s one decorator: it tells the checker not to ask for a decreasing argument, an exemption real programs need when a loop cannot be proven to terminate. It also moves the def outside the proof’s guarantees — a function allowed not to terminate inhabits every type — so it inhabits {x == 1} as easily as anything else. It compiles, and bend PROOF.bend prints:

All terms check, but 1 def relies on unsafe or foreign code:
- LAWS.false_law

and exits 0. This is not a bug and not a secret — it is the first entry in upstream’s WONTFIX.txt, under DESIGN:

@unsafe programs check and exit 0 (#776, #805) The checker prints “All terms check, with N unsafe annotations.” and exits 0. @unsafe is a choice the author made in the source; read the note, not the exit code.

(Upstream’s note still shows the older wording; the message 2.0.24 prints is the one quoted above.)

Two measured details about the note. First, the count covers everything the run loads: one @unsafe def anywhere in the import graph — even one no proof touches — degrades the message. Second, the count is over defs, and the message names them: the run above lists - LAWS.false_law under the verdict. A ~ template instance does not appear in it — the disclosure is about what relies on unsafe or foreign code. The message is still something to read, not a bit to parse.

The vanishing spec

LAWS.bend is the human’s file, and the gate is a check on the files it is handed — whatever is there. Delete the law and see. With the proof def left behind, the report is:

Error:
- expected : '->'
- observed : ':'
Location:
4>| def Laws.add_zero_law(x):

A parse error that names nothing. It reads as “add a return type” — the wrong repair for a law that went missing (this message is filed upstream as bendlang/bend#850). Delete the def too, and:

All terms check.

Zero laws checked, all of them fine. What stops the quiet half of this is one check, added in 2.0.8: a PROOF.bend that sits beside a LAWS.bend must import it.

$ bend PROOF.bend        # with the import line removed
bend: PROOF.bend must import ./LAWS.bend (see bend --help)

That closes “the AI skipped the law file”. It cannot close “the law file was edited”, because the law file is the spec — and a spec the constrained thing can edit is not a spec. The gate checks that two files agree; keeping them in agreement is a social arrangement, and it is the load-bearing part.

The CI that greps wrong

Three plausible ways to wire the gate into CI, run against the @unsafe fixture above:

The exit code is fooled because the design says so. The substring grep is fooled because All terms check, but 1 def relies on unsafe or foreign code: contains All terms check. Only the exact-line match notices the difference.

The recipe

bend PROOF.bend > gate.out 2>&1 || exit 1
grep -qx 'All terms check.' gate.out || exit 1

Two lines, one job each. The first fails on compile errors, open laws (1 TODO found.), and the import check. The second insists on the verdict line exactly — no with N annotations, no skip, no partial run. If a future version rewords the line, this CI goes red; for a check that depends on a message, that is the correct failure mode, and gate_matrix.sh is what notices it first.

What the gate does guarantee

Stated with the same care, because it is not nothing:

• The break tests. Change the implementation and the gate closes; restore it and the gate opens. Five of the six patches the previous chapters record — the three life_par ones and two of the three life_anim ones — were re-run while this chapter was written, and every one still closes the gate. (Each patch asserts it changed exactly one spot before writing, and every file was restored byte-identical — the discipline of the appendix, re-used.)
• Open laws are refused. A declared law without a proof is 1 TODO found. The code is incomplete, and not a valid proof yet. — exit 1. A ?TODO hole is the same.
• Skipped law files are refused (the import check above).
• It is fast. The two Life proofs check in 0.07 s and 0.06 s — re-measured while writing this chapter. None of this is bought with patience.

The Bend Hub

The previous chapter stopped at a library gap. Its index-safety law needs arithmetic facts that Base does not state. The Bend Hub is where Bend programs can share facts such as these. It is a public, content-addressed package store. It needs no account, and packages have no names or version numbers. A package’s content hash is its identity.

Open the Hub to browse packages or paste a hash into its search box. To use a package, copy its import line into a Bend file:

import 0x1ee1b5d0c2a66817bf368b849f3117fc/nat.bend as Nat

The first bend run downloads the package to ~/.bend/lib, checks its content against the hash, and then checks it with the rest of the program. The alias on the right becomes the namespace. For example, a proof can now rewrite with %Nat.add_assoc(a, b, c) instead of defining associativity again.

To publish a package, check its entry file and then pass --publish:

bend nat.bend
bend nat.bend --publish

The second command uploads the file and its imports, then prints the import line for the new hash. Changed content produces a new package and a new hash. Existing imports stay pinned to the bytes that their authors checked.

Lemmas contributed by this book

The Life proofs exposed three gaps in Base. We extracted their reusable lemmas and published them to the Hub:

• nat.bend contains six facts about Nat.add: zero and successor in both rewrite directions, associativity, and commutativity.
• string.bend contains five facts about String.append and String.reverse.
• list.bend contains six matching facts about append, reverse, and length for List.

The repository keeps the package sources and publication log. Anyone can open a package on the Hub, read its source, and run bend on it. A valid package prints All terms check. The original index-safety wall still stands because it needs Nat.cmp facts that these packages do not contain. The Hub does not remove the proof work; it lets one proof publish that work for the next one.

The three edges

Keep them in view and the guarantee is shaped like this: a change that breaks a stated property cannot pass unnoticed, provided three things stay separately true.

1. No @unsafe in the import graph of anything you gate. It is not a scan the compiler does for you; it is a choice in your sources, and one grep if you want a machine to check it.
2. The spec file is the humans’. The compiler can refuse a proof that skips its laws; nothing can refuse a law that was deleted. That half is a review habit, not a check.
3. The CI reads the verdict line exactly, in the two lines above.

The gate is a young instrument, and this chapter is its boundary map: what it proves, what it only promises, and how to tell which one you are looking at. Within those edges, “All terms check.” means exactly what the previous two chapters said it means. Outside them, it means whatever you let it mean.

Running it

sh tools/drift/gate_matrix.sh

Seven fixtures, seven lines, one per case — the false law, the TODO, the missing import, the emptied spec, the stray @unsafe, the stray proof def. Run it after a bend update; the day one of those lines changes is the day the boundary moved.

Every deliberately-broken probe, and the error it produces

This book contains a lot of code that does not compile. That is on purpose: Bend’s error messages are precise, local and mechanical, and in many places they taught us more in ten seconds than the guide did in ten minutes. So every failure shown in the book is a real file in this repository, and every error quoted is pasted from running it.

This appendix is the index. Run any of them yourself.

cd basics && bend hello_bad.bend

❌ does not compile

Two of these are worth singling out, because they are the cases where the error message is less helpful than Bend’s usual standard:

• hello_bad.bend points at the signature line and says unknown: IO. It never mentions angle brackets, so it reads as though Base failed to import. The rule the message does not state: IO(Unit) in a signature, do IO<Unit>: in a do block.

⚠️ compiles, runs, and lies

The most instructive category. Nothing here fails — which is the problem.

pat_bad.bend. Bend’s Nat patterns are 0n and 1n+p, where the second means “at least 1”, not “exactly 1”. The obvious way to write a three-way dispatch —

  match n:
    case 0n:  ...
    case 1n+p: ...
    case 2n+p: ...

— compiles, runs, and silently swallows n = 1 into the second case, because 1n+p matches 1 with p = 0n. The 2n+p arm is only reached for n ≥ 2. There is no warning. This is the closest thing to a footgun in the language, and it is a direct consequence of Nat being a Peano datatype rather than a machine integer.

esc_bad.bend. Bend’s string escapes are exactly \n \t \r \0 \\ \' \" \u{...}. There is no \e and no \x1b. \033 does not error — it parses as \0 followed by the two literal characters 33, so you get a NUL byte and the text 33. On a terminal the NUL is invisible and you see a space and 33. The working spelling is \u{1B}.

Both of these are exactly the shape to watch for: a wrong program that runs and produces output that looks plausible. The animation chapter hit the same class of bug — a mirrored render, correct in y, wrong in x.

The proofs are probes too

life/LIFE_PAR_PROOF.bend and life/LIFE_ANIM_PROOF.bend are not just proofs; they are two more gates in this same list. Each is paired with a table of deliberate changes to the implementation that it must reject. Those tables are in Your first law and proof and A second law, and the wall underneath, and re-running them is part of maintaining this repository.

One caveat, learned the hard way three times: a break test that silently fails to replace anything passes. Confirm s.count(old) == 1 before writing. The full story is in life/README.md in the repository.

Every number in this book, and how it was measured

Every timing in this book comes from one machine, and this appendix is the record of which machine, what command, and what the number did when it was re-run.

The machine

hw.perflevel0.logicalcpu reports 10. That is why --threads 8 and --threads 10 are where the parallel curves flatten and --threads 14 is slower: past ten the scheduler is putting work on the efficiency cores. Any thread count above 10 in this book should be read as oversubscription, not as more capacity.

All numbers were re-run for this appendix on 2026-09-18, on the machine above, with nothing else running. Where a value moved, the book quotes the new one.

Every one of them is re-checked mechanically with tools/drift/run_drift.py — 92 checks — so a version that moves a number says so instead of leaving the book quietly wrong.

1. The two proof gates

cd life
/usr/bin/time -p bend LIFE_PAR_PROOF.bend
/usr/bin/time -p bend LIFE_ANIM_PROOF.bend

user is about 2.5× real because Bend’s checker itself runs in parallel. The wall-clock number is what a human experiences; it includes Bend’s startup.

2. The size of a proof error

# break the proof by miscalling a lemma, then:
bend LIFE_PAR_PROOF.bend 2>&1 | wc -c
bend LIFE_PAR_PROOF.bend 2>&1 | python3 elide_errors.py | wc -c

Worth noting the contrast: a late proof error is small. Three deliberate changes to the implementation produced errors of 270, 553 and 638 bytes, all readable. The 14 KB monster only appears when the goal is stuck at a point where block has already unfolded into conses — which is a middle-of-the-proof situation, and the one where you most need to see the difference.

3. pow2: the parallel curve

cd parallel && bend pow2_26.bend -o pow2_26
for t in 1 2 4 8 14; do /usr/bin/time -p ./pow2_26 --threads $t; done

pow2(26n) is 67,108,864 additions. Every run prints 67108864.

Near-perfect to 4, then it saturates. The value is not the arithmetic — it is that a plain parallel let runs on the CPU with no ! anywhere. ! is what sends a call to the GPU; it is not what enables parallelism.

4. The GPU entry fee

cd gpu
bend gpu_floor.bend -o gpu_floor && ./gpu_floor   # result is 4!
bend pow2_gpu.bend  -o pow2_gpu  && ./pow2_gpu    # result is 67108864
bend gpu_twice.bend -o gpu_twice && ./gpu_twice   # two calls

Sixty-seven million additions cost the same as four. And a second GPU call in the same process costs almost nothing extra. So the ~85 ms is a per-process entry cost, not a per-call tax — and gpu_floor has no fork-join work left in it at all, which rules out the scheduler as the explanation. It is the Metal runtime: device, command queue, pipeline state.

This is the measurement that changed the meaning of every other GPU number in the book. If you take one methodological habit from this appendix, take this one: when a GPU number surprises you, write a program that does nothing and measure that.

5. mandelbrot — uniform numeric work

cd gpu/mandelbrot
./cpu --threads 1     # 5.10, 5.11
./cpu --threads 10    # 0.72, 0.71
./gpu                 # 0.12, 0.11, 0.10

4096² pixels, 51 iterations.

The first run is slow. An early measurement of this binary was 0.226 s, which settled to 0.108 s on repetition — a factor of two. Never quote a GPU number from a single run.

6. queens — divergent search

cd gpu/queens
./cpu --threads 1     # 6.02, 6.19
./cpu --threads 10    # 0.85, 0.86
./gpu                 # 1.36, 1.34, 1.41

N=17 exhaustive search.

The CPU wins, and not narrowly. This is the one place where the guide’s own claim — divergent work stays on the CPU — came out against the GPU by our own measurement rather than by repetition.

7. Life — the row-window engine

cd life && bend life_row.bend -o life_row
./life_row --threads 1

Sixty-four generations, one thread:

The right column is flat over a 64× range of sizes. That is what O(n) looks like.

⚠️ IO.now() has one-millisecond resolution. The 32×32 row is four ticks wide, so its ns figure carries roughly ±25%; the book’s tables once said 76 there. Every small value in this book is subject to this. Treat the shape of a column as the finding and the individual cells as approximate.

8. Life — naive vs row window, head to head

./life_par --threads 1     # last line: "naive, no fork", 64x64, 16 generations
./life_row --threads 1     # last line: 64x64, 16 generations

Both single-threaded, 64×64, sixteen generations:

≈ 1,600×. The divisor sits on the timer’s resolution, so across sessions this ratio reads anywhere from about 1,600× to 2,000×. The order of magnitude is the finding.

The naive side also demonstrates the complexity directly:

Cells ×4, cost per cell ×4, total ×16. That is O(n²) announcing itself.

9. Life — the fork-join granularity table

cd life && bend life_par.bend -o life_par
./life_par --threads 1
./life_par --threads 10

64×64, four generations, three leaf sizes. blk is how many cells each leaf task computes; 2^d × blk = 4096.

Three things to read here.

The speedup is only about 2–3× on ten cores. That is not the scheduler failing; it is the shape of this program. Each generation must finish before the next can start, so there is a join barrier every generation, and there are only four generations.

Finer is not reliably faster. An earlier version of this code — the build + flatten structure, before it was rewritten into tree_cells so the law could be proved — showed blk=1 clearly ahead at every thread count. After the rewrite the ordering is much flatter at ten threads and blk=16 is marginally ahead. The rewrite moved app (the concatenation of the two halves) inside the fork-join region, so every join has one worker concatenating while the other idles; more joins means more idling.

The lesson is about the confusion, not the numbers: “finer granularity is faster” was true of one implementation, and was written down as if it were a property of the scheduler. It was corrected by the rewrite.

The command’s own wall clock is not the number to quote. The same command also runs two naive, no fork cases — depth zero, one leaf for the whole grid, so serial by construction — and they are most of it. /usr/bin/time -p on ./life_par --threads 1 reads 14.2 s against 10.5 s on --threads 10, while the three fork-join cases inside that same process go from 5.7 s to 2.3 s. The two serial cases account for the difference: 8.4 s of the fourteen, and 8.2 s of the ten and a half.

10. Life — the row engine under the same fork-join tree

cd life && bend life_rowpar.bend -o life_rowpar
./life_rowpar --threads 1
./life_rowpar --threads 4
./life_rowpar --threads 10

life_rowpar.bend hangs the same fork-join tree over the row engine, one level up: the leaf is a run of consecutive output rows (rows3), the join is rows_app, blk is rows per leaf. The clock wraps evolve only — the grid is built and the cells counted outside it — so these figures are not comparable with life_row’s whole-process numbers in section 7, which include both.

Two to three runs per cell, 2026-09-20. The ten-thread tree cells are the noisiest numbers in this appendix: a further run moved them by up to 30%.

256×256, 64 generations:

512×512, 64 generations:

/usr/bin/time -p over the whole six-benchmark run: --threads 1 reads real 8.90 / user 8.88; --threads 4 real 5.90 / user 9.22; --threads 10 real 6.00 / user 9.47. The forks are real at both thread counts; four threads is the better deal.

The finding is the shape, not the digits: the O(n) engine’s work is uniform, so the same tree that buys 3.1× on the naive engine buys a stable 1.4× here — but only up to four cores. Four leaves per generation cap the width, finer leaves cost more than they return, and the algorithm fix has already removed almost everything the cores could multiply.

The disciplines, collected

Everything above is one number with a command. These are the habits that made the numbers mean something, and each was learned by getting it wrong first.

A benchmark that measures two things measures neither. The first parallel Life benchmark ran the serial version and the parallel version in the same process, so the reading was of the whole process — and the serial baseline swallowed half the wall clock. The parallel section was going from 493 ms to 211 ms while the process looked flat. The fix is a narrower benchmark, not a better one.

real can lie about parallelism; user cannot. real includes every serial part of the program. user is total CPU time across all cores, so user / real is the average number of cores actually working. When user climbs from 7.0 s to 11.6 s across a thread sweep, the parallelism is real regardless of what real does.

Measure the floor. If a number surprises you, build the smallest program that should be cheap, and time that. gpu_floor cost the same as the real workload and rewrote the conclusion of a whole chapter.

Write the unit down. ns per cell, per generation moves in a straight line where ms does not, and user / real says something real cannot. A raw millisecond count is only comparable to another millisecond count from the same machine, kernel and load.

A ratio has a resolution too. 8,114 / 5 looks precise and is not: the divisor is five timer ticks. Report the range you actually observed, and say which end is at risk.

Re-run before quoting. Every number here was re-measured for this appendix, and two of them moved. That is the normal outcome, not a sign that something was wrong the first time.

What Base does not give you

Every chapter in this book uses import Base, and almost every chapter takes it for granted. This appendix is what is actually in it — and what is conspicuously not.

The inventory

Base ships inside the Bend installation, as a single file:

~/.bend/bend2/base.bend

Measured, for Bend 2.0.24:

tools/base-inventory.py re-measures every row of this table and the one below against the installed base.bend. It is what caught the lemma count, so it is worth running on a bend update before quoting anything here.

The 22 types break down as 13 is Data, 3 is Type and 6 is Kind — that division is the subject of Kinds and copies, and it is not decoration: it is why Array cannot be read twice and List<&2, T> can.

The 16 largest namespaces, by size — Result ties with TCP at 6 and is the one row that does not fit here; the tool prints all 28:

Ten lemmas, and the ones that are missing

A proposition law claims an equation ({a == b}). A type-family law declares a type you fill in with type X.*, which is what Word(32n) is. Of the 84 law declarations in Base, 10 are propositions, and all 10 have a proof:

Two counting traps, and this appendix sat in the first one for a while:

• grep -c -e '-> {' base.bend returns 0, and that number means nothing. Base writes its proofs as def Nat.ge_refl(a): with no return type — the law it fills supplies it. A grep for -> { asks for a shape Base never uses, so it reports zero however many lemmas are there. The count above is taken from what each law declares, not from the shape of the def that proves it.
• law in Base is usually not the law of the last two chapters. 74 of the 84 declare a type family, not a proposition. That is the trap at the end of this appendix, and it counts on the other side of this one.

The correction is small and the conclusion is not. None of the ten touches the functions a proof actually needs. There is no fact about Nat.add, none about String.append, none about List, Nat.mod or Nat.cmp. U32.add_comm is the one lemma here a reader might have imported, and this book never reaches for it — the Hub package defines its own add_comm, about Nat.add, because Base’s is about U32 and Word and does not generalise. The gap is per-type, not only per-name.

This is what sets the price of everything in the last part of this book. Writing a law is cheap. Proving it is cheap if every fact you need reduces to structural induction. If it does not, you are writing the standard library yourself, first, inside your own file.

What the two proofs had to fill in

life/LIFE_PAR_PROOF.bend and life/LIFE_ANIM_PROOF.bend between them define eleven lemmas. Only three are about Life:

Five of the eight library lemmas are String lemmas, and the reason is visible in the inventory above: String has 40 functions and no facts at all. There is no String.append_nil to import. There is no String.reverse_reverse.

If you want to prove anything about string manipulation in Bend today, you begin by writing these. There is no shortcut and no simp.

Why the lemmas look the way they do

Two shapes recur, and both are consequences of how Base is written rather than of what is true mathematically.

A function that recurses on its first argument is stuck on a variable. String.append matches on its first argument, so append(a, SNil{}) does not reduce when a is a variable — the reducer has nothing to match on. Hence append_nil2, whose statement is written with a on the left precisely so the goal can be reoriented. Nat.add is the same, hence add_zero.

A function with an accumulator hides its own structure. String.reverse is not a structural recursion; it calls reverse.go(s, acc). A goal containing reverse(x) for a variable x is therefore stuck, and induction will not go through until the invariant is generalised over the accumulator. That is what reverse_go_spec, rowrev_spec and inner are for.

The two taxes, and why they are not the same size

The book’s last chapter explains why one law was written and a second, equally desirable one was not. The distinction is worth restating here as a piece of planning advice:

The String lemmas are all of the first kind. The arithmetic ones are of the third and fourth: Nat.cmp compares two numbers, so an induction over it needs a hypothesis about a pair.

So when choosing what to prove: prefer laws whose proof obligation reduces to structural induction. The distance from a structural recursion is the cost, and it is an order of magnitude, not a percentage.

A trap: law in Base is not the law of the last two chapters

Base uses the law keyword 72 times, and every one of them declares a type family, not a proposition:

law Word:
  for n: Nat
  Data

type Word.Nil is Data:
  WNil{}

type Word.Con<-p: Nat> is Data:
  WCon{head: Bool, tail: Word(p)}

Word(32n) is then a type, and it is what U32 is made of (type U32 is Data: U32{data: Word(32n)}).

Both uses are the same idea — a law is a declaration you have to fill in — but the mechanism is not interchangeable, and it is worth not being surprised:

• In Base, a law is filled by the type X.* declarations in its namespace.
• In user code, write the type family with def instead:

  def Tree(d: Nat) -> Data:
  

  This is what bend/demos/pure_par_sort/main.bend does upstream, and what life/life_par.bend does here.

Declaring a type family with law in a user file does not work, and the failure is not a syntax error:

law MyWord:
  for n: Nat
  Data

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

Adding the type MyWord.Nil / type MyWord.Con declarations does not change it, and using MyWord(2n) as a type gives expected : a datatype, observed : MyWord(2n). Whether that is a limitation or a deliberate restriction is not something this book established — it is a measured behaviour, and it is why no chapter ever writes law for anything except a proposition.

The same message is what you get for a law you have declared and not proved, which is a genuinely useful thing: write the law first, run, and let the compiler tell you it is unfinished.

The short version

Base gives you a rich term library — 383 definitions covering lists, strings, maps, numbers, arrays, IO, files, TCP and UDP — and a reasoning library of ten lemmas, none of them about anything on that list.

For programming, that is fine and it is generous. For proving, it means the first law you prove is cheap and every law after it that touches arithmetic is not, and the difference between those two cases is whether your obligation reduces to a structural recursion.