Reference

Design and architecture

Brine is built on one promise: every rule the language states is enforced, either by a proof at compile time or by a runtime check that can never be turned off. The rest follows from that and from five other goals: native speed, parallelism in the syntax, usability for people and coding agents alike, first-class support on every major OS, and a small language. This page explains those choices and how the compiler and runtime implement them. It is adapted from docs/DESIGN.md in the Brine repository, the source of truth for why Brine is the way it is.

Philosophy

Rules cannot be broken. Every rule is enforced by a static proof or by a runtime check that can never be turned off: not in release builds, not with a flag. There is no unsafe, no -DNDEBUG, no --unchecked. The compiler’s job is to prove checks away; the programmer can’t switch them off.
Fast. Compiled ahead of time to native code. No garbage collector, no VM, no interpreter. Value semantics with copy-on-write keep the language simple without giving up performance.
Natively parallel. Parallelism is syntax, not a library: par for, par [..], par sum(..), par(a, b). Running as many processes on many machines (MPI-style) is the built-in world module. Data races and distributed deadlocks are compile errors.
Usable by humans and agents. Python-like syntax and one obvious way to write things. Every diagnostic has a stable code, a precise span, an explanation and, where possible, a machine-applicable fix. Every command has --json output. brine explain <code> and brine guide are built in.
Cross-platform. macOS, Linux and Windows are first-class. Code goes through brine’s own IR to native x86-64 and AArch64 backends (fast dev builds on Windows and Linux) or to portable C11 for whatever C compiler is present (optimized builds, and every other platform).
Clean and easy to understand. A small language surface. No hidden control flow, no implicit conversions, no aliasing surprises.

The language at a glance

struct Particle:
    pos: float
    vel: float

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

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

fn main():
    let n = 1_000_000
    let xs = par [float(i) * 0.5 for i in 0..n]      # 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:                                # race-free parallel loop
        out[i] = xs[i] + 1.0
    var p = Particle(pos=0.0, vel=2.0)
    p.step(0.5)
    print(f"total = {total:.3f}, clamp = {clamp(15, 0, 10)}, pos = {p.pos}")

total = 83333208333375008.000, clamp = 10, pos = 1.0

Core rules

Area	Rule
Bindings	`let` is immutable, `var` is mutable. No shadowing inside a function.
Types	Static, inferred for locals, explicit on function signatures. No implicit numeric conversion (literals adapt to context).
Integers	`int` is 64-bit signed; `i8`..`i128`, `u8`..`u128`. Overflow traps (checked arithmetic). Narrowing conversions are checked. 128-bit types need a 64-bit target, and their overflow checks are never proved away (the prover’s own arithmetic is 128-bit).
Floats	`float` is f64; `f32`. IEEE semantics.
Values	Everything has value semantics: `let b = a` copies, and arguments are passed by value. Arrays and strings are copy-on-write and reference counted, so copies are O(1) until one is changed.
References	Explicit at both ends: `fn fill(ref xs: [int])` is called as `fill(ref xs)`; methods that change their receiver take `ref self`. `let r = ref x` makes `r` a second name for `x`. References are second-class: they can’t be stored in structs or arrays or returned, so they never dangle, and the compiler always knows what they point to. A `ref` argument can’t alias another argument. `mut x: T` on a parameter is a local copy the function may change.
Maps	`{K: V}` hash maps that remember insertion order. Values, like arrays (copy-on-write). Reading a missing key panics; `m.get(k)` returns `Option[V]`. Keys need a total `==` (no floats). `par` bodies may read maps but not change them.
Strings	Immutable UTF-8. `len`, `s[i]` and slices count bytes (`s[i]` is a one-character `str`); `for c in s` walks characters. Case conversion and character classes follow Unicode (`is_digit` is `0`-`9`).
Slices	`xs[a:b]` and `s[a:b]` copy; out-of-range bounds panic (or are proven in range). No negative indexes.
Evaluation order	A statement that changes a variable (a mutating method, a `ref` argument) can’t read that variable anywhere else, so the order arguments are evaluated in can never change the result.
I/O	`read_file`, `write_file`, `file_exists`, `getenv` and `run` return `Result`, `Option` or `bool`: failures are values, never crashes. Effects that depend on order (`write_file`, `run`) aren’t allowed in `par` bodies.
Enums	Tagged unions with named fields per variant; values are immutable and may be recursive. `match` must be exhaustive (checked at compile time, with an example of a missed value).
Memory	Deterministic: atomic reference counting, freed at scope exit. No GC pauses.
Generics	`fn f[T](x: T)`, `struct Pair[A, B]`, `enum Option[T]`. Monomorphized: every use with new type arguments is a specialized copy, checked and proven like ordinary code. Type arguments are inferred from arguments and the expected type.
Errors	`Result[T, E]` and `Option[T]` for expected failures; runtime traps with a source location (`panic`) for bugs. `x?` returns a `None` or `Err` to the caller (no implicit error conversions). `main` may return `Result[(), E]`.

