# Design and architecture > Why Brine is the way it is (its principles and core rules) and how the compiler, its backends and the runtime are built. Source: https://docs.brinelang.org/reference/design/ 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 [Section titled “Philosophy”](#philosophy) 1. **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. 2. **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. 3. **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. 4. **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 ` and `brine guide` are built in. 5. **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). 6. **Clean and easy to understand.** A small language surface. No hidden control flow, no implicit conversions, no aliasing surprises. ## The language at a glance [Section titled “The language at a glance”](#the-language-at-a-glance) glance.br ```brine 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}") ``` Output ```text total = 83333208333375008.000, clamp = 10, pos = 1.0 ``` ## Core rules [Section titled “Core rules”](#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 [Section titled “Proofs”](#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](/proofs/contracts/) and [Runtime checks](/proofs/runtime-checks/). ## Parallelism [Section titled “Parallelism”](#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](/reference/errors/#e0510). So a brine program can’t deadlock waiting for a message that never comes. See [Parallelism](/parallelism/overview/), [Race freedom](/parallelism/race-freedom/) and [GPUs](/parallelism/gpu/). ## Compiler pipeline [Section titled “Compiler pipeline”](#compiler-pipeline) ```text 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 [Section titled “Backends”](#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](/tooling/builds-and-backends/). ## Runtime [Section titled “Runtime”](#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 [Section titled “Memory model”](#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 [Section titled “Debugging and caching”](#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](/tooling/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 [Section titled “Made for agents”](#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 [Section titled “Self-hosting”](#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 [Section titled “Decisions”](#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. | ## Related [Section titled “Related”](#related) * [Roadmap](/reference/roadmap/) * [Builds, backends and performance](/tooling/builds-and-backends/) * [Platforms](/reference/platforms/) * [Quick reference](/reference/quick-reference/)