NewBrine compiles to WebAssembly: try it live in your browser
New in 0.4.0: GPU offload with no annotations

Fast, parallel
and proven.

Brine is a compiled systems language with Python-like syntax. The compiler proves your rules before the program runs, turns data races and deadlocks into compile errors, and runs par code on every core or the GPU, with the same result bits on any machine.

More options
curl -fsSL https://raw.githubusercontent.com/brinelang/brine/main/install.sh | sh
search.brBrine 0.4.0
fn index_of(xs: [int], target: int) -> int:
    ensures -1 <= result < len(xs)proven
    var lo = 0
    var hi = len(xs)
    while lo < hi:
        invariant 0 <= lo <= hi <= len(xs)proven
        let mid = lo + (hi - lo) / 2
        if xs[mid] == target:bounds check removed
            return mid
        if xs[mid] < target:
            lo = mid + 1
        else:
            hi = mid
    return -1

fn main():
    let squares = par [i * i for i in 0..1_000_000]every core
    let total = par sum(float(x) for x in squares)same bits anywhere
    print(index_of(squares, 144), total)
$ brine run search.br --release
     Built search [release] in 0.19s
12 3.333328333335e+17
  • 21.8×faster on 32 threads than on 1one par sum, no other changes
  • 9×faster on the GPU, picked automaticallyf32 n-body step, RTX 4090
  • 1.00×the run time of C on mandelbrotbrine --release vs gcc -O2
  • 0data races that compilea race is error E0501

Runs on Linux (x86-64 and ARM64), macOS (Apple silicon and Intel) and Windows x86-64. Offloads to NVIDIA GPUs through CUDA and Apple GPUs through Metal.

Run it here,
in your browser.

These are real Brine programs, compiled with brine build --target wasm and running on this page. In a browser WebAssembly gets one thread, so par runs in order, with the same results it gives on 32 cores.

mandelbrot.wasmwaiting
Click to zoom in, shift-click to zoom out

args …

mandelbrot.br--release --target wasm
# Draws the Mandelbrot set. The page passes the view as arguments:
#   center x, center y, width of the view, pixels across, pixels down, max steps

fn escape(cx: float, cy: float, limit: int) -> int:
    # 0 inside the set; outside, a smooth escape time (x16)
    var x = 0.0
    var y = 0.0
    var i = 0
    while i < limit:
        let x2 = x * x
        let y2 = y * y
        if x2 + y2 > 256.0:
            let nu = log(log(x2 + y2) / 2.0 / log(2.0)) / log(2.0)
            return max(1, int((float(i) + 1.0 - nu) * 16.0))
        y = 2.0 * x * y + cy
        x = x2 - y2 + cx
        i += 1
    return 0

fn main():
    let a = args()
    let (cx, cy, span) = (float(a[0]), float(a[1]), float(a[2]))
    let (w, h, limit) = (int(a[3]), int(a[4]), int(a[5]))
    let step = span / float(w)
    let (left, top) = (cx - span / 2.0, cy - step * float(h) / 2.0)
    var rows = [""] * h
    par for y in 0..h:                    # each row is independent
        let ci = top + float(y) * step
        let row = [escape(left + float(x) * step, ci, limit) for x in 0..w]
        rows[y] = " ".join([str(v) for v in row])
    print("\n".join(rows))

Each program is about 420 KB of WebAssembly, loaded when you get here and run in a Web Worker by Brine's 6 KB loader. Build your own

Parallelism is syntax, not a library.

Four constructs cover loops, maps, reductions and fork-join. There are no threads to manage, no locks, and no annotations: put par in front and Brine uses every core. Inside a par body the compiler only allows what can't race.

A data-parallel loop over a thread pool. Each iteration may write only its own element of an outer array.

var out = [0.0] * n
par for i in 0..n:
    out[i] = sqrt(xs[i]) * 2.0
How par works
par sum(float(collatz_len(i)) for i in 1..=20_000_000)
1 thread2.763 s
32 threads0.127 s
21.8× fastersame result on both: 3249531153.0
Measured on a 16-core Ryzen 9 9950X3D. Animation durations are to scale.

Same bits on
every machine.

A float sum depends on the order you add things up. Most parallel runtimes let that order depend on the thread count, so the answer changes from laptop to server. Brine fixes the order: leaves of 16 elements, then a balanced tree. It depends only on how many elements there are, so par sum gives the same result on 1 thread, 32 threads or a GPU.

The tree is also more accurate. For this sum, its error is 6.4e-15; a plain left-to-right loop is off by 5.4e-13, about 84 times more.

How reductions work
Who adds which leaf
0163248648096112128144160176192208224240
Each box is 16 consecutive elements, folded left to right. Threads change the colors, never the tree.
Results of the same par sum on different hardware
Ran onTimeResult
1 thread147.6 ms19.69104359191385001✓
2 threads75.0 ms19.69104359191385001✓
8 threads19.3 ms19.69104359191385001✓
32 threads10.5 ms19.69104359191385001✓
RTX 409012.1 ms19.69104359191385001✓

