Start here

Coming from Python

Brine reads like Python, so most of what you know carries over: indentation, for loops, comprehensions, f-strings, slices. The differences come from Brine being compiled, statically typed and safe to run in parallel. Most are compile errors with a code and a fix, so the compiler tells you when a Python habit doesn’t apply. The ones to remember: declare variables with let or var, convert numbers explicitly, values are copied, and failures are Result values, not exceptions.

What carries over

fn main():
    let words = ["brine", "is", "a", "language"]
    let lengths = [len(w) for w in words if len(w) > 1]   # comprehension
    for i, w in enumerate(words):                         # enumerate, unpacking
        if i == 0:
            print(f"{w:>8} first")                        # f-string with a format
        elif len(w) < 3:
            continue
        else:
            print(f"{w:>8} {len(w)}")
    print(lengths, words[1:3], words[:2])                  # slices
    print("is" in words, "x" not in words, 0 <= len(words) < 10)
    print(" ".join(words).upper(), "a,b".split(","), "  pad ".strip())
    let (q, r) = (17 / 5, 17 % 5)                         # tuple unpacking
    print(q, r, 'single quotes work too', max(lengths), sum(lengths))
    for i in range(10, 0, -3):
        print(i, end=" ")
    print()

   brine first
language 8
[5, 2, 8] ["is", "a"] ["brine", "is"]
true true true
BRINE IS A LANGUAGE ["a", "b"] pad
3 2 single quotes work too 8 15
10 7 4 1

Also the same: # comments, while, break, continue, pass, and, or, not, a if cond else b, match/case, print(..., sep=, end=), str(x), int("42"), float("2.5"), and most string methods. Files end in .br and use 4-space indentation (tabs are an error).

At a glance

Python	Brine	Notes
`def f(x):`	`fn f(x: int) -> int:`	parameter and return types are required (E0110)
`class Point:`	`struct Point:`	fields with types, methods inside (E0110)
`x = 1`	`let x = 1` / `var x = 1`	`let` can’t change; `var` can
`x = 2` (new name, same scope)	a new name	no shadowing (E0207)
`True`, `False`, `None`	`true`, `false`, `None`	`None` needs a known `Option` type (E0332)
`n * 0.5` with `n: int`	`float(n) * 0.5`	no implicit conversions (E0305)
`7 // 2`	`7 / 2`	integer `/` already rounds down; `//` is E0105
`7 / 2` → `3.5`	`float(7) / float(2)`
`2 ** 10`	`pow(2.0, 10.0)`	no `**` operator; `pow` takes floats
`xs[-1]`	`xs[len(xs) - 1]`	no negative indexes (panics at runtime)
`b = a` (same list)	`b = a` (a copy)	values, not shared references
`f(xs)` changes `xs`	`f(ref xs)`	the function declares `ref xs: [int]`
`xs.append(x)`	`xs.push(x)`	E0206 suggests the name
`sorted(xs)`	`var ys = xs` then `ys.sort()`	`sort` is in place
`"ab" * 3`	`"ab".repeat(3)`
`d[k]` raises `KeyError`	`d[k]` panics	test `k in d`, or use `d.get(k)`
`if xs:`	`if len(xs) > 0:`	conditions must be `bool` (E0307)
`x is None`	`x == None` or `x.is_none()`
`try` / `except`	`Result`, `match`, `?`	no exceptions
`else if`	`elif`	E0114, with a fix
`a, b = b, a`	`let (x, y) = (b, a)`	no multiple assignment to existing variables
`lambda x: x + 1`	a named `fn`	no lambdas
`def f(x, y=0)`	two functions, or pass `y`	no default arguments
`f(y=1, x=2)`	`f(x=2, y=1)`	keyword arguments must be in parameter order (E0302)
`{k: v for ...}`	a loop that fills a `var m: {K: V} = {}`	list comprehensions only
`import math`; `math.sqrt(x)`	`sqrt(x)`	math functions are built-ins; `import` loads your own `.br` files
global variables	`const` at the top level, or pass values	statements go inside functions
`"""multi-line"""`	`"line 1\nline 2"`	strings end on the line they start
`xs[::2]`	`[xs[i] for i in range(0, len(xs), 2)]`	slices have no step

