Start here

A tour of Brine

This page walks through Brine in about fifteen minutes. Every example is a whole program that compiles; paste one into tour.br and run it with brine run tour.br. Each section links to the page that covers its topic in full.

Hello, Brine

fn main():
    print("Hello, brine!")

Blocks start with : and are indented 4 spaces, as in Python. Functions use fn, and the program starts at main. Comments start with #.

Values and types

fn main():
    let n = 42                      # int (64-bit)
    let x = 2.5                     # float (64-bit)
    let small: u8 = 200             # literals adapt to the type
    let ok = n > 10 and not (x < 0.0)
    let name = "brine"
    let point = (3, 4)              # tuple
    print(n, x, small, ok, name, point.0)
    print(f"{name} has {len(name)} letters, x = {x:.3f}")
    print(float(n) * x, int(x), str(n) + "!")
    print(-7 / 2, -7 % 2)          # integer `/` rounds down

42 2.5 200 true brine 3
brine has 5 letters, x = 2.500
105.0 2 42!
-4 1

Types are static and inferred. There are no implicit conversions: an int and a float don’t mix until you write float(n) or int(x). Integer overflow, division by zero and out-of-range conversions stop the program with a clear message (a panic) unless the compiler proves they can’t happen. More in Values and types.

Bindings

fn main():
    let limit = 10                  # immutable
    var total = 0                   # mutable
    for i in 0..limit:
        total += i
    let (q, r) = (17 / 5, 17 % 5)   # unpack a tuple
    var names: [str] = []           # annotate when it can't be inferred
    names.push("ann")
    print(total, q, r, names)

45 3 2 ["ann"]

let can’t change, var can. A name is declared once per function: there’s no shadowing. More in Bindings.

Control flow

fn classify(x: int) -> str:
    if x < 0:
        return "negative"
    elif x == 0:
        return "zero"
    return "small" if x < 10 else "large"

fn main():
    for x in [-3, 0, 7, 12]:
        print(x, classify(x))
    var k = 1
    while k < 100:
        k *= 3
    print(k, 0 <= k < 1000)

-3 negative
0 zero
7 small
12 large
243 true

0..n counts from 0 to n - 1 and 0..=n includes n. Comparisons chain, and logic is and, or, not. More in Control flow.

Functions and values

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

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

fn main():
    print(area(2.0, 3.5))
    let a = [1, 2, 3]
    var b = a                       # a copy (cheap: copy-on-write)
    b[0] = 99
    print(a, b)
    fill(ref b, 7)                  # the caller writes `ref` too
    print(b)

7.0
[1, 2, 3] [99, 2, 3]
[7, 7, 7]

Everything is a value: assigning or passing an array copies it, so changing b never changes a. Copies are cheap because arrays and strings are shared until one side changes. To let a function change your variable, it declares a ref parameter and you pass ref b, so it’s visible at the call. More in Functions.

Structs and methods

struct Particle:
    pos: float
    vel: float

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

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

fn main():
    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

Methods go inside the struct. A method that changes its receiver takes ref self. More in Structs.

Enums and match

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

    fn area(self) -> float:
        match self:                  # must cover every case
            case Shape.Circle(r):
                return 3.14159 * r * r
            case Shape.Rect(w, h):
                return w * h
            case Shape.Empty:
                return 0.0

fn describe(n: int) -> str:
    match n:
        case 0:
            return "zero"
        case 1 | 2 | 3:
            return "a few"
        case x if x < 0:
            return "negative"
        case _:
            return "many"

fn main():
    let shapes = [Shape.Circle(radius=1.0), Shape.Rect(w=2.0, h=3.0), Shape.Empty]
    for s in shapes:
        print(s, s.area())
    print(describe(2), describe(-5), describe(40))

Shape.Circle(radius=1.0) 3.14159
Shape.Rect(w=2.0, h=3.0) 6.0
Shape.Empty 0.0
a few negative many

Each enum variant can carry its own fields. A match must handle every possible value; leave out case Shape.Empty: and the program doesn’t compile (E0320). More in Enums and match and Generics.

Option, Result and ?

fn first_even(xs: [int]) -> Option[int]:
    for x in xs:
        if x % 2 == 0:
            return Some(x)
    return None

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

fn parse_pair(a: str, b: str) -> Result[int, str]:
    let hi = parse_bit(a)?           # an Err returns from parse_pair at once
    let lo = parse_bit(b)?
    return Ok(hi * 2 + lo)

fn main():
    print(first_even([1, 3, 4, 5]), first_even([1, 3]))
    print(parse_pair("1", "0"), parse_pair("1", "x"))
    match parse_pair("1", "1"):
        case Ok(v):
            print("value", v)
        case Err(e):
            print("error", e)
    print(first_even([7]).unwrap_or(-1))