par sum(1.0 / float(i) for i in 1..=200_000_000). A sequential loop gives 19.69104359191437936

The GPU, with
no code changes.

The same par code runs on an NVIDIA GPU through CUDA or an Apple GPU through Metal when that's faster. Nothing to annotate, no kernels to write, nothing to install but the driver. Without a GPU, programs run on the CPU as before.

  1. The compiler decides what can run there

    Bodies built from numeric code, loops, branches, structs, array reads and out[i] writes become CUDA (PTX) or Metal kernels, shipped inside your binary.

    int & float mathloops & branchesstructs & tuplessqrt, abs, min, maxstrings & mapsprintingsin, exp, log
  2. The runtime decides when it pays

    It times the construct on the CPU, estimates the GPU including copies and launches, and moves it only when that is at least 25% faster. Small or memory-bound work stays on the CPU.

  3. The results don't change

    Kernels follow the CPU’s float rules exactly: no fused multiply-adds, exactly rounded / and sqrt, the same reduction tree. If a check fails on the device, the construct reruns on the CPU and panics as usual.

f32 n-body step: 16,384 bodies, 268M interactions
$ BRINE_GPU_LOG=1 brine run nbody.br --release
brine gpu: nbody.br:23:12 par map n=16384 -> cpu 33.164 ms (starting the GPU)
brine gpu: NVIDIA GeForce RTX 4090 ready in 185 ms
brine gpu: nbody.br:23:12 par map n=16384 -> gpu 4.381 ms (kernel 3.591 ms, copies 0.741 ms, 0.5 MB; cpu estimate 33.197 ms)
brine gpu: nbody.br:23:12 par map n=16384 -> gpu 3.653 ms (kernel 3.564 ms, copies 0.075 ms, 0.5 MB; cpu estimate 33.197 ms)
32 CPU threads
33.2 ms
RTX 4090
3.65 ms

9× faster, chosen by the runtime

The first runs stay on the CPU while the GPU starts in the background. The f64 version of the same step stays on the CPU, because it isn't faster on this card: auto measures instead of guessing. GPU offload in the docs

Many processes.
No deadlocks.

Every Brine program can run as many cooperating processes, on one machine or many, with MPI-style collectives in the built-in world module. Every call is collective, and the compiler checks that all ranks make the same calls in the same order. A program that could hang doesn't compile.

  • rank()
  • size()
  • barrier()
  • broadcast(root, v)
  • sum(v)
  • min(v)
  • max(v)
  • gather_all(v)
  • shift(v, by)
  • exchange(xs)
The world module
world.br
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)all-gather
    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]

The bugs that hurt most
don't compile.

Races, distributed deadlocks and broken contracts are compile errors, not 3 a.m. pages. Every error has a stable code, the exact span, the reason, and how to fix it.

race.brTwo threads writing one variable
fn main():
    let xs = [1, 2, 3, 4]
    var total = 0
    par for i in 0..len(xs):
        total += xs[i]
    print(total)
$ brine check race.br
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
FixUse a reduction: let total = par sum(x for x in xs) brine explain E0501
clamp.br
fn clamp(x: int, lo: int, hi: int) -> int:
    requires lo <= hievery caller must prove this
    ensures lo <= result <= hiproven for every return
    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: check removed

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

test "clamp stays in range":tests live in the language
    assert clamp(15, 0, 10) == 10
    assert clamp(-5, 0, 10) == 0
$ brine check clamp.br --report
   Checked clamp in 0.00s — 2 runtime checks proven unnecessary, 0 remain
$ brine test clamp.br
test clamp stays in range ... ok

test result: ok. 1 passed; 0 failed; finished in 0.01s

Rules that
can't be broken.

Write what must be true with requires, ensures andinvariant. A prover built into the compiler checks every one at compile time, and uses what it learns to delete runtime checks it no longer needs. Safety you don't pay for at run time.

No unsafe
There is no escape hatch. Every rule holds in every program.
No off switch
No --unchecked, no -DNDEBUG. Release builds keep every check the prover could not remove.
Checks or proofs
Overflow, bad indexes and division by zero stop with a clear message, unless proven impossible. Then the check is gone.
Sound
The prover never accepts a false claim. When it can’t prove something, it lists the facts it knew.
Proofs in Brine

Reads like Python.
Runs like C.

A small language with one obvious way to write things, and none of the footguns.

shapes.br
enum Shape:
    Circle(radius: float)
    Square(side: float)
    Dot

    fn area(self) -> float:
        match self:must cover every case
            case Shape.Circle(r):
                return 3.14159 * r * r
            case Shape.Square(s):
                return s * s
            case Shape.Dot:
                return 0.0

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 shapes = [
        Shape.Circle(radius=1.0),
        Shape.Square(side=2.0),
        Shape.Dot,
    ]
    let total = sum(s.area() for s in shapes)
    print(f"total area: {total:.2f}")
    print(parse_bit("1")?)? passes an Err up
    return Ok(())
  • Python-like syntax

    Indentation, comprehensions, f-strings, slices. Models and people already know it.

  • Static types, inferred

    Types on signatures, inferred for locals. Generics are specialized, so they cost nothing.

  • Structs, enums, match

    Tagged unions with exhaustive match that shows you a value you missed.

  • Errors are values

    Option and Result with ?. Files and processes fail with values, never crashes.

  • Values, not pointers

    let b = a copies, cheaply, with copy-on-write. Explicit ref when you want to share.

  • Native, no GC

    Ahead-of-time compiled. Memory is freed deterministically at scope exit. No VM, no pauses.