Declaring variables: let and var

Every variable is declared once, with let (can’t change) or var (can). Assigning to a name that was never declared is an error, and so is changing a let:

fn main():
    let count = 0
    for i in 0..3:
        count += i
    print(count)

error[E0401]: cannot assign to `count` because it was declared with `let`
 --> letlet.br:4:9
  |
4 |         count += i
  |         ^^^^^ immutable
2 |     let count = 0
  |         ----- declared here
  |
  = help: declare it with `var count = ...` to make it mutable
  = run `brine explain E0401` for more about this error
error: could not compile due to 1 error

fn main():
    total = 0
    print(total)

error[E0201]: cannot assign to undefined variable `total`
 --> varundecl.br:2:5
  |
2 |     total = 0
  |     ^^^^^ not declared
  |
  = help: declare it first: `var total = ...`
  = run `brine explain E0201` for more about this error
error[E0201]: cannot find value `total`
 --> varundecl.br:3:11
  |
3 |     print(total)
  |           ^^^^^ not found in this scope
  = run `brine explain E0201` for more about this error
error: could not compile due to 2 errors

A name can be declared only once per function, even in an inner block. Python lets you rebind x = int(x); in Brine, pick a new name:

fn main():
    let x = 1
    let x = 2
    print(x)

error[E0207]: `x` is already defined in this function
 --> shadow.br:3:9
  |
3 |     let x = 2
  |         ^ defined again here
2 |     let x = 1
  |         - first defined here
  |
  = help: brine doesn't allow shadowing; pick a new name, or declare it with `var` and assign to it
  = run `brine explain E0207` for more about this error
error: could not compile due to 1 error

Why: a name that means one thing for the whole function is easier to read and lets the prover reason about it. See Bindings.

Static types

Local types are inferred, but function parameters and return values need types, and a variable keeps its type:

fn double(x):
    return x * 2

fn main():
    print(double(2))

error[E0110]: parameter `x` needs a type
 --> noparamtype.br:1:12
  |
1 | fn double(x):
  |            ^ expected `: type`
  |
  = help: write `x: int` (or another type)
  = run `brine explain E0110` for more about this error
error: could not compile due to 1 error

int is a 64-bit integer, not Python’s unlimited one. Overflow stops the program with a panic instead of giving a wrong answer, and a literal that doesn’t fit is a compile error (E0315). Use i128 or u128 for bigger numbers. See Values and types.

No implicit conversions

An int and a float never mix on their own, not even in ==. Convert one side:

fn mean(xs: [float]) -> float:
    return sum(x for x in xs) / len(xs)

fn main():
    print(mean([1.0, 2.0, 3.0]))

error[E0305]: cannot divide `float` and `int`
 --> conv.br:2:12
  |
2 |     return sum(x for x in xs) / len(xs)
  |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ `/` with mismatched operands
  |
  = help: brine never converts numbers implicitly; use `float(x)` or `int(x)`
  = run `brine explain E0305` for more about this error
error: could not compile due to 1 error

fn mean(xs: [float]) -> float:
    return sum(x for x in xs) / float(len(xs))

fn main():
    print(mean([1.0, 2.0, 3.0]))

The same goes for strings: "n = " + n is an error; write f"n = {n}" or "n = " + str(n). Literals adapt to their context, so let f: float = 1 and let b: u8 = 200 are fine.

Integer division rounds down

/ on two integers gives an integer, rounded down like Python’s //. % takes the sign of the right side, as in Python. Python’s // is an error that points you to /:

fn main():
    print(7 / 2, -7 / 2, -7 % 2, float(7) / float(2))

3 -4 1 3.5

