AGENTS.md and common mistakes

Every project made by brine new or brine init has an AGENTS.md that tells coding agents how to work in it: the commands to run, and the rules that most often trip up a model, or a person, who knows Python. This page shows the file, then takes each rule in turn with code that breaks it, what the compiler says, and the fix.

The file

This is the AGENTS.md that brine new hello writes (Brine 0.4.0):

AGENTS.md

# AGENTS.md — working on `hello`

This is a brine project. brine is a compiled,
verified, natively parallel language with Python-like syntax.

## Commands
- `brine check` — type-check and verify (fast; run after every edit)
- `brine run` — build and run `src/main.br`
- `brine test` — run all `test "...":` blocks
- `brine fmt` — format all sources (always run before committing)
- `brine guide` — the full language reference (read it once)
- `brine explain <CODE>` — explanation of any error code, e.g. `brine explain E0601`

Add `--json` to any command for machine-readable output (one JSON object per line).

## Rules that commonly trip people up
- `let` is immutable, `var` is mutable; no shadowing.
- No implicit numeric conversions: write `float(i)`, `int(x)`.
- Arguments are passed by value. A function that changes the caller's variable
  declares `ref x: T` and callers write `f(ref x)`; methods use `ref self`.
- `requires`/`ensures`/`invariant`/`prove` must be proven at compile time.
  If the prover can't, the error lists the known facts; add an `invariant`,
  a `requires`, or an `assert` (runtime check that becomes a known fact).
- Inside `par for i in ...:` you may only write `out[i]` of outer arrays.
- Maps: `m[k]` panics if `k` is missing; test with `k in m` or use `m.get(k)`.
- No negative indexes (`xs[-1]` is an error); write `xs[len(xs) - 1]`.
- Strings index and slice by bytes; `s[i]` is a one-character `str`.
- One expression can't change a variable and also read it, or change it twice
  (`print(xs.pop(), xs)`, `xs.push(xs.pop())`); split it into two statements.
  Uses on different sides of `and`/`or`/`if-else` are fine.
- Types are optional (`let x = 5` or `let x: int = 5`); if brine.toml has
  `typed = true` under `[check]`, every `let`/`var`/`for` variable needs one.
- `match` must cover every case; read enum variant data with `match`, not `.field`.
- Expected failures return `Result[T, E]` (`Ok(x)` / `Err(e)`) or `Option[T]`
  (`Some(x)` / `None`); `panic` is for bugs. `x?` passes a failure up to the caller.

The file is yours to edit: add your project’s own conventions below the generated part. brine init doesn’t overwrite an existing AGENTS.md.

let is immutable, var is mutable

let declares a name that never changes; var declares one that can. Each name is declared once per function, so there’s no shadowing either.

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

Fix: declare it with var.

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

Declaring the same name again is E0207; pick a new name, or make the first one a var and assign to it. See Bindings.

No implicit numeric conversions

int and float (and i32, u8, …) never convert on their own, not even in arithmetic or comparisons.

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

Fix: convert explicitly. int(x) truncates toward zero, and conversions to smaller types such as i32(n) are checked.

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]))

See Values and types.

Arguments are passed by value; ref changes the caller’s variable

Arguments are copies, and parameters are read-only. A function that changes the caller’s variable declares a ref parameter, and the caller writes ref too, so the change is visible where it happens.

fn add_one(ref xs: [int]):
    xs.push(1)

fn main():
    var xs: [int] = []
    add_one(xs)
    print(xs)

error[E0402]: parameter `xs` is a `ref`; pass the argument with `ref`
 --> refex.br:6:13
  |
6 |     add_one(xs)
  |             ^^ the callee may modify this
  |
  = help: passing by reference is always visible at the call site in brine
  = run `brine explain E0402` for more about this error
error: could not compile due to 1 error

Fix: add_one(ref xs).

fn add_one(ref xs: [int]):
    xs.push(1)

fn main():
    var xs: [int] = []
    add_one(ref xs)
    print(xs)

Methods work the same way. A method that changes its struct takes ref self; with plain self, the receiver is read-only:

struct Counter:
    n: int

    fn bump(self):
        self.n += 1