Some(4) None
Ok(2) Err("not a bit: x")
value 3
-1

Brine has no exceptions and no null. A function that can fail returns Result[T, E]; a value that may be missing is Option[T]. x? gives the value inside, or returns the Err/None to the caller. File and process functions such as read_file return Result too. More in Error handling.

Arrays, strings and maps

fn main():
    var xs = [3, 1, 2]
    xs.push(5)
    xs.sort()
    let evens = [x * x for x in 0..10 if x % 2 == 0]
    print(xs, xs[1:3], xs[len(xs) - 1], evens)

    let s = "hello, brine"
    print(s.split(", "), s.upper(), s.find("brine"), s[0:5])

    var ages = {"ann": 31, "bob": 27}
    ages["cy"] = 40
    print(ages.get("zed"), "bob" in ages, ages.keys())

[1, 2, 3, 5] [2, 3] 5 [0, 4, 16, 36, 64]
["hello", "brine"] HELLO, BRINE Some(7) hello
None true ["ann", "bob", "cy"]

There are no negative indexes: the last element is xs[len(xs) - 1]. Strings are UTF-8 and index by bytes. Reading a missing map key panics, so test with in or use get. More in Arrays, Strings and Maps.

Parallel code with par

fn collatz_len(n: int) -> int:
    var x = n
    var steps = 0
    while x != 1:
        x = x / 2 if x % 2 == 0 else 3 * x + 1
        steps += 1
    return steps

fn main():
    let n = 1_000_000
    let lens = par [collatz_len(i) for i in 1..=n]       # parallel map
    let longest = par max(l for l in lens)               # parallel reduction
    let total = par sum(float(l) for l in lens)
    print(f"longest: {longest}, average: {total / float(n):.2f}")

    var out = [0.0] * 8
    par for i in 0..8:                                   # parallel loop
        out[i] = sqrt(float(i))                          # writes only out[i]
    print(out)

    let (a, b) = par(collatz_len(27), collatz_len(97))   # fork-join
    print(a, b)

longest: 524, average: 131.43
[0.0, 1.0, 1.4142135623730951, 1.7320508075688772, 2.0, 2.23606797749979, 2.449489742783178, 2.6457513110645907]
111 118

Construct	Meaning
`par for i in lo..hi:`	a loop whose iterations run on every core
`par [e for i in lo..hi]`	a parallel map
`par sum(e for ...)`	a parallel reduction: `sum`, `product`, `min`, `max`, `any`, `all`
`par(f(a), g(b))`	run independent expressions at the same time; returns a tuple

The thread count defaults to every core; brine run --threads 4 or BRINE_THREADS=4 changes it. More in Parallelism.

Data races are compile errors

Inside a par body, variables from outside are read-only, except that a par for may write its own element of an outer array (out[i]). Break the rule and the program doesn’t compile:

fn main():
    let xs = [1, 2, 3, 4]
    var total = 0
    par for i in 0..len(xs):
        total += xs[i]
    print(total)

error[E0501]: cannot assign to `total` inside a `par` body
 --> race.br:5:9
  |
5 |         total += xs[i]
  |         ^^^^^ would be a data race
  |
  = note: `total` is shared by all parallel iterations
  = help: a `par for` may only write `total[i]` (its own element); to combine values use `par sum(...)`, `par [...]`, or a sequential loop
  = run `brine explain E0501` for more about this error
error: could not compile due to 1 error

The fix is a reduction:

fn main():
    let xs = [1, 2, 3, 4]
    let total = par sum(x for x in xs)
    print(total)

The same bits on every machine

A par reduction combines its elements in one fixed order that depends only on how many there are, never on how many threads run. A float par sum gives the same bits on 1 thread, 32 threads, or a GPU:

fn main():
    let xs = [1.0 / float(i) for i in 1..=1_000_000]
    let seq = sum(x for x in xs)                 # left to right
    let tree = par sum(x for x in xs)            # fixed tree order
    print(f"{seq:.17f}")
    print(f"{tree:.17f}")

brine run determ.br --threads 1
brine run determ.br --threads 32

14.39272672286498889
14.39272672286572430

The par sum can differ from a left-to-right sum in the last bits. It is usually closer to the exact answer: here the exact sum is 14.3927267228657236… More in Deterministic reductions.

GPUs without annotations

The same par constructs can run on an NVIDIA GPU (CUDA) or an Apple GPU (Metal). You don’t change the code or install anything beyond the driver:

fn main():
    let n = 4_000_000
    let xs = par [float(i) * 0.001 for i in 0..n]
    var ys = [0.0] * n
    par for i in 0..n:
        var v = xs[i]
        for k in 0..200:
            v = v * 0.999 + 0.001
        ys[i] = sqrt(v)
    print(par sum(y for y in ys))

brine run gpu.br --release                   # GPU when it's faster
BRINE_GPU=off brine run gpu.br --release     # CPU only
BRINE_GPU=on brine run gpu.br --release      # GPU whenever it can
BRINE_GPU_LOG=1 brine run gpu.br --release   # where each `par` ran, and why

152610131.78961766

The compiler decides which bodies can run on a GPU (numeric code, loops, structs, array reads and out[i] writes). The runtime measures each construct and moves it to the GPU only when it expects that to be faster. Results are the same bits either way. More in GPU offload.

Many processes with world

The built-in world module runs one program as several cooperating processes, MPI style:

fn main():
    let rank = world.rank()
    let size = world.size()

    var local = 0
    for i in 0..1_000_000:
        if i % size == rank:
            local += i
    let total = world.sum(local)                 # every rank gets the total

    let all = world.gather_all(rank * rank)      # everyone gets everyone's value
    if rank == 0:
        print(f"{size} ranks, total = {total}, squares = {all}")

brine run world.br --ranks 4

4 ranks, total = 499999500000, squares = [0, 1, 4, 9]

Every world call is collective, and the compiler checks that all ranks make the same calls in the same order, so the program can’t deadlock:

fn main():
    if world.rank() == 0:
        let total = world.sum(1)
        print(total)

error[E0510]: some ranks might not reach this communication
 --> dead.br:3:21
  |
3 |         let total = world.sum(1)
  |                     ^^^^^^^^^^^^ calls `world.sum`
2 |     if world.rank() == 0:
  |        ----------------- this may differ between ranks
  |
  = note: every rank must make the same `world` calls in the same order, otherwise the program could hang
  = help: move the call out of the rank-dependent branch or loop; compute rank-specific values first, then communicate on every rank
  = run `brine explain E0510` for more about this error
error: could not compile due to 1 error

More in The world module and Deadlock freedom.

Contracts the compiler proves

fn clamp(x: int, lo: int, hi: int) -> int:
    requires lo <= hi                 # every caller must prove this
    ensures lo <= result <= hi        # the compiler proves this
    if x < lo:
        return lo
    if x > hi:
        return hi
    return x

fn last(xs: [int]) -> int:
    requires len(xs) >= 1
    return xs[len(xs) - 1]            # in bounds: no runtime check

fn main():
    let xs = [4, 8, 15]
    print(clamp(15, 0, 10), last(xs))

10 15

requires, ensures, invariant and prove are checked at compile time. If the compiler can’t prove one, it’s an error, with the facts it knew. Call last with an empty array and the program doesn’t compile:

fn last(xs: [int]) -> int:
    requires len(xs) >= 1
    return xs[len(xs) - 1]

fn main():
    let xs: [int] = []
    print(last(xs))

error[E0601]: cannot prove the precondition of `last`
 --> proof.br:7:11
  |
7 |     print(last(xs))
  |           ^^^^^^^^ this call might violate `requires len(xs) >= 1`
2 |     requires len(xs) >= 1
  |              ------------ precondition declared here
  |
  = note: with the values used here, this is always false
  = help: add an `assert` before the call to check it at runtime, or a `requires` to this function so its callers must prove it
  = run `brine explain E0601` for more about this error
error: could not compile due to 1 error

assert is the runtime counterpart: it’s checked when the program runs, in every build, and the prover treats it as a fact afterwards. There’s no flag to turn checks off. More in Proofs, Contracts and Fixing proof failures.

Tests

fn clamp(x: int, lo: int, hi: int) -> int:
    requires lo <= hi
    ensures lo <= result <= hi
    if x < lo:
        return lo
    if x > hi:
        return hi
    return x

fn main():
    print(clamp(15, 0, 10))

test "clamp stays in range":
    assert clamp(15, 0, 10) == 10
    assert clamp(-5, 0, 10) == 0

test "clamp keeps values inside":
    assert clamp(7, 0, 10) == 7

brine test clamp.br

     Built tests [dev] in 0.10s
test clamp stays in range ... ok
test clamp keeps values inside ... ok

test result: ok. 2 passed; 0 failed; finished in 0.03s

Tests live next to the code. brine test runs each one in its own process, in parallel. More in Testing.

Where to go next

Coming from Python: the differences that trip people up.
The language: every feature in detail, plus modules, built-ins, the os module and C interop.
Quick reference: the whole language on one page (also brine guide).
Using Brine with coding agents.