fn main():
    print(7 // 2)

error[E0105]: `//` is not an operator in brine
 --> floordiv.br:2:13
  |
2 |     print(7 // 2)
  |             ^^ use `/`
  |
  = note: `/` on integers already rounds down like Python's `//`; comments start with `#`
  = run `brine explain E0105` for more about this error
error: could not compile due to 1 error

Values are copied

In Python, b = a makes two names for one list. In Brine it makes a copy, and so does passing an argument. Copies are cheap (arrays and strings are shared until one side changes), and a change through one name never shows up in another:

fn main():
    let a = [1, 2, 3]
    var b = a
    b.push(4)
    var grid = [[0] * 3] * 2       # two separate rows, unlike Python
    grid[0][0] = 1
    print(a, b, grid)

[1, 2, 3] [1, 2, 3, 4] [[1, 0, 0], [0, 0, 0]]

Parameters are read-only. To change the caller’s variable, the function declares a ref parameter and the caller writes ref as well, so you can see it at the call:

fn add_item(xs: [int]):
    xs.push(4)

fn main():
    var xs = [1, 2, 3]
    add_item(xs)
    print(xs)

error[E0403]: cannot push to parameter `xs`
 --> alias.br:2:5
  |
2 |     xs.push(4)
  |     ^^ parameters are read-only
1 | fn add_item(xs: [int]):
  |             -- declared here
  |
  = help: to change a local copy, declare it `mut xs: ...`; to change the caller's variable, declare it `ref xs: ...` and call with `ref`
  = run `brine explain E0403` for more about this error
error: could not compile due to 1 error

fn add_item(ref xs: [int]):
    xs.push(4)

fn main():
    var xs = [1, 2, 3]
    add_item(ref xs)
    print(xs)

Why: with no hidden sharing, two par iterations can’t change the same list behind your back, which is what makes race freedom checkable. See Functions.

No negative indexes

xs[-1] is not the last element. It’s an out-of-bounds index, and the program stops when it reaches it:

fn main():
    let xs = [1, 2, 3]
    print(xs[-1])

panic: index -1 is out of bounds for an array of length 3
  --> negidx.br:3:11

Write xs[len(xs) - 1]. Slices don’t take negative bounds either: xs[len(xs) - 2:] is the last two elements.

Strings index by bytes

Strings are UTF-8. len(s), s[i] and slices count bytes, not characters. For ASCII text that’s the same thing. To walk characters, use for c in s or s.chars():

fn main():
    let s = "héllo"
    print(len(s), len(s.chars()), s[0], s[1:3])
    for c in s:
        print(c, end=" ")
    print()

6 5 h é
h é l l o

é takes two bytes, so s[1:3] is "é" and len(s) is 6. Strings can’t be changed in place (s[0] = "x" is E0404); build a new one. See Strings.

Missing map keys panic

Reading a key that isn’t there stops the program. There’s no KeyError to catch. Test first, or use get, which returns an Option:

fn main():
    let ages = {"ann": 31}
    if "bob" in ages:
        print(ages["bob"])
    print(ages.get("bob"), ages.get("bob", 0), ages.get("ann"))

None 0 Some(31)

Without the check, ages["bob"] prints panic: key "bob" is not in the map. See Maps.

match covers every case

match looks like Python’s, but it must handle every possible value. A missing case is a compile error that names it:

enum Color:
    Red
    Green
    Blue

fn name(c: Color) -> str:
    match c:
        case Color.Red:
            return "red"
        case Color.Green:
            return "green"

fn main():
    print(name(Color.Blue))

error[E0320]: this `match` doesn't handle every possible value
 --> nomatch.br:7:11
  |
7 |     match c:
  |           ^ of type `Color`
  |
  = note: not handled: `Color.Blue`
  = help: add `case Color.Blue:`, or a catch-all `case _:`
  = run `brine explain E0320` for more about this error
error: could not compile due to 1 error

See Enums and match.

No exceptions: Result and ?

There is no try, except or raise. A function that can fail returns Result[T, E], and the caller decides what to do. x? returns the error to the caller, like an exception propagating, but visible in the code and in the function’s type:

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)?
    let lo = parse_bit(b)?
    return Ok(hi * 2 + lo)

fn main():
    match parse_pair("1", "x"):
        case Ok(v):
            print(v)
        case Err(e):
            print("error:", e)

error: not a bit: x

File and process functions return Result too: read_file(path) is a Result[str, str], never a crash. panic(msg) is for bugs, and can’t be caught. main may return Result[(), str]; an Err prints error: ... and exits with status 1. See Error handling.

None needs a type

None is a value of Option[T], so Brine needs to know the T. There’s no null:

fn main():
    let x = None
    print(x)

error[E0332]: can't infer which `Option` type `None` belongs to
 --> none.br:2:13
  |
2 |     let x = None
  |             ^^^^ type unknown here
  |
  = help: add a type annotation, e.g. `let x: Option[int] = None`
  = run `brine explain E0332` for more about this error
error: could not compile due to 1 error

fn main():
    let x: Option[int] = None
    print(x == None, x.is_none(), x.unwrap_or(5))

Conditions must be bool

There’s no truthiness. An empty list, 0 or "" isn’t false; write the test you mean:

fn main():
    let xs = [1]
    if xs:
        print("non-empty")

error[E0307]: condition must be a `bool`, found `[int]`
 --> truthy.br:3:8
  |
3 |     if xs:
  |        ^^ not a bool
  |
  = help: check the length explicitly, e.g. `len(xs) > 0`
  = run `brine explain E0307` for more about this error
error: could not compile due to 1 error

Keywords and operators

Brine uses fn, struct and elif. The compiler recognizes the spellings from Python and other languages and says what to write instead:

def add(a: int, b: int) -> int:
    return a + b

fn main():
    print(add(1, 2))

error[E0110]: brine uses `fn` to define functions
 --> def.br:1:1
  |
1 | def add(a: int, b: int) -> int:
  | ^^^ use `fn` here
  = run `brine explain E0110` for more about this error
error: could not compile due to 1 error

fn main():
    let x = 3
    if x < 0:
        print("neg")
    else if x == 0:
        print("zero")

error[E0114]: use `elif` instead of `else if`
 --> elif.br:5:5
  |
5 |     else if x == 0:
  |     ^^^^^^^ write `elif`
  = run `brine explain E0114` for more about this error
error: could not compile due to 1 error

Operators from C-like languages are E0105, and braces or semicolons are E0106:

Written	Error	Write instead
`a && b`, `a \|\| b`, `!a`	E0105	`a and b`, `a or b`, `not a`
`i++`, `i--`	E0105	`i += 1`, `i -= 1`
`7 // 2`	E0105	`7 / 2`
`x > 0 ? a : b`	E0110	`a if x > 0 else b`
`fn main() {`	E0106	`fn main():` and an indented block
`print(1);`	E0106	`print(1)`
`class P:`	E0110	`struct P:`
`True`	E0201	`true`

One change per expression

An expression can’t change a variable and also read it, or change it twice. Python evaluates left to right; Brine rules out the question:

fn main():
    var xs = [1, 2, 3]
    print(xs.pop(), xs)

error[E0405]: `xs` is changed and also read in the same expression
 --> twovars.br:3:11
  |
3 |     print(xs.pop(), xs)
  |           ^^^^^^^^ changed here
  |                     -- read here
  |
  = help: make the change in its own statement first, then use the result
  = run `brine explain E0405` for more about this error
error: could not compile due to 1 error

Split it in two: let last = xs.pop(), then print(last, xs).

Summary

Declare with let or var; declare each name once per function.
Write parameter and return types; convert numbers with float(), int().
Integer / rounds down; there’s no // or **.
Assignment and arguments copy. Use ref to change a caller’s variable.
No negative indexes; strings index by bytes; missing map keys panic.
match must be exhaustive; None needs a type; conditions must be bool.
Failures are Result values passed up with ?, not exceptions.
fn, struct, elif, and/or/not, true/false.

Next: A tour of Brine covers the parts Python doesn’t have: par, contracts and world.