fn main():
    var c = Counter(n=0)
    c.bump()
    print(c.n)

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

Fix: fn bump(ref self):. The call stays c.bump().

struct Counter:
    n: int

    fn bump(ref self):
        self.n += 1

fn main():
    var c = Counter(n=0)
    c.bump()
    print(c.n)

To change a local copy without touching the caller’s value, declare the parameter mut x: T. See Functions.

Contracts must be proven at compile time

requires, ensures, invariant and prove are not runtime checks. The compiler must prove them, or the program doesn’t compile. Here first_or_last calls last without knowing that xs is non-empty:

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

fn first_or_last(xs: [int]) -> int:
    return last(xs)

fn main():
    print(first_or_last([1, 2, 3]))

error[E0601]: cannot prove the precondition of `last`
 --> lastreq.br:6:12
  |
6 |     return last(xs)
  |            ^^^^^^^^ this call might violate `requires len(xs) >= 1`
2 |     requires len(xs) >= 1
  |              ------------ precondition declared here
  |
  = note: nothing is known here about the values involved
  = note: to prove: len(xs) > 0
  = 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

The notes list what the prover knew (“nothing”) and what it needed. There are three fixes. Pass the obligation to the callers with a requires:

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

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

fn main():
    print(first_or_last([1, 2, 3]))

Or check it at runtime with an assert, which the prover then knows is true:

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

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

fn main():
    print(first_or_last([1, 2, 3]))

Or handle the case where it’s false:

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

fn last_or(xs: [int], default: int) -> int:
    if len(xs) == 0:
        return default
    return last(xs)

fn main():
    print(last_or([1, 2, 3], 0), last_or([], 0))

For loops, the missing fact is usually an invariant. Don’t weaken or delete the contract to make the error go away. See Contracts and Fixing proof failures.

par for may only write out[i]

Inside a par body, variables from outside are read-only. The one exception: par for i in ... may write element i of an outer array, exactly the loop variable. Any other write could race with another iteration.

fn main():
    let n = 8
    var out = [0] * n
    par for i in 0..n - 1:
        out[i + 1] = i
    print(out)

error[E0501]: cannot assign to `out` inside a `par` body
 --> parwrite.br:5:9
  |