Each rule exists to make one of the goals possible. Value semantics and second-class references mean values never alias, which is what lets the par rules be simple and lets the prover reason about a variable without tracking pointers. The evaluation-order rule removes the one place where C-like languages leave the result up to the compiler. And because overflow traps, the prover can treat integers as mathematical integers.

Proofs

There are two kinds of obligations:

Explicit ones are written by the programmer and must be proven at compile time, or the program doesn’t compile: requires (proven at every call site), ensures (proven at every return; result names the return value), invariant (proven on loop entry and preserved by every iteration) and prove e (an inline claim).
Implicit ones come from the language’s safety rules: array bounds, division by zero, integer overflow, narrowing conversions, pop() on an empty array. They are proven when possible and otherwise checked at runtime, and the check can never be disabled. brine check --report lists every check that remains, so you can add the facts that remove them.

assert e bridges the two: a runtime check (always on) that becomes a known fact for the prover afterwards. When a precondition can’t be proven, the compiler suggests an assert (check at runtime) or a requires (push the obligation up to the callers).

The prover is a built-in decision procedure for linear integer arithmetic with booleans: symbolic execution plus Fourier–Motzkin elimination with integer tightening. It is sound (it never accepts a false claim) but incomplete (it may fail to prove a true claim; then you add an invariant, requires or assert). See Contracts and Runtime checks.

Parallelism

Construct	Meaning
`par for i in lo..hi:`	data-parallel loop over a thread pool
`par [e for i in lo..hi]`	parallel map
`par sum(e for i in lo..hi)`	parallel reduction (`sum`, `product`, `min`, `max`, `any`, `all`)
`par(f(a), g(b))`	fork-join of independent expressions; returns a tuple

Race freedom is a compile-time rule. Inside a par body, variables from the enclosing scope are read-only, with one exception: an outer array may be written only at the loop index (out[i] = ...), and then not accessed at any other index in the body. Function calls can’t receive outer variables as ref. Since values have no observable aliasing, this is enough for data-race freedom.

Reductions are deterministic. They combine in one fixed order that depends only on the number of elements, never on the number of threads: leaves of 16 consecutive elements, each folded left to right, then a balanced binary tree over the leaves. A float par sum gives the same bits on a laptop, a 128-core server and a GPU, and the tree loses less precision than a left-to-right sum.

GPUs run eligible constructs with no annotation and no change in meaning: the kernels follow the CPU’s floating-point rules exactly, and a check that fails on the device reruns the construct on the CPU, which panics as usual. The compiler decides what can run on a GPU; the runtime decides, per launch, whether it should.

Many processes. The world module gives every program MPI-style ranks and collectives. Every operation is collective (there is no unmatched send or recv), and the compiler checks that every rank makes the same calls in the same order by classifying each value as uniform (the same on every rank) or varying; a communication under a varying condition is E0510. So a brine program can’t deadlock waiting for a message that never comes.

See Parallelism, Race freedom and GPUs.

Compiler pipeline

source ─► lexer (indentation-aware) ─► parser ─► AST
      ─► checker (names, types, mutability, race freedom)
      ─► uniform (deadlock freedom for `world`)
      ─► verifier (symbolic execution + solver; proves contracts, removes runtime checks)
      ─► lowering to brine IR (lower.br)
      ─► x86-64 machine code (x64.br, COFF/ELF objects)    dev and debug builds on x86-64 Windows/Linux
       └► AArch64 machine code (a64.br, ELF objects)        dev and debug builds on AArch64 Linux
       └► C11 (ir_c.br) ─► system C compiler               --release, and every other platform
      ─► link with the brine runtime ─► native executable

Stage	Source	Does
lexer	`compiler/lexer.br`	tokens, with indentation turned into block structure
parser	`compiler/parser.br`	the syntax tree; syntax errors (`E01xx`)
checker	`compiler/check.br`, `types.br`	names, types, generics, mutability, references, `par` rules (`E02xx`-`E05xx`)
uniform	`compiler/uniform.br`	deadlock freedom for `world` (E0510, E0511)
verifier	`compiler/verify.br`, `solver.br`	proves contracts (`E06xx`) and removes the runtime checks it can prove unnecessary
lowering	`compiler/lower.br`	the brine IR, with the remaining checks and reference counting made explicit
backends	`x64.br`, `a64.br`, `ir_c.br`, `ptx.br`, `msl.br`	machine code, C, GPU kernels
objects and debug info	`obj.br`, `dwarf.br`	COFF and ELF objects, DWARF
driver	`driver.br`, `main.br`	the pipeline, caching, the C toolchain, the CLI

The compiler uses par itself: imported modules are parsed a wave of imports at a time, in parallel, and the prover takes every function on its own. Results are combined in a fixed order, so the output never depends on the thread count.

Backends

The brine IR (compiler/ir.br) sits between the verifier and code generation: virtual registers with machine kinds (i8..u128, f32, f64, ptr, bool), explicit control flow, explicit checks (only those the prover couldn’t remove), explicit reference counting, stack slots, and data with relocations. Every backend reads it:

x86-64 (x64.br, objects by obj.br) writes machine code and a COFF (Windows) or ELF (Linux) object directly, in well under a second for the whole compiler. It’s the default for dev and debug builds there; debug builds add DWARF and skip the optimizations.
AArch64 (a64.br) is the same design for 64-bit ARM Linux, with .eh_frame unwind info and the same DWARF.
C (ir_c.br) writes one statement per IR instruction. gcc and clang at -O2/-O3 make it as fast as hand-written C, so it serves --release and every platform without a native backend. It’s also the bootstrap seed.
PTX (ptx.br) and Metal (msl.br) turn each par construct that can run on a GPU into a kernel, next to the CPU code. ptx.br also decides which constructs are eligible, for both.

Three rules keep the backends interchangeable:

Nothing above the IR may depend on a backend: no C-only semantics leak into the checker or the verifier.
The runtime ABI (value layouts, reference counting, panics, the brine_x_* entry points for helpers that are static inline in C) is fixed, so native code and the C runtime link together.
Every backend passes the same end-to-end test suite, and the compiler built by each one builds itself to the same object.

A native backend’s main wins are compile speed, independence from a C toolchain, and what C can’t express well (guaranteed tail calls, exact overflow handling, SIMD, debug info). Running faster than C comes mostly from what brine knows that C doesn’t (no aliasing, proven-away checks, race-free par), and the IR is where those facts are kept for every backend. See Builds, backends and performance.

Runtime

The runtime (runtime/brine_rt.h and runtime/brine_rt.c) is C, embedded in the compiler binary, and compiled once per runtime version and cached. It has Win32 and POSIX code paths and provides:

reference-counted, copy-on-write strings, arrays and maps, with a small-block allocator;
checked arithmetic and the panic path (every panic goes through brine_panic_at with a source location);
the thread pool and the deterministic reductions;
GPU offload: loading the CUDA driver or the Metal framework at run time, timing each construct, and choosing CPU or GPU per launch;
the world transport: full-mesh TCP with a background receiver per peer, so sends never block;
files, processes and the os module.

Memory model

Every value is reference counted with atomic counts, and generated code releases every temporary and local at scope exit, so memory is freed at a predictable point and there are no collector pauses. A value with a single reference is freed without an atomic instruction. Values can’t form reference cycles (references are second-class, assignment copies, and enum values are immutable), so reference counting needs no cycle collector. BRINE_LEAKCHECK=1 prints the number of live strings and arrays at exit; brine’s test suite requires 0.

Copy-on-write makes value semantics cheap: let b = a shares the array until one of them is changed, and a change to an array with a single reference happens in place.

Debugging and caching

Debugging: native debug builds carry DWARF with lines, brine function names (Point.norm) and every local and parameter by its brine name and type. Debug code keeps each value in its stack slot, so print in the debugger is always right. brine debug loads runtime/brine_gdb.py, which prints values the way brine does. Elsewhere, and with BRINE_BACKEND=c, debug builds go through C with #line directives. See Debugging.
Caching: objects are named by a hash of what they’re made from. C output is split into one translation unit per core (by a hash of each function’s name, each unit declaring only what it uses), compiled in parallel, so an edit recompiles only the units it touches. An unchanged program skips the link (the .brine-hash stamp).
Timing: BRINE_TIMES=1 prints the time of each phase; BRINE_TIMES=2 also names the functions the prover is slow on.

Made for agents

Stable error codes; every error has a primary span, a “why” and a “how to fix”.
Machine-applicable fixes in JSON: fixes: [{line, column, end_line, end_column, replacement}].
Deterministic output: the same input gives the same diagnostics in the same order.
No configuration for anything common. brine guide and an AGENTS.md in every new project.
Syntax chosen to match what models already know (Python), minus the footguns.

Self-hosting

The compiler was first written in Rust, then ported to brine module by module, with every stage cross-checked against the Rust compiler: identical diagnostics, prover reports and generated C on every file, plus mutation fuzzing. The brine compiler builds itself to a fixed point, and the Rust compiler has been retired.

Its own generated C, bootstrap/brinec.c, is the seed that builds it from scratch with only a C compiler. Each release refreshes the seed, and CI builds brine from it on every platform, so the chain from a plain C compiler to the current brine is always tested.

Decisions

Questions the design has settled, and why. Open questions are marked [DECISION] in docs/DESIGN.md until they are answered.

Question	Answer
Should explicit claims the prover can’t decide fall back to runtime checks in a “development” mode?	No. That would be a rule that can be broken. Use `assert` explicitly instead.
How are distributed deadlocks handled?	Ruled out at compile time. Every `world` operation is collective, and the uniformity check makes every rank reach the same calls in the same order. A rank that crashes makes the others stop with an error instead of hanging.
Should `par` reductions match a sequential loop’s result?	No: they match each other. A fixed tree order gives the same bits for any thread count and on the GPU, and is usually more accurate. Programs that need a left-to-right order sum sequentially.