# Quick reference

> The whole Brine language on one page, the same text `brine guide` prints.

Source: https://docs.brinelang.org/reference/quick-reference/

Brine is a compiled, verified, natively parallel language with Python-like syntax. Blocks use `:` plus 4-space indentation. Comments start with `#`. This page is the whole language on one page. The same text is built into the compiler, so it works offline and always matches the version you have installed:

```sh
brine guide
```

This page is the guide of Brine 0.4.0. For more detail on each part, see [values and types](/language/values-and-types/), [parallelism](/parallelism/overview/), [proofs](/proofs/contracts/), [the brine command](/tooling/cli/) and [error codes](/reference/errors/).

## Programs and commands

[Section titled “Programs and commands”](#programs-and-commands)

```sh
brine new hello && cd hello    # create a project (brine.toml, src/main.br, AGENTS.md)
brine run                      # build + run          brine run file.br -- args
brine check                    # type-check + prove   brine check --report
brine check --typed            # also require a written type on every variable
brine test                     # run test blocks      brine test "name filter"
brine fmt                      # format               brine fmt --check
brine run --ranks 4            # 4 cooperating processes (world module)
brine debug file.br            # debug build in gdb/lldb: break file.br:12, step, print x
brine explain E0601            # explain any error code
brine run --target wasm        # WebAssembly, run with Node.js (needs wasi-sdk, $WASI_SDK_PATH)
brine build --target web -o d  # d/: index.html + brine.js + program.wasm, for a browser
```

Add `--json` to any command for one JSON object per line. WebAssembly runs on one thread (`par` runs in order, same results) and as one `world` rank; in a browser there are no files or processes.

## Values and types

[Section titled “Values and types”](#values-and-types)

| Type                                                   | Examples                                                        |
| ------------------------------------------------------ | --------------------------------------------------------------- |
| `int` (= `i64`), `i8 i16 i32 i128 u8 u16 u32 u64 u128` | `42`, `1_000_000`, `0xff`, `0b1010`                             |
| `float` (= `f64`), `f32`                               | `3.14`, `1e-9`                                                  |
| `bool`                                                 | `true`, `false`                                                 |
| `str`                                                  | `"hi\n"`, `f"x = {x}, pi = {pi:.3f}"`                           |
| arrays `[T]`                                           | `[1, 2, 3]`, `[0.0] * n`, `[i * i for i in 0..n if i % 2 == 0]` |
| maps `{K: V}`                                          | `{"ann": 31, "bob": 27}`, `var m: {str: int} = {}`              |
| tuples `(A, B)`                                        | `(1, "one")`, `pair.0`                                          |
| structs                                                | `Point(x=1, y=2)` or `Point(1, 2)`                              |

* No implicit conversions. Convert explicitly: `float(i)`, `int(x)` (truncates), `i32(n)` (checked), `str(v)`, `int("42")` (parses), `float("2.5")`.
* Literals adapt to context: `let b: u8 = 200`, `let f: f32 = 1`, `let big: i128 = 10_000_000_000_000_000_000_000`. Integer literals go up to `u128`’s maximum (2^128 - 1); above `i128`’s maximum only a `u128` holds them.
* `i128` and `u128` need a 64-bit target (they’re a GCC/Clang feature). The prover can’t remove their overflow checks; those always run.
* Integer overflow, out-of-range conversions, division by zero and out-of-bounds indexing stop the program with a clear message (a *panic*), unless the compiler proved they can’t happen, in which case the check is removed.
* Integer `/` rounds down like Python’s `//` (`-7 / 2 == -4`), and `%` takes the sign of the right side (`-7 % 2 == 1`). Use `float(a) / float(b)` for a fractional result.
* Values are **values**: `let b = a` copies (cheaply, copy-on-write). Changing `b` never changes `a`. To share a variable on purpose, use `ref` (see Functions).

## Bindings

[Section titled “Bindings”](#bindings)

```brine
let x = 10              # immutable
var total = 0           # mutable
total += x
let (q, r) = (17 / 5, 17 % 5)   # tuple unpacking
let (a, (b, c)) = (1, (2, 3))   # nests
var names: [str] = []   # annotate when the type can't be inferred
let n: i32 = 7          # ...or whenever you like
for i: int in 0..3:     # loop variables too: `for k: str, v: int in m.items():`
    total += i
const LIMIT = 100       # compile-time constant (top level)
```

Types are optional, Python style. To require them, put `typed = true` under `[check]` in brine.toml (or pass `--typed`): then every `let`, `var` and `for` variable needs a written type (error E0337 tells you which one to add). No shadowing: a name can be declared only once per function. `_` ignores a value (`let (q, _) = ...`, `for _ in 0..n:`); it may repeat and can’t be read.

## Control flow

[Section titled “Control flow”](#control-flow)

```brine
if x < 0:
    print("negative")
elif x == 0:
    print("zero")
else:
    print("positive")


let sign = "neg" if x < 0 else "non-neg"   # conditional expression


for i in 0..n:          # 0, 1, ..., n-1        (also: 0..=n, range(a, b, step))
    pass
for x in xs:            # iterates over a snapshot of xs
    pass
for i, x in enumerate(xs):  # unpack tuples: (0, xs[0]), (1, xs[1]), ...
    pass
for i, (k, v) in enumerate(pairs):  # nested tuples too (also in comprehensions)
    pass
for c in "héllo":       # each UTF-8 character, as a one-character str
    pass
while k < n:
    k += 1              # break / continue work as usual
```

Comparisons chain: `0 <= i < n`. Logic is `and`, `or`, `not`.

## Functions

[Section titled “Functions”](#functions)

```brine
fn area(w: float, h: float) -> float:
    return w * h


fn fill(ref xs: [int], v: int):      # `ref` param: changes the caller's variable
    for i in 0..len(xs):
        xs[i] = v


fn countdown(mut n: int):            # `mut` param: a local copy the function may change
    while n > 0:
        n -= 1


fn main():
    var data = [0] * 10
    fill(ref data, 7)                # the caller says `ref` too
    let d = ref data                 # `d` is another name for `data`
    d[0] = 1                         # changes `data`
```

Arguments are passed by value (cheaply: arrays and strings are copy-on-write). References can’t be stored in structs or arrays or returned, so they never dangle. `main` may return `int` (the exit code). Parameter types are required; local types are inferred.

## Structs and methods

[Section titled “Structs and methods”](#structs-and-methods)

```brine
struct Particle:
    pos: float
    vel: float


    fn step(ref self, dt: float):    # method that modifies its receiver
        self.pos += self.vel * dt


    fn energy(self) -> float:
        return 0.5 * self.vel * self.vel


    fn at_rest(pos: float) -> Particle:   # no `self`: call as Particle.at_rest(1.0)
        return Particle(pos=pos, vel=0.0)


var p = Particle(pos=0.0, vel=2.0)
p.step(0.1)
print(p, p.energy())                 # Particle(pos=0.2, vel=2.0) 2.0
```

## Enums and `match`

[Section titled “Enums and match”](#enums-and-match)

```brine
enum Color:            # no data: a plain tag
    Red
    Green


enum Shape:
    Circle(radius: float)
    Rect(w: float, h: float)
    Empty


    fn area(self) -> float:          # enums can have methods
        match self:
            case Shape.Circle(r):
                return 3.14 * r * r
            case Shape.Rect(w, h):
                return w * h
            case Shape.Empty:
                return 0.0


enum Expr:                           # recursive enums are fine
    Num(value: int)
    Add(left: Expr, right: Expr)


let s = Shape.Rect(w=2.0, h=3.0)     # positional or keyword fields
print(s, s.area(), s == Shape.Empty) # Shape.Rect(w=2.0, h=3.0) 6.0 false
```

Patterns: `_`, a name (captures), int/str/bool literals, tuples `(a, 0)`, alternatives `1 | 2 | 3`, and variants `Shape.Rect(w, _)` / `Expr.Add(left=l)` (nested to any depth). A guard adds a condition: `case x if x < 0:`. Every `match` must handle every value (error E0320 shows one it misses); end with `case _:` when listing values isn’t possible. Variant data is read with `match`, never with `.field`.

## Generics, `Option` and `Result`

[Section titled “Generics, Option and Result”](#generics-option-and-result)

```brine
struct Pair[A, B]:
    first: A
    second: B


fn first[T](xs: [T]) -> Option[T]:     # type parameters in brackets
    if len(xs) == 0:
        return None
    return Some(xs[0])


fn parse_bit(s: str) -> Result[int, str]:
    if s == "0":
        return Ok(0)
    if s == "1":
        return Ok(1)
    return Err(f"not a bit: {s}")


let p = Pair(first=1, second="one")     # type arguments are inferred...
let q = Pair[int, str](first=2, second="two")   # ...or written out
let none: Option[int] = None           # `None` alone needs a known type
match first([3, 4]):
    case Some(x):
        print(x)
    case None:
        print("empty")
print(parse_bit("1").unwrap(), parse_bit("x").unwrap_or(-1))   # 1 -1
```

`x?` unwraps an `Option` or `Result`: it gives the value inside `Some`/`Ok`, or returns the `None`/`Err` from the current function at once (the function must return `Option[...]`, or `Result[..., E]` with the same `E`):

```brine
fn load(path: str) -> Result[int, str]:
    let text = read_file(path)?          # Err(...) is returned to the caller
    return parse_bit(text.strip())


fn main() -> Result[(), str]:           # an Err prints "error: ..." and exits with 1
    print(load("bit.txt")?)
    return Ok(())
```

`Option[T]` (`Some(value)`, `None`) and `Result[T, E]` (`Ok(value)`, `Err(error)`) are always available. Methods: `is_some()`, `is_none()`, `is_ok()`, `is_err()`, `unwrap()` (panics on `None`/`Err`), `unwrap_or(default)`, `ok()` (Result to Option). Each use of a generic function or type with new type arguments makes a specialized copy, so generic code is as fast as hand-written code. A generic function’s body is checked for each set of type arguments it’s used with: `largest[T]` that compares with `>` works for `int` and `str`, and is an error for a struct.

Methods can have type parameters of their own, next to their type’s:

```brine
struct Box[T]:
    v: T


    fn pair[U](self, u: U) -> (T, U):
        return (self.v, u)


let b = Box(v=1)
print(b.pair("x"), b.pair[float](2.5))   # (1, "x") (1, 2.5)
```

## Arrays

[Section titled “Arrays”](#arrays)

```brine
var xs = [3, 1, 2]
xs.push(5)              # append
let last = xs.pop()     # remove and return the last element (xs.pop(i): at i)
xs.insert(0, 9)         # put 9 at index 0, shifting the rest right
xs.extend([7, 8])       # append every element
xs.sort()               # numbers and strings; stable
xs.reverse()
xs.clear()
print(len(xs), xs == [3, 1, 2], 3 in xs, xs.index(3))  # index: Option[int]
print(xs.contains(3))   # the same as `3 in xs`
print(xs[1:3], xs[:2], xs[2:])   # slices are copies; out of range panics
```

There are no negative indexes: write `xs[len(xs) - 1]`. A statement can’t both change a variable and read it elsewhere (`print(xs.pop(), xs)` is an error), so evaluation order never matters.

## Strings

[Section titled “Strings”](#strings)

Strings are immutable UTF-8. `len(s)`, `s[i]` and slices count **bytes**; `s[i]` is a one-character string (ASCII text is the common case, and `for c in s` / `s.chars()` walk real characters).

```brine
let s = "hello, brine"
print(s[0], s[7:], s + "!", "ri" in s, s.contains("ri"), f"{s} has {len(s)} bytes")
print(s.find("brine"))                    # Some(7); None if absent
print(s.split(", "), "a b  c".split())    # ["hello", "brine"], ["a", "b", "c"]
print("-".join(["a", "b"]), "ab".repeat(3), s.replace("l", "L"))
print(s.starts_with("he"), s.ends_with("!"), s.count("l"))
print("  x ".strip(), "  x".lstrip(), "x  ".rstrip(), s.upper(), s.lower())
print("a\nb".lines(), s.chars(), s.bytes())  # [str], [str], [int]
print("42".is_digit(), "ab".is_alpha(), " ".is_space(), "a1".is_alnum())
print(ord("a"), chr(97))                   # 97 "a"
```

Case conversion and `is_alpha`/`is_space` follow Unicode, as in Python (`"straße".upper()` is `"STRASSE"`); `is_digit` is `0`-`9`, the digits `int()` reads. `str(x)` converts any printable value; `int("42")` and `float("2.5")` parse (and panic on bad input, so check with `is_digit` first when the text comes from outside).

## Maps

[Section titled “Maps”](#maps)

```brine
var ages = {"ann": 31, "bob": 27}   # {str: int}; remembers insertion order
ages["cy"] = 40                     # insert or replace
ages["ann"] += 1                    # missing keys panic: check with `in` first
if "bob" in ages:
    print(ages["bob"])
print(ages.get("zed"))              # Option[int]: None
print(ages.get("zed", 0))           # 0 (default)
ages.remove("bob")                  # true if it was there
for name in ages:                   # keys, in insertion order (a snapshot:
    print(name, ages[name])         # the loop body may change the map)
print(ages.keys(), ages.values(), ages.items(), len(ages))
```

Keys can be integers, `bool`, `str`, enums, or arrays/tuples/structs of those (not floats). Maps are values like everything else: `let b = a` copies (lazily).

## Built-ins

[Section titled “Built-ins”](#built-ins)

`print(a, b, ...)` (`sep=" "` goes between the values and `end="\n"` after them: `print(x, end="")`), `len`, `abs`, `min(a, b)`, `max(a, b)`, `sqrt`, `sin`, `cos`, `tan`, `exp`, `log`, `pow(x, y)`, `floor`, `ceil`, `round`, `clock()` (seconds), `args()` (command-line arguments), `exit(code)`, `panic(msg)`, `eprint(...)` (print to stderr), `ord(c)`, `chr(n)`, `enumerate(xs)`.

Files and processes (all failures are values, never crashes):

```brine
match read_file("in.txt"):              # Result[str, str]; text must be UTF-8
    case Ok(text):
        print(len(text.lines()))
    case Err(e):
        eprint(e)                       # "cannot read in.txt: No such file or directory"
write_file("out.txt", "hi\n")          # Result[(), str]
file_exists("out.txt")                  # bool
getenv("HOME")                          # Option[str]
run(["cc", "-O2", "-o", "app", "app.c"])  # Result[int, str]: Ok(exit code), Err if it can't start
```

`write_file` and `run` can’t be used inside `par` (their effects would happen in an unpredictable order).

The `os` module (built in, no import; errors are `Err` values with the OS’s message, e.g. `"The system cannot find the file specified. (os error 2)"`):

```brine
os.list_dir(path)       # Result[[str], str]: entry names (not paths), sorted, no "." / ".."
os.is_dir(path), os.is_file(path)            # bool
os.make_dir(path)       # Result[(), str]: creates missing parents; Ok if it exists
os.remove_file(path), os.rename(src, dst)    # Result[(), str]; rename replaces dst
os.cwd(), os.temp_dir() # str (temp_dir has no trailing separator)
os.set_cwd(path)        # Result[(), str]: change the working directory
os.write_bytes(path, b) # Result[(), str]: write a [u8] as a binary file
os.exe_path()           # str: the absolute path of the running program
os.abs_path(path)       # Result[str, str]: canonical; on Windows `\\?\C:\...`
os.name(), os.arch()    # "windows"/"macos"/"linux"..., "x86_64"/"aarch64"...
os.pid(), os.cpu_count()                     # int (cpu_count >= 1)
os.sleep(0.5)           # seconds
os.is_terminal(2)       # is fd 1 (stdout) / 2 (stderr) / 0 a terminal?
os.enable_ansi()        # Windows: let the console show color codes
os.free_ports(n)        # Result[[int], str]: n distinct free localhost TCP ports
let p = os.spawn(["cc", "x.c"], {"LANG": "C"}, true, false)?  # Result[int, str]: a handle
#   env: added to this process's environment; capture: collect stdout/stderr;
#   stdin: false gives the child an empty stdin. cmd[0] is searched on PATH.
os.wait(p)              # int: exit code (101 if killed by a signal)
os.poll(p)              # Option[int]: exit code if it has exited
os.kill(p)              # stop it
let (out, err) = os.output(p)   # captured text once it has exited ("" if not captured)
```

`os.spawn`, `wait`, `poll`, `kill`, `make_dir`, `remove_file`, `rename`, `sleep` and `enable_ansi` can’t be used inside `par`. Results of `os` calls (except `os.name()`/`os.arch()`) count as rank-dependent for `world` deadlock checks.

`embed("help.txt")` is a `str` with the file’s contents, read when the program is compiled (path: a string literal, relative to the file containing the call; `\r\n` becomes `\n`). It works in `const`s too: `const HELP = embed("help.txt")`. Reductions over generators: `sum(x * x for x in xs)`, `product`, `min`, `max`, `any(x < 0 for x in xs)`, `all(...)`. `min`/`max` of an empty sequence panic.

## Parallelism (data-race free by construction)

[Section titled “Parallelism (data-race free by construction)”](#parallelism-data-race-free-by-construction)

```brine
let ys = par [f(x) for x in xs]              # parallel map
let total = par sum(x * x for x in xs)        # parallel reduction
var out = [0.0] * n
par for i in 0..n:                            # parallel loop
    out[i] = xs[i] * 2.0                      # only out[i] of outer arrays may be written
let (a, b) = par(work(1), work(2))            # fork-join
```

Rules: inside a `par` body, outer variables are read-only, except that `par for i` may write `arr[i]` (exactly the loop variable) of an outer array. Reductions are deterministic: same result bits on any machine and thread count. They fold leaves of 16 consecutive elements left to right, then combine the leaves in a balanced pairwise tree (so `par sum` of floats can differ in the last bits from a sequential `sum`, usually by being more accurate). Integer overflow of any partial result in that order traps. `BRINE_THREADS=n` or `brine run --threads n` sets the thread count.

**GPUs.** `par for`, `par [...]` and `par` reductions also run on a GPU (NVIDIA through CUDA, Apple silicon through Metal) when the runtime expects that to be faster (big constructs with much work per byte copied); the results are the same bits, and a failing check panics as on the CPU. On Apple GPUs, f64 code stays on the CPU (they have no f64). Nothing to write or install beyond the driver: the compiler makes a kernel of every body that only uses int/float arithmetic, comparisons, branches, loops, structs, tuples, reads of outer arrays and scalars, `out[i]` writes, `sqrt`, `abs`, `floor`, `ceil`, `round`, `min`, `max`, and calls to functions that do the same. Strings, maps, new arrays, printing, `sin`/`exp`/`log`/`pow` and the like keep a body on the CPU. `BRINE_GPU=off|on|auto` (default `auto`; `on` uses the GPU whenever it can), `BRINE_GPU_LOG=1` prints where each construct ran and why.

## Multiple processes and machines: `world`

[Section titled “Multiple processes and machines: world”](#multiple-processes-and-machines-world)

```brine
fn main():
    let rank = world.rank()           # 0 .. world.size()-1
    let local = sum(i for i in 0..1000 if i % world.size() == rank)
    let total = world.sum(local)      # every rank gets the total
    if rank == 0:
        print(total)
    let left = world.shift(rank, 1)       # send to rank + 1, receive from rank - 1
    let inbox = world.exchange([rank] * world.size())   # xs[j] goes to rank j
```

API: `rank()`, `size()`, `barrier()`, `broadcast(root, v)`, `sum(v)`, `min(v)`, `max(v)`, `gather_all(v) -> [T]`, `shift(v, by)`, `exchange(xs) -> [T]`. Message types: `int`, `float`, `bool`, `str`, and arrays of those (`[[float]]`, …). Run with `brine run --ranks N`. Without it, `world.size() == 1`.

**No deadlocks, by construction.** Every rank takes part in every `world` call, and the compiler checks that all ranks make the same calls in the same order: a call under a condition that depends on `world.rank()` (or received values, `clock()`, …) is an error (E0510). Results of `sum`/`min`/`max`/`broadcast`/ `gather_all` are the same on every rank, so loops like `while world.max(err) > tol:` are fine.

## Proofs: rules that can’t be broken

[Section titled “Proofs: rules that can’t be broken”](#proofs-rules-that-cant-be-broken)

```brine
fn clamp(x: int, lo: int, hi: int) -> int:
    requires lo <= hi                 # every caller must prove this
    ensures lo <= result <= hi        # proven for every return
    if x < lo:
        return lo
    if x > hi:
        return hi
    return x


fn index_of(xs: [int], target: int) -> int:
    ensures -1 <= result < len(xs)
    var lo = 0
    var hi = len(xs)
    while lo < hi:
        invariant 0 <= lo <= hi <= len(xs)     # holds before every iteration
        let mid = lo + (hi - lo) / 2
        if xs[mid] == target:                  # bounds check proven: removed
            return mid
        if xs[mid] < target:
            lo = mid + 1
        else:
            hi = mid
    return -1
```

* `requires`, `ensures`, `invariant` and `prove e` **must** be proven at compile time; if the prover can’t, it’s an error listing the facts it knew.
* `assert e` checks at runtime (always, in every build) and is a known fact afterwards. Use it to hand the prover a fact it can’t derive itself.
* Specs may use arithmetic, comparisons, `and`/`or`/`not`, `len`, `abs`, `min`, `max`, fields, indexing, constants and `result`.
* In `for i in a..b` loops, invariants may mention `i`: they must hold at the start of each iteration (and with `i = b` after the loop).
* The prover handles linear integer arithmetic (`+ - `and multiplication or division by constants). It never accepts a false claim.
* `brine check --report` lists the runtime checks that remain.

## Modules

[Section titled “Modules”](#modules)

```brine
import geometry            # loads geometry.br next to the main file
import util.strings as s   # loads util/strings.br


let a = geometry.area(2.0, 3.0)
let p = geometry.Point(x=1, y=2)


from geometry import Point, area   # use these names directly
let q = Point(x=3, y=4)
```

`from m import x` only imports items defined in `m` itself. A name can’t be both imported and defined in the same module.

## Tests

[Section titled “Tests”](#tests)

```brine
test "clamp keeps values in range":
    assert clamp(15, 0, 10) == 10
    assert clamp(-5, 0, 10) == 0
```

`brine test` runs each test in its own process, in parallel. `$BRINE` is set to the `brine` running the tests, so a test can run the compiler.

## C interop

[Section titled “C interop”](#c-interop)

```brine
extern fn rand() -> i32     # declare a C standard library function (ints, floats, bools only)
```