5 |         out[i + 1] = i
  |         ^^^^^^^^^^ would be a data race
  |
  = note: `out` is shared by all parallel iterations
  = help: a `par for` may only write `out[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

Fix: index the write with the loop variable and shift the read instead, or build the array with par [...]. To add values up, use a reduction such as par sum(...).

fn main():
    let n = 8
    var out = [0] * n
    par for i in 1..n:
        out[i] = i - 1
    let same = par [0 if i == 0 else i - 1 for i in 0..n]
    print(out, out == same)

See Race freedom.

m[k] panics if k is missing

Reading a missing key stops the program. This compiles, then panics when it runs:

fn main():
    var counts = {"a": 1}
    for w in ["a", "b", "a"]:
        counts[w] += 1
    print(counts)

Output

panic: key "b" is not in the map
  --> mapmiss.br:4:9

Fix: test with in, or read with get, which returns an Option (or a default when you pass one).

fn main():
    var counts: {str: int} = {}
    for w in ["a", "b", "a"]:
        if w in counts:
            counts[w] += 1
        else:
            counts[w] = 1
    print(counts, counts.get("z", 0))

Output

{"a": 2, "b": 1} 0

See Maps.

No negative indexes

xs[-1] isn’t the last element. It’s out of bounds, and the program stops when it gets there:

fn main():
    let xs = [10, 20, 30]
    print(xs[-1])

Output

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

This is a runtime panic, not a compile error, so brine check won’t flag it. Fix: count from the end with len.

fn main():
    let xs = [10, 20, 30]
    print(xs[len(xs) - 1], xs[len(xs) - 2:])

See Arrays.

Strings index and slice by bytes

len(s), s[i] and s[a:b] count bytes of UTF-8. For ASCII text that’s the same as characters; for other text it isn’t:

fn main():
    let s = "héllo"
    print(len(s), len(s.chars()), s[0], s[1:3])
    let at = s.find("l").unwrap()
    print(at, s[at:])

Output

6 5 h é
3 llo

é is two bytes, so the first l is at byte 3. Use positions from find rather than counting characters, and walk characters with for c in s or s.chars(). See Strings.

One expression can’t change a variable and read it

An expression that changes a variable (a mutating method such as pop, or a ref argument) can’t also read it or change it again elsewhere. Then the order in which arguments are evaluated can never change the result.

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

error[E0405]: `xs` is changed twice in the same expression
 --> pushpop.br:3:13
  |
3 |     xs.push(xs.pop())
  |             ^^^^^^^^ changed here
  |     ----------------- and changed here
  |
  = help: make one change in its own statement first, e.g. `let v = ...`, then use `v`
  = run `brine explain E0405` for more about this error
error: could not compile due to 1 error

Fix: split it into two statements.

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

print(xs.pop(), xs) is the same error (“changed and also read”). Uses on different sides of and, or or if/else are fine, because only one side runs first.

Types are optional, unless the project says otherwise

let x = 5 and let x: int = 5 are both fine. A project can require a written type on every variable with this in brine.toml:

brine.toml

[check]
typed = true

brine check --typed does the same for one run. This program compiles normally:

fn main():
    let x = 5
    var total: int = 0
    for i in 0..x:
        total += i
    print(total)

With --typed, each variable without a type is an error, with the type to add:

brine check --typed typed.br

error[E0337]: `x` has no written type
 --> typed.br:2:9
  |
2 |     let x = 5
  |         ^ add `: int`
  |
  = note: this project asks for a type on every variable (`typed = true` in brine.toml, or `--typed`)
  = run `brine explain E0337` for more about this error
error[E0337]: `i` has no written type
 --> typed.br:4:9
  |
4 |     for i in 0..x:
  |         ^ add `: int`
  |
  = note: this project asks for a type on every variable (`typed = true` in brine.toml, or `--typed`)
  = run `brine explain E0337` for more about this error
error: could not compile due to 2 errors

Fix: let x: int = 5 and for i: int in 0..x:. In --json output, each E0337 carries a fix that inserts the type. See Projects.

match must cover every case

A match has to handle every possible value. The error names a value it misses:

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

Fix: add the case, or end with case _:.

Read enum data with match, not .field

The fields of an enum variant aren’t readable with ., because the value might be a different variant:

enum Shape:
    Circle(radius: float)
    Square(side: float)

fn main():
    let s = Shape.Circle(radius=1.0)
    print(s.radius)

error[E0205]: enum `Shape` has no fields
 --> field.br:7:13
  |
7 |     print(s.radius)
  |             ^^^^^^ use `match` to read the data in a variant
  = run `brine explain E0205` for more about this error
error: could not compile due to 1 error

Fix: match on the variant and bind its fields.

enum Shape:
    Circle(radius: float)
    Square(side: float)

fn main():
    let s = Shape.Circle(radius=1.0)
    match s:
        case Shape.Circle(r):
            print(r)
        case Shape.Square(side):
            print(side)

See Enums and match.

Failures are Result and Option, not exceptions

Brine has no exceptions. An expected failure is a Result[T, E] or an Option[T]; panic is for bugs. x? returns a failure to the caller, so the function using it must return a matching Result or Option:

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 main():
    let b = parse_bit("1")?
    print(b)

error[E0341]: `?` needs the function to return Result[..., str]
 --> qmark.br:9:13
  |
9 |     let b = parse_bit("1")?
  |             ^^^^^^^^^^^^^^^ this returns from a function that returns `()`
  |
  = help: change the return type to `Result[..., str]`, or handle the value with `match`
  = run `brine explain E0341` for more about this error
error: could not compile due to 1 error

Fix: handle it with match, or make the function return a Result. main may return Result[(), E]; an Err prints error: ... and exits with status 1.

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 main() -> Result[(), str]:
    let b = parse_bit("1")?
    print(b)
    match parse_bit("7"):
        case Ok(v):
            print(v)
        case Err(e):
            print("bad input:", e)
    return Ok(())

See Error handling.

Related

• Using Brine with coding agents
• Coming from Python: more differences, with their errors
• Error codes