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.

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:

• The language — the syntax and the parts of the standard library this book actually uses.
• The idea that changes everything — affine values. Until this lands, nothing about Bend makes sense; after it, most of the language is obvious.
• 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.
• 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. Version 2.0.5 was current while this was written, and some of what follows will have been fixed by the time you read it.

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.5:

• 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 --version

bend 2.0.5

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:

That first row matters more than it looks. bend is a shell script that resolves the version, checks for updates, and then hands the work to bun running the TypeScript. So the thing on your PATH is a launcher, and every invocation carries a small startup cost you will notice later when you are timing things — and an automatic update check, which is why a first run sometimes stalls.

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 trap: the installer does not know about fish

The install script ends by adding ~/.bend/bin to your shell’s startup file, and it decides which one with this:

case ${SHELL:-} in
  *zsh)  rc=$HOME/.zshrc ;;
  *bash) rc=$HOME/.bashrc ;;
  *)     rc=$HOME/.profile ;;
esac

Only zsh and bash are handled. If your login shell is zsh, the line lands in ~/.zshrc — which fish does not read. If your login shell is fish, you fall through to the *) branch and it writes to ~/.profile, which fish does not read either. Either way the script cheerfully prints:

Your PATH now has ~/.bend/bin; open a new shell to use bend.

…and which bend finds nothing.

The fix is one line in your fish config:

fish_add_path ~/.bend/bin

This is worth knowing about for a second reason: it is the kind of thing that makes people conclude a language is broken when it is a five-line shell script in the installer. Bend’s compiler is fine. Its installer assumes bash.

Telemetry, and turning it off

The launcher sends an anonymous report on every run — version, OS, architecture, which subcommand, exit code, elapsed milliseconds — by POSTing to bend-lang.com/ping in the background. Set:

export BEND_NO_TELEMETRY=1

This book sets it everywhere, and so should you if you are going to run the benchmarks in it, since the reports are fire-and-forget but they are not free.

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              # ① interpreted, on a JavaScript backend (bun)
bend hello.bend -o hello     # ② compiled to a native executable
./hello

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

The difference is parallelism. The JavaScript backend runs everything sequentially — Bend’s own documentation says so plainly, and it means what it says. 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. 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>: is a block of such actions, run in order, top to bottom. Every line in it produces a value of some type; the block’s own value is the last one.

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:

• in a signature, a type is applied with parentheses: IO(Unit), List(Nat);
• in a do block, and in some other positions, it is written with angle brackets: do IO<Unit>:, List<&2, Nat>.

The compiler points at the signature line and never mentions the brackets. The same mistake cost this book’s author a bisection session, and it is preserved in the repository as basics/hello_bad.bend.

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: numbers and patterns — 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
7 |     case 1n+p:
8>|       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
10 |     case 1n+q:
11>|       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

# 探针 1：终止检查器是否接受「结构性递归」做取模
# x mod n：对 x 做结构性递归，用 k 累积。每次调用 x 都变小（p 是 x 的真子部分）
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.

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: lists, where a one-line function 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>}

Two things in that declaration are worth noticing now and will make sense in the next chapter. The -A: Kind(a) and the is Kind(a) are about how many times a value of this type may be copied, and that is the single most consequential thing about Bend. For this chapter, read past it.

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<&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 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 your first sighting of a quantity

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 are allowed to find this signature strange. 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. The next chapter 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 next two chapters 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":

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. Syntax, numbers, lists, strings — nothing you have seen so far would be out of place in a language you already know.

That ends now. The next chapter is about the one rule in Bend that changes how you write every single function, and until it makes sense, nothing else about Bend will.

Next: affine values.

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.

— GUIDE.txt:55

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
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 声明了，但一次都没用
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 在【两个分支里都出现】，但任何一条执行路径上只走一次
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.

— GUIDE.txt:586

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.

— GUIDE.txt:147-153

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.
• Closures are affine and cannot be marked otherwise. The next chapter 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: copies, kinds and the + mark — what + really costs, and why it is refused for some types and not others.