What Brine leaves out
  • unsafe
  • null
  • exceptions
  • garbage collector
  • implicit conversions
  • data races
  • deadlocks
  • a flag to turn checks off
Take the tour

As fast as C,
before you add par.

--release builds go through Brine's own IR and an optimizing C compiler, and keep every safety check the prover couldn't remove. On single-threaded benchmarks, Brine runs within a few percent of hand-written C, sometimes faster. Then par uses the rest of your cores.

Run time relative to C (gcc -O2) brine --release C = 1.0×Lower is faster

Ryzen 9 9950X3D, Windows 11, gcc 16.2, best of 3 runs. The programs are single-threaded ports of the classic benchmarks. Brine is slower on wordfreq, where string and map handling still has work to do. Reproduce: brine run bench/compare.br

Show the numbers
BenchmarkC -O2brine --releaseBrine dev build
binarytrees1.334 s0.738 s (0.55×)0.89×
fannkuch1.664 s1.514 s (0.91×)1.22×
mandelbrot0.579 s0.577 s (1.00×)1.30×
nbody0.717 s0.723 s (1.01×)3.42×
spectral0.270 s0.274 s (1.02×)2.03×
sieve0.246 s0.284 s (1.15×)1.44×
matmul0.063 s0.074 s (1.16×)6.28×
wordfreq0.023 s0.089 s (3.91×)5.06×
Compile speed

<1 s

to rebuild the whole 34,000-line compiler on the native backend. Dev builds on Linux and Windows go straight to machine code, with no C compiler.

Memory

No GC

Reference counting with copy-on-write values. Memory is freed at scope exit, so there are no pauses to tune.

Checks

Proven away

Bounds and overflow checks the prover removes cost nothing. brine check --report shows what was proven.

Your coding agent
already speaks Brine.

Familiar syntax, one way to write things, and a compiler that rejects whole classes of bugs. That's the feedback loop an agent needs. Diagnostics come as JSON, and the whole language fits in one page of context.

--json

Diagnostics a program can read

Stable codes, exact spans, notes and help. One object per line, so an agent can act on it without parsing prose.

$ brine check --json
{
  "severity": "error",
  "code": "E0501",
  "message": "cannot assign to `total` inside a `par` body",
  "file": "race.br",
  "line": 5,
  "column": 9,
  "end_line": 5,
  "end_column": 14,
  "label": "would be a data race",
  "related": [],
  "notes": [
    "`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"
  ],
  "fixes": []
}
brine explain

Every error, explained

All 76 error codes have a written explanation with a fix, from the terminal or the docs.

$ brine explain E0501
E0501: writing shared state in `par`

Iterations of `par` code run at the same time.
To rule out data races, a `par` body may not
assign variables from outside it…
brine guide

The language in one prompt

A complete quick reference that prints in a second. Agents read it once and write idiomatic Brine.

brine new

AGENTS.md in every project

New projects come with instructions for agents: the commands, the rules and the workflow.

demo/AGENTS.md
# AGENTS.md — working on `demo`

## Commands
- `brine check` — type-check and verify (fast; run after every edit)
- `brine test` — run all `test "...":` blocks
- `brine guide` — the full language reference
- `brine explain <CODE>` — explanation of any error code
llms.txt

Docs for models, too

The docs publish llms.txt and llms-full.txt, and every page has a Markdown version. Add .md to any docs URL.

  • /llms.txtindex
  • /llms-full.txteverything
  • /llms-small.txtcompact
  • /parallelism/gpu.mdany page

Using Brine with coding agents

Written in Brine.
Built by Brine.

The compiler, prover, formatter, test runner and GPU code generators are one Brine program. To build it from source you need a C compiler and nothing else. It compiles itself and reaches a fixed point, so a rebuild produces the same output.

34,000+
lines of Brine in the compiler
<1 s
for the compiler to rebuild itself
5
code generators: x86-64, AArch64, C, PTX, Metal
1
dependency to build from source: a C compiler
Read the compiler
  1. bootstrap/brinec.cthe compiler, as generated C
  2. ccany C11 compiler
  3. brinethe full toolchain
  4. compiler/*.brBrine builds itself
fixed pointbrinec.c ≡ brinec.c

Get brining
in a minute.

One command installs the compiler and toolchain. No runtime to set up, no package manager to learn first.

More options
curl -fsSL https://raw.githubusercontent.com/brinelang/brine/main/install.sh | sh
terminal
$ brine new hello && cd hello
$ brine run
     Built hello v0.1.0 [dev] in 2.25s
Hello, brine!
[0, 1, 4, 9, 16, 25, 36, 49, 64, 81]