Copies, kinds, and the + mark

The last chapter 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
# 试图把数组标成可重用
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

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 signature that looked strange makes sense:

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.

— GUIDE.txt:586

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
# 闭包本身能调两次吗？用 t5 那个能编译的闭包写法，只加一个 +
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 ~ has to be written on BOTH sides. See t11_templatemiss.bend for what
# happens when you forget the one at the call site.
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 ~ on the parameter means template, and the ~ at the call site is what makes the argument one. 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.

The error you will actually hit is not about templates at all. Leave the ~ off the call site and the argument becomes an ordinary affine value, which cannot be used twice — and Bend says so, without mentioning the ~ it is missing:

Error:
- expected : -f
- observed : f (consumed more than once)
Location: twice~0

Kept as affinity/t11_templatemiss.bend. Location: twice~0 is the only hint that this is a specialized copy — and it is not much of a hint unless you already know what ~ is.

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 chapter, 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

# 探针 2：数组读的手感。a[i] 返回 Array<U32> & U32（一个 Sigma）
def main() -> IO(Unit):
  do IO<Unit>:
    a = [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.

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 — three chapters, one mechanism, 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.

— GUIDE.txt:147-153

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

# 一个在并行调用上分治的例子：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.

! is not the parallel switch

This is the mistake to avoid, and it cost this book’s author a wrong conclusion early on:

pow2(26n)      # parallel, on the CPU
pow2!(26n)     # parallel, on the GPU

Both are parallel. ! does not turn parallelism on. Under native compilation, a parallel let forks onto multiple cores with no mark at all; ! means something else entirely — hand this call to the GPU. That is the next chapter.

❌ The measurement trap

The first attempt at these numbers was run under bend pow2_26.bend, without compiling, and real did not move at all as threads went up.

That is not a bug. From the guide: the JavaScript target ignores all of it and runs sequentially. bend file.bend interprets; bend file.bend -o file compiles natively, and only the compiled binary has more than one core.

There is no way to see this from the numbers alone — a sequential run looks exactly like a parallel run that does not scale. It is worth internalising now, because every number in the rest of this book comes from a compiled binary.

The files

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

Next: the GPU, and the ! mark — where the numbers get strange, 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 shape of the work

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. Each leaf then decodes its own column quadruple and runs the classic bitmask backtracker over the remaining 13 rows.

And that second half is where the uniformity ends:

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

Branches that get pruned early return almost immediately. Branches that do 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. This is the best place in the book to see 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

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

The same rule, from the other side. solve wants to add up Stats{sols, nodes} from a child call and a sibling call. Taking the child’s result apart to read its fields is exactly what Bend refuses, so the accumulation is rearranged so that each result arrives as a parameter instead.

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, and 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. 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.

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:

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

sel is a select — a conditional value, not a conditional jump. Every pixel takes the same path through the same instructions; only the data differs. The escape count is still correct, because a frozen z stops changing and the remaining iterations are wasted work that 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 — and on a GPU, arithmetic is the thing that is nearly free.

The two passes

The render is not one fork. It is two, plus something in between:

1. Histogram. Fork 2^18 blocks of 64 pixels; each block sorts its escape counts into 8 buckets and the buckets are merged pairwise up the fork tree.
2. The CDF. A serial pass turning the root histogram into an equalisation lookup table. Small, sequential, unavoidable.
3. Recolour. Fork again, one leaf per pixel this time, running each pixel back through the lookup table and summing by position.

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:

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. The last part takes the same machinery — affinity, kinds, the fork — and points it at a different question: not how fast, but how do you know it is right, without reading the code.

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.

The escape route

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. That is the next chapter, and it is worth about a factor of 1600.

The whole file

import Base

# ============================================================
# 生命游戏 (Conway's Game of Life)
# 网格是一个平的 List<&2, Nat>，长度 w*h，取值 0 或 1。
# 坐标 (x,y) → 下标 y*w + x；越界自动绕回，所以世界是个环面。
# ============================================================

# ---- 取第 i 个元素；走过头返回 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)

# ---- 坐标 → 值，环形 ----
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)))

# ---- 8 个邻居之和 ----
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))))))))

# ---- 生死规则 ----
# 恰好 3 个邻居 → 活（无论原来死活）；恰好 2 个 → 维持原状；否则死
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))

# ---- 下一代：n 个格子，从下标 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))}

# ---- 初始图案：一个滑翔机 glider，坐标 (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))}

# ---- 渲染成字符串，每 w 个字符一行 ----
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))))

# ---- 演化 gens 代。gens 必须放最左：终止检查器要求「会使参数变小的那个排第一」 ----
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 same game in O(n).

Life in O(n), by rows

The previous chapter ended on the diagnosis: the cost is not the rule, and not the neighbour sum — it is computing an index at all. So the fix is to stop indexing.

Which raises the question of how you read a cell’s neighbours without jumping to them. The answer is the one this chapter is named after.

The trick: sum the columns first

A cell’s eight neighbours are the 3×3 block around it, minus the centre. So take the three rows involved — the one above, the one at, the one below — and sum them column by column into a single row s:

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

Now the 3×3 block around (x, y) is exactly s[x-1] + s[x] + s[x+1], because between them those three entries have visited every cell of the block once. Take off the centre, which got counted in s[x]:

neighbours(x) = s[x-1] + s[x] + s[x+1] - cur[x]

Nine cells, three additions. And the whole thing is a walk — three lists moving together, one position at a time. No index is ever computed, so no list is ever traversed twice.

That is the entire optimisation. Everything below is bookkeeping to make the walk work at the edges and between rows.

Walking in circles

The world wraps, so the rows have to rotate. 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. That keeps one rotation primitive to get right, and both are O(w) — a pass over the row, which is the same order as the pass we are already doing.

Both are used in newrow, the function that produces one new row:

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{})

rot_r(s) is s shifted so that position x holds s[x-1]; rot_l(s) holds s[x+1]. Three lists, same length, walked in lockstep — s[x-1], s[x], s[x+1] are simply the current heads.

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 has to rotate too.

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

zip3 walks the three staggered row lists together, one row from each per step, and calls newrow. Note what this means: the grid is never indexed, at either level. Not horizontally within a row, not vertically across rows. The whole generation is one walk of a structure that is 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 ns 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.

This is the number worth carrying away from the whole Performance part of the book. Ten cores bought about 3× in the last chapter. Changing the algorithm bought about 2,000×, from the same programmer, in the same language, on the same afternoon.

Put the two side by side and the ordering is unambiguous — the parallel naive version, on ten cores, at 4 generations, is still 676 ms. The serial row-window version does 16 generations in 4 ms. Parallelism is a multiplier on an algorithm. It does not choose one for you.

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

Next: the naive engine, parallelised, and why the honest answer is “it depends”.

Is it actually parallel?

The previous two chapters established that the algorithm matters more than the cores. This one is about the cores, and about a question that sounds trivial and is not: how do you know a program is running in parallel?

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, at least not reliably, and getting this wrong is easy enough that this chapter’s author did it twice.

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, +k: Nat, +blk: Nat) -> Tree(d):
  match d:
    case 0n:
      block(g, w, h, blk, k)
    case 1n+p:
      a b = tree_cells(p, g, w, h, k, blk) tree_cells(p, g, w, h, k + cells_in(p, blk), blk)
      app(a, b)

2^d × blk = w × h covers the grid, so blk is a granularity knob and everything else stays fixed. The a b = ... line is the fork; app 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.

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. Wall clock alone will lie to you, as the next section shows.

❌ The trap: you can measure the wrong thing

The first version of this benchmark ran the serial and parallel engines in the same process, back to back, so the reader could compare them. At 32×32 it reported a speedup of about 2.2×, and the parallel engine looked disappointing.

It was not. Look at what the wall clock was made of:

The parallel section went from 493 ms to 211 ms — 2.3× on four threads, which is unremarkable but real. The whole process barely moved, because the other half of it was a serial baseline that does not parallelise at all and was being included in every reading.

This is Amdahl’s law doing what it does, and it is easy to walk into: a benchmark that measures two things reports neither. The fix is not a better benchmark, it is a narrower one — time only the region that is supposed to be parallel.

Granularity

With the benchmark narrowed, here is the knob. 64×64, four generations, one thread and ten:

Coarser leaves are strictly worse here, which is the wrong way round from the usual advice — usually you coarsen tasks to amortise fork overhead. But note that blk=64 is already slower at one thread, where there is no fork overhead to amortise. So this is not a scheduling effect at all; the coarse-leaf implementation is doing more work. That is a fact about this code, and it took a second measurement to find the cause.

The refactor that flipped it

The same function had to be rewritten so that its correctness could be proved — that is the last part of this book. The change was to merge the tree-building and the flattening into one function, so that the join happens in place instead of in a second pass.

Both versions, measured in the same session, same machine:

Two things moved, in opposite directions.

Serial got about 18% faster. flatten had to walk the whole tree a second time to collect the results; the new version appends at the join and never revisits.

Parallel got worse, and the best granularity flipped from blk=1 to blk=16. The reason is visible once you look for it: app is serial work — concatenating two lists is one thread’s job — and the refactor moved it inside the fork-join region. So at every join, one worker is concatenating while its partner sits idle. The more joins there are, the more idle time; hence blk=1 degrading and the optimum moving to fewer, larger joins.

This is exactly 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.

An earlier version of this repository’s notes recorded “finer granularity is faster” as a finding about the scheduler. It is not. It was true of one implementation and stopped being true when that implementation changed. The rule that survives is narrower and more useful:

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.

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 the reason is now visible rather than mysterious: the joins are serial, and the naive engine’s inner loop — eight list walks per cell — is not a shape the scheduler can balance, because every walk is a different length.

The row-window engine from the previous chapter has none of those properties. It also does not need the cores.

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: making it move.

Making it move

The engine from the O(n) chapter is fast enough that animation is free. Forty by sixteen is 640 cells; at the measured rate of about 70 ns per cell per generation that is a rounding error. So this chapter is not about performance at all — it is about the two things that went wrong the first time, both of which are about text, and one of which is a good example of a bug that type-checks.

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. 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.

Everything else in the animation is that loop plus a renderer.

Trap 1: do not clear the screen

The first frame clears everything and hides the cursor:

IO.write("\u{1B}[?25l\u{1B}[2J")

After that, never again. [2J erases the whole screen, and doing it every frame makes the terminal blank and repaint — visible flicker on every generation. Instead each frame starts with [H, which moves the cursor to the top-left and overwrites in place:

def frame(+rs: Rows) -> String:
  String.append("\u{1B}[H", String.reverse(framerev(rs, SNil{})))

The visible difference is immediate and it is worth trying both ways once, because “clear the screen each frame” is the obvious implementation and it is the wrong one.

A note on writing the escape itself. 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.

Trap 2: String.reverse flips characters, not cells

This is the bug worth the chapter.

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.

Verifying it without watching it

“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 so that each has a distinguishable behaviour, and the behaviour was extracted and checked:

The glider’s coordinates were obtained by decoding each frame’s live cells and running a connected-component analysis on them — so the claim is “four frames, four component sets, each shifted by exactly (1,1) from the one before”, not “the shape looked like a glider”.

Streaming

One thing had to be confirmed before the animation was worth writing: does the output stream, or does it emerge all at once at the end? If the runtime buffers, the first 21 seconds are a blank screen and the last second is a mess.

It streams. Measured, native-compiled:

Roughly linear, starting immediately. That is the fact the whole animation rests on, and it is cheaper to check than to suspect.

Running it

cd life && bend life_anim.bend

320 generations × 70 ms ≈ 22 seconds. Both backends work; the compiled one is smoother.

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

Next: turning a belief into a compiler check.

Your first law and proof

Everything so far has been a program. This chapter is about the other thing Bend is for, and it is the reason the language exists at all.

Consider what we have been doing for four chapters. We wrote a parallel Life step, measured it, and concluded it computes the same thing as the sequential loop. We concluded that by testing it — running both, counting live cells, seeing 5 each time. That is evidence about the inputs we happened to try. It is not knowledge about the code.

Bend lets you replace it with something that is not evidence: a proof the compiler checks. Here is that claim, as a thing the compiler can read.

A law is a type

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.

(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.)

There is nothing imperative here and nothing to run. == is not a comparison that returns a Bool — it is a type, and the law tree_is_serial names the type “both sides are the same list”. A proof is a def of that type:

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

Note the shape. It is an ordinary function — it takes the law’s parameters and its body is induction on d, which is a match because Nat is a datatype. The case d = 0 is proved by {==}.

{==} is reflexivity

{==} is the proof of {x == x}: the two sides are already the same term.

That is the whole of the interesting content in this kind of proof. There is no tactic language, no auto, no simp. {==} is the only axiom and % is the only rule. So the entire craft is: move one side until it equals the other, one lemma at a time. The depth-0 case needs no work because a tree of depth zero is one leaf, and one leaf is the loop.

At depth p + 1, the tree is two depth-p trees joined, and the spec is one undecomposed loop. Something has to split that loop in two. That is the first non-trivial lemma.

%: applying a lemma

%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>}

%lemma(args) : P rewrites the goal using lemma. The rule, and it is the one thing to get right:

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 line above, 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 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}:

Nat.add recurses on its first argument. So when the first argument is a variable k, the term Nat.add(k, 0n) does not reduce — the reducer has nothing to match on. That is the entire reason add_zero exists: not because it is mathematically interesting, but because one side of an equation is stuck.

This is worth naming because it recurses through everything below. Base has no lemma library. 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.

Measured, on this machine:

Under a tenth of a second, including startup. 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 previous chapter’s law compared two functions that both compute Life. This one compares two functions that both compute a string, and it is the more interesting of the two — because the thing being proved is not an optimisation detail, it is a constraint we 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 the previous chapter: 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).

In the previous chapter that was a note in the source and a paragraph in the book. 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). That means a goal containing reverse(x) for a variable x is stuck, and the invariant has to be generalised over the accumulator before induction will go through. Hence reverse_go_spec(s, +acc), and rowrev_spec(r, +acc), and inner(rs, +acc) which is the law generalised over the accumulator:

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.

Parameter modifiers follow use, not meaning. A parameter that appears only in the type gets -; one that is used more than once in the proof body needs +. reverse_go_spec’s acc looks erased — the type mentions it twice, which is why it is tempting to write -acc — but it appears in the recursive call, so it must be +acc. The rule is mechanical once you look at the body, and wrong every time you reason about it semantically.

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.09 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}
  {==}

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.
• t11_templatemiss.bend says consumed more than once, which reads as “closures cannot be called twice”. The actual complaint is that ~ is missing at the call site. The corrected form is twice(~(x => (x + 1 : U32)), 40).

⚠️ 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.

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.

Two things to read here.

The speedup is only about 2.6–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 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/app/<version>/<hash>/bend2/base.bend

Measured, for Bend 2.0.5:

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 namespaces, by size:

Zero lemmas

grep -c -e '-> {' base.bend returns 0.

A lemma in Bend is a function whose return type is an equation, {a == b}. Base has none. Not one fact about Nat.add, not one about String.append, not one about List or Nat.mod or Nat.cmp.

This is the single most important fact in this appendix, and it 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 — 373 definitions covering lists, strings, maps, numbers, arrays, IO, files, TCP and UDP — and no reasoning library at all.

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.