Memory management

Philosophy: colorless memory management

The problem with having multiple MM strategies is the risk of “coloring”: GC can only talk to GC, Arena can only talk to Arena. This would be the same problem that async introduces into the type system, and that Zig solves by decoupling async from typing via an IO interface.

The solution here is analogous: a MemoryManager interface. Each allocation carries an implicit pointer to its MemoryManager. The runtime calls the interface when it needs to allocate, free or track, without knowing which strategy is underneath. The result is free mix-match between strategies, without coloring, without manual inter-strategy tracking.

The MemoryManager interface

The interface has four methods. The signature is the contract that every strategy (gc/arena/none) implements:

decl MemoryManager {
    fn alloc(size: usize, align: usize) -> Result[Ptr, error{OOM}]
    fn resize(ptr: Ptr, new_size: usize, old_size: Optional[usize]) -> bool
    fn free(ptr: Ptr, size: Optional[usize])
    fn trace(visit: fn(Ptr))      // derived by the compiler; override optional
}

Four decisions define this contract, each in favor of honesty or safety:

• alloc receives alignment (power of 2), not just size; it matters for SIMD, cache lines and FFI. It is Zig’s model.
• resize returns bool, not a new Ptr. C’s classic realloc returns a possibly different pointer, hiding a copy+free behind a call that looks cheap. Here resize only tries to grow/shrink in-place; if it returns false, you decide whether to do alloc+copy+free. No magic copy, the same no-magic philosophy that cut the propagation ? (section 7).
• size is Optional[usize] in free/resize, filled in by the compiler. Since freeing is automatic in the colorless model (section 6), and whoever calls free is the runtime, not you, it is no use to say “pass the size if you want performance”: there is no one to pass it. The turn is that the compiler frequently knows the size statically (size_of[T]() is constant). So it emits free(ptr, size_of[T]()) when the type is known (the common case performance by default, the MM skips the internal lookup), and free(ptr, none) when it is dynamic/type-erased (the MM consults its own metadata simplicity when necessary). It is better than a default parameter: the optimal choice comes from whoever actually knows (the compiler), without a human decision. Implementation requirement: the MM has to work with none (always freeing via its own metadata) and may optimize when it receives the size.
• trace is derived by the compiler (detailed below).

trace derived, and the no-op that is never called

trace is what allows safe mix-match with GC: the collector passes a visit callback, and the object calls visit(field) for each pointer-field it contains, marking the target as alive. The design question is who writes the enumeration logic, and the answer is: the compiler, never you.

The compiler knows the layout of each type (which fields are pointers, where they are). So it synthesizes the trace automatically, via the same comptime reflection that auto-derives serialize (section 10):

decl Node { next: *Node; data: *byte; count: int }
// the compiler generates the trace: visits next, visits data, ignores count (not a pointer).
// you write nothing.

This eliminates by construction the classic manual-GC bug (“I forgot a field in the trace the collector does not see it collects a live object use-after-free”): the compiler never forgets a field. It is the same play as exhaustive match: safety comes from the compiler knowing the structure. Manual override exists only as an escape-hatch for exotic cases (custom FFI layout, “hidden” pointers that reflection does not see); 99% of types use the derived one.

The no-op trace of arena/none is not a method that is called and ignored; it is a call that is never generated. The intuition (“the GC skips arena/none”) is the right result; the correction is who decides and when: it is not the GC at runtime, it is the compiler at compile time. If the GC consulted “is this object arena or gc?” for each object in the graph, it would be a branch per object: millions of objects, millions of branches, and an MM tag read on each visit, which is expensive. But the compiler already knows statically which MM each allocation uses (it is what makes dead-MM elimination work, see further on), so it simply does not emit tracing for arena/none objects. The trace of Arena/Manual exists in the interface for completeness, but the body { } never runs because it is never invoked.

// runtime no-op (NOT how it works), one branch per object:
loop obj in grafo { if obj.mm.is_managed() { obj.mm.trace(obj, visit) } }

// static no-op (this is how it works), zero cost:
// on seeing that 'buf' is @mm(arena), the compiler does NOT emit tracing for 'buf'.
// the GC never finds it in its scan root.

The gcarena boundary (a GC object that contains a pointer to an arena object) is also static: the GC object’s generated trace, on reaching that field, sees by the pointer’s type (which the compiler knows) that it points to something arena-managed and does not recurse there. The compiler emits “this field points to arena do not trace this field”. Zero overhead, again, and no runtime tag. When the GC runs, it finds Arena objects in the graph and never tries to trace them, move them or corrupt them, because the call simply does not exist.

Available strategies

Each strategy is an implementation of the MemoryManager interface:

Strategy	Description
gc	Garbage collector: automatic tracking of live references
arena	Arena allocation: bulk release when the arena is destroyed
none	Manual, like C: explicit alloc/free by the developer
c	Memory coming from C via FFI: the interface points to C’s free/deallocator (section 17)

What @mm means

@mm defines the default MemoryManager for new allocations within that context: process, function or object. It is not a fixed tag on the type; it is the allocator that will be used when no other instruction exists.

// global default MM: defined at compile time
// --mm=gc   (default if not specified); --mm=arena / --mm=none make main and
// every process spawned without its own @mm run under that strategy. A program
// with no gc context anywhere (no @mm(gc), no @promote(gc)) links no collector.

// Override per process: all new allocations inside worker use arena
@mm(arena)
spawn worker(data)

// Override per object: this specific allocation uses arena
buf: HugeBuffer @mm(arena) = ...

// No annotation: uses the current context's MM
x: SmallStruct = ...   // uses the current process/function's @mm

The context is dynamic: what a function allocates follows the @mm active where it is called, unless it declares its own. Each level sets the strategy for its extent, and an arena one is also a region whose memory goes back whole when it ends:

Context	Strategy for	An arena region dies
@mm(kind) spawn f()	the whole process	with the process
@mm(kind) fn f()	each call of f (and its callees)	when the call returns: one fresh region per call
@mm(kind) { ... }	the block (and its callees)	at the block’s end, on every exit (return, break, continue included)
x: T @mm(kind) = ...	x’s initializer	when x’s scope ends

A pointer into a region that has ended dangles. The compiler catches it in the local scope — a pointer allocated in the region and used after it (stored in an outer variable, carried out by a break, returned) — the same courtesy check as a use after free; the general escaping case inherits arena’s unsafe semantics. To keep a value past its region, copy it out with @promote.

Values live where they were made

Values — a string’s bytes, a slice’s or List’s backing, an interface’s box — follow the same contexts as mm.alloc:

Context	Where a value made here lives	When it dies
gc	the collected heap	when nothing reaches it
arena (block, call, object, process)	the arena’s region	with the region
none	the value region of the scope it was made in	at the end of that scope, like a C local

So a program that is entirely none or arena needs no collector at all.

Each strategy also compiles to its own code. A function is colorless — it allocates under whatever strategy is active where it is called — so the compiler builds it once for each strategy it actually runs under (a program that names a single strategy builds it once). The gc build carries none of the region machinery: no value scopes, owners or escape copies, except where it reaches another strategy’s memory through a pointer or a mut parameter. The none and arena builds carry none of the collector’s: no collection polls and, unless they call into gc code, no stack roots. A function value or an interface method runs the build of the strategy its call is made in.

A value never dangles, because leaving its lifetime is a copy — the copy-on-bind every value already has (section 6, “sharing is an optimization”), done for real only when sharing would cross a lifetime. A value leaves its region at exactly three points:

• assigned to a variable declared in an outer scope;
• stored into a field, element or container that outlives it;
• returned.

The copy lands where the destination lives: the outer scope, the container’s region, or the caller’s context. A value stored through a pointer — a mut argument, a pointer receiver, a closure’s capture — finds the scope its target belongs to. A value stored into a module variable lives as long as the process. Nothing changes under gc, where everything stays in the collected heap.

@mm(none) fn names(n: int) -> List[string] {
    var out: List[string] = List.new()
    loop i in 0..n {
        let s := "item-{{ i }}"    // made in the loop body's region: dies each iteration
        out.push(s)                // copied into out's backing, which lives as long as out
    }
    return out                     // copied into the caller's context
}

Under none a variable owns its value, like a C++ std::string: reassigning it (or a field or element of it) lets go of the old value, and the end of its scope lets go of what it holds. Owned values are counted, so places that hold the same value share it — a binding read from a variable, an element stored from another — and the last one to let go frees it. A view of a List (xs[a..b]) holds the backing the same way: it stays a window onto the List (a write shows through both), and nothing is freed under it while it lives, even if the List is reassigned or grows. A List read whole from a place is shared too — one more count, no copy — and is copied only when one of its holders writes it (copy-on-write: storing into an element, a push, a mut argument or a pointer into it), so its holders stay independent values; copying it frees nothing and changes nothing anyone else sees. A view is not a holder: xs[a..b], xs.to_slice() and a pointer to an element are windows that must see every write of the List they came from, so a List with a view is copied at once when bound, as before. Views are counted apart from holders: a let bound to a view counts only while its scope lives (after it, the List is shared lazily again); any other view (an argument, a field, a pointer) marks the List for good. A slice read whole is still copied on bind (section 6). At a variable’s last use, either one simply moves. Appending to a string that a variable holds alone (s = s + x, s += x, s.append(x)) writes into the string’s own memory when there is room. An accumulator in a loop therefore runs in constant memory and amortized constant time per append, without a collector. An arena keeps the bump contract: it never frees one object, so a value reassigned inside an arena region stays until the region dies. The memory analyzer points out that accumulator pattern (“use @mm(none) or gc for constant memory in this loop”).

The memory analyzer (-Wmm, mk analyze) lists every escape copy with its place and reason; returns are listed as information (-Whints), since a return is the sanctioned way out. --strict-mm turns each store-side copy into an error that says “promote it or return it”, for code that must never copy implicitly. Writing @promote on the stored value (last = row @promote(none)) marks the copy as intended.

var last := ""
loop i in 0..3 {
    last = "row {{ i }}"                  // -Wmm: copied out of this scope; an error under --strict-mm
    last = "row {{ i }}" @promote(none)   // the same copy, written explicitly: accepted everywhere
}

Each allocation carries its MemoryManager

When an object is allocated, it receives an implicit pointer to the MemoryManager that created it. That pointer travels with the object, regardless of which process contains it now.

// Process A: @mm(arena)
buf: HugeBuffer @mm(arena) = ...   // buf.mm = ArenaInstance

spawn gc_worker(buf @transfer)

// Process B: @mm(gc), but buf.mm still points to Arena
// Process B allocates new things with GC
// When buf goes out of scope: runtime calls buf.mm.free() → Arena.free()
// The GC does not touch buf. The arena does not leak.

There is no inter-strategy tracking. The runtime does not need to understand “GC tracking Arena”; it just calls buf.mm.free().

MM boundaries: transfer between processes

@transfer between processes with different MMs is valid. The object arrives at the destination process with its mm intact. The destination process uses its @mm for new allocations; the received object’s mm is used only to free it when it goes out of scope. (Both @transfer and @promote are transient behaviors, in the sense of section 6: they annotate how a value crosses the boundary between processes, move or copy, not a value that persists.)

Along the same line, a note about infrastructure: a process’s control-block and the buffer of a buffered channel belong to the runtime, not to the @mm of whoever creates it. So a @mm(none) process still spawns children (each with its @mm) and uses a buffered channel normally: none means your heap allocations are managed manually (explicit alloc/free, C-style, per the strategy table), it does not forbid the heap and it does not touch the runtime’s own bookkeeping.

// Valid: Arena → GC via @transfer
@mm(arena) spawn producer(data)
@mm(gc)    spawn consumer(chan)

// producer
result: Data @mm(arena) = process(data)
chan <- result @transfer

// consumer receives result with result.mm = Arena
// consumer allocates its own things with GC
// when result goes out of scope: result.mm.free() → Arena.free()

@promote(mm, level): optional optimization

@promote copies an object to a new MemoryManager. It is a performance tool, not a correctness one: mix-match works without it. In terms of the interface’s methods: @promote(gc) ≈ dest.alloc(size, align) copy bytes (eventual) source.free. It is a memory directive, so it uses the @ sigil, in the same place as @mm/@transfer:

// Without promote: works correctly, zero extra design cost
chan <- result @transfer

// With promote: copies result to the GC before transferring,
// allowing the source arena to be destroyed without waiting for the consumer
chan <- result @promote(gc) @transfer

The copy level is a parameter, level: shallow | deep (probably an enum), with default shallow:

result @promote(gc)           // shallow (default)
result @promote(gc, deep)     // deep, explicit

• shallow (default, cheap): copies the object; the internal pointers keep pointing to the same original children. A deep copy by reflex would be wrong here: an “optimization” that silently copies a whole graph becomes the most expensive thing in the program, and duplicating shared children breaks identity/aliasing. The post-shallow graph is just another case of “an object of one MM pointing to an object of another MM”, which trace already covers (the GC traces the gc-copy, finds the pointer to the arena child and does not recurse).
• deep (expensive, explicit): copies the object and the reachable subgraph to the destination MM. It is what you use to cut the cord with the source, when you want to destroy the entire arena and need nothing else to point to it. The deep carries the cost warning, just as @mm(none) carries the responsibility warning.

The source is not freed automatically. @promote is purely “copy over there”; the original follows the normal lifetime rules (it dies when it would go out of scope anyway). Whoever wants to free early calls the source strategy’s free explicitly (destroy the arena in bulk). No free semantics built into @promote.

Two compiler diagnostics accompany @promote, and the first is bigger than it looks:

free of a region with a live pointer: local detection plus unsafe territory in general. A shallow that retains a pointer to the source and then frees the source leaves a dangling pointer. But this is not a special case of promote; it is the general case of manually freeing a strategy while there are live pointers into it (you can create the same situation with arena.free() and a raw &, with no promote at all). And proving there is no live pointer at the moment of the free is lifetime analysis, which the language decided not to have. The honest resolution is two combined levels:

• Local detection (courtesy): in the same scope, the compiler sees the shallow @promote(gc) retain a pointer to buf (arena) and an arena.free() afterward error, with a clear message. Catches the obvious case.
• Unsafe in the general case: when the pointer escapes to another function, arena/none inherits the unsafe semantics: you asked for manual management, you own the lifetime. It is the price of the escape-hatch, consistent with “no lifetimes”. The GC remains the safe-by-construction path; arena/none is the fast-but-you-take-care one. And the honesty has to be explicit here: for the hard case (complex mutable aliasing graph, pointers escaping between structures, exactly where Rust’s borrow checker cost pays off) this language gives less static guarantee than Rust, not a slimmed-down version of the same. Outside the GC there are no lifetimes nor the tooling that proves absence of dangling; there is human discipline, as in C. It is the conscious price of not having lifetimes, and the GC is the net that makes it payable.

The local ownership gate, and opt-in @consume

Two things sharpen that net on the manual path (arena/none) without turning into a borrow checker. Both stay off the GC path entirely, so safe code never meets them.

The local gate is always on, sound, and free. Where an allocation and its free live in the same function and the pointer does not escape (not returned, not stored in a struct that escapes, not @transfer-ed), lifetime is decidable — no lifetimes needed to know it — so the compiler makes it a hard error, not a courtesy: a manual alloc with no free on some path is a leak error, a second free is a double-free error, a use after free is a use-after-free error. This is the local courtesy check (above) promoted to a gate. It is sound and complete on this fragment (it never misses a bug and never rejects a valid program there), because the fragment is decidable; it needs no annotation; and it is exactly “you cannot compile obviously-broken manual memory”. Each of these is judged per path: a free on one branch followed, after the branch, by a use or a second free is a use-after-free / double-free on the path that took the branch, and is reported as a conditional one (a branch that diverges – { free(p); return } – contributes nothing to the code after it, and a branch whose condition is known at compile time – a literal if false, or a const such as const DEBUG := false; if DEBUG { ... }, including !/&&/|| of those – is not a path at all; it is still checked, it just does not reach the code after it. An immutable let does not decide a branch: it is a runtime binding even when its initializer is a literal). The same per-path rule governs the moves of @transfer and @consume below.

The escape boundary stays unsafe by default; @consume is the opt-in upgrade. The moment a manual pointer escapes the function, the property becomes undecidable (Rice), so a sound gate would have to reject valid programs — the borrow checker’s bill. Makoto does not send that bill by default: an escaping arena/none pointer keeps the unsafe semantics above (human discipline, GC as the net). But an author who wants the guarantee across the boundary marks the parameter @consume (written after the type, like @mm: fn free_it(p: *T @consume)): it makes the pointer linear (affine ownership) — the callee now owns it and must free-or-transfer it exactly once, and the caller may not use it afterward (@transfer’s move-invalidation, generalized). The obligation is discharged by any of: freeing it, returning it, passing it to another @consume, @transfer-ing it — or storing it in a field of a struct that itself escapes (returned or transferred). This last case is a valid transfer: fn keep(p: *T @consume) -> Box { return Box{ owned: p } } moves ownership into the Box, and the Box carries it out to the caller, so p is accounted for — no leak. Field-capture-into-an-escaping-aggregate counts, symmetrically with how the local gate treats “stored in a struct that escapes” as an escape. Because the move happened through a capture rather than a written marker, the memory analyzer (below) adds a hint, never a warning, suggesting the explicit form, Box{ owned: p @transfer }; writing it (or returning p itself) silences the hint, and the program is correct either way. This gives the sound cross-function gate (leak/double-free/UAF caught through the call) with no lifetimes — ownership is move, not borrow, and lifetimes are the tax on borrows, which the language does not have.

@consume on a function parameter: called exactly once. Calling a function value consumes it, so the same decorator on a parameter of function type, f: fn() @consume, says the callee calls f exactly once on every path. It is checked inside the callee like a manual pointer’s obligation: a path that does not call it is an error, a second call is an error, and so is any use that could repeat it – passing it to an ordinary parameter, or calling it inside a lambda or a loop body. Handing it to another @consume function parameter is its one use. A caller can rely on it: a lambda passed to such a parameter runs once, at the call, which is what lets it use something that must be used once – a <-> reply address (section 4):

fn with_lock(f: fn() @consume) {
    lock()
    f()                 // exactly once, on every path
    unlock()
}

req, reply := <-> ch catch |e| { return }
with_lock(fn() { reply <- answer(req) })    // ok: the lambda runs exactly once
xs.each(fn(x) { reply <- x })              // error: each's parameter is not @consume, so it may run many times

“At most once” (a lambda that may not run at all) is the affine @consume_once of the verification layer (verification.md section 2), which also covers function parameters when that layer arrives.

@consume is an opt-in contract, in the exact slot of @requires/@ensures (section 14): a per-function promise that is checked where it is written and invisible where it is not. It passes the opt-in test the same way — a caller only meets @consume on an API whose author chose it, and only on the manual path, which is already opt-in. It is not tainted coloring (section 1): it is memory’s own color (ownership) on a memory operation, not one system’s color leaking into another. The default remains “C with a GC net and a local gate”; @consume is the summonable “prove the ownership” upgrade for the rare API that wants it, never the ambient rule. It is one decorator (consume covers ownership-and-free; borrow is the silent default), never a lifetime zoo.

Unnecessary deep: warning, never error. The compiler does not know whether you needed deep (it depends on your future intent to destroy the source). But it detects the degenerate case (deep over an object with no pointers, or whose pointers are all already of the destination MM), where deep and shallow are provably identical warning (“unnecessary deep; use shallow”). Superfluous deep is waste, not a bug.

autofree: the ownership gate, run as an optimization

The local ownership gate (above) proves something valuable and then only uses it to diagnose: on the decidable fragment — an allocation whose pointer does not escape, whose last use is determinable in this function — the lifetime is known with no lifetimes. autofree turns that same proof into an optimization. Where the analysis proves a linear lifetime, the compiler inserts the object’s free right after its last use instead of leaving the object for its MemoryManager to reclaim later. It is a compile-time pre-pass: try to autofree; where it cannot prove, leave it to the MM.

The payoff is largest on gc. A collector’s cost scales with the number of live objects it has to trace; an object with a provably-linear lifetime never needed to be a managed object at all — it is born, used, and dead within one frame. Autofreeing it removes it from the collector’s world: fewer roots to mark, fewer objects to sweep, less heap that ever reaches a collection. And it generalizes, because freeing is colorless (free(p) routes through the object’s own mm, above): the same pre-pass helps arena and none too, not just the collector. It is Go’s escape analysis with the decision pushed one notch further — not merely “stack or heap”, but “free at last use, or hand to the strategy”.

Soundness is the whole point, so it only ever acts on the provable. Any mistake here is a use-after-free, so autofree inserts a free only where the escape-and-last-use proof is total (the decidable fragment, 100% precision); the instant a pointer escapes, is stored where it might outlive the frame, or has an undecidable last use, the object falls back to the MM exactly as before. And because it only frees an object the proof shows is already dead, autofree cannot change observable behavior — it changes when memory is reclaimed, never what the program computes. The same source produces the same output with autofree on or off. Where the last use is a plain statement in the object’s own scope, the reclaim lands right after it rather than at scope end (so a long tail of unrelated work no longer holds the object live); where the last use straddles branches, the reclaim falls back to scope exit, always guarded so no path frees twice. And the reclaim is colorless — it routes through the object’s real manager at run time, since the ambient @mm strategy is dynamic: a gc object is reclaimed from the collector, a none object is freed, and an arena object is a deliberate no-op.

That arena no-op is a real limitation, stated plainly: an arena is a bump allocator, and a bump allocator cannot free one object — it reclaims the whole region at once, which is its entire reason to exist. So autofree cannot free an individual arena object early; it can only decline to, and let the arena’s mass reclaim do its job. The one way to give an arena object an early death would be to not put it in the arena at all — allocate it on the stack, or on the freeable none heap — but that breaks the neutrality guarantee above: an object that never reaches mm.alloc is missing from mm.used and the memory observability of section 19, so the program’s observed memory would depend on whether autofree ran. Autofree refuses that trade by default: the guarantee that on/off is invisible is worth more than an early free the arena was designed not to need. (Retargeting could be offered someday as an explicit, neutrality-waiving opt-in; it is not the default, and not implied by @mm(arena).)

Autofree is on by default (--no-autofree disables it), and its aggressiveness is a build knob, --autofree=<mode>, in the spirit of a C compiler’s warning-to-error dial:

• default — autofree acts on gc and arena allocations (arena only as far as a bump allocator allows — see the no-op above; the real reclaim is on gc). none is untouched: its manual-free contract and the leak/double-free/UAF gate stay exactly as documented above.
• conservative — the analysis runs over every strategy, but none keeps its manual contract: an @mm(none) allocation still requires your explicit free, and a missing one is still a leak error. Autofree never inserts a free into none here (that would double-free your manual one); it is opt-in coverage of the analysis without loosening a single none diagnostic.
• optimized — autofree acts on none as well: an @mm(none) allocation with a provably-linear lifetime and no manual free gets one inserted for you, and is therefore no longer a leak error — the compiler freed it. You still own the escaping cases (unprovable lifetimes stay unsafe, as ever); this mode simply lets the decidable fragment of manual memory be as ergonomic as gc, with the manual free reserved for what actually escapes.

The default is the safe middle: it lightens gc for free (an object with a provable local lifetime never has to be a managed object) and leaves the manual path’s contract untouched, so no existing none program changes meaning. optimized is for the author who wants the proof to also discharge manual frees; conservative is for one who wants the analysis everywhere but not a single none error relaxed.

The memory analyzer: a borrow-checker you consult, not one that fights you

The same escape-and-lifetime analysis that powers the gate and autofree can say more than it enforces. A tool built on it is a borrow-checker inverted: where Rust makes the check mandatory (the tax you pay on every program), Makoto makes it advisory by default and reserves compilation-blocking for what it can prove is catastrophic. You get the borrow-checker’s utility — bugs caught at compile time — without its bill, because the GC is still the net and the decidable gate is still the only thing that must pass.

It reports in tiers, by how sure it is:

• Proven-fatal always an error. The decidable-fragment gate (leak / double-free / use-after-free on a non-escaping manual pointer), a @consume obligation dropped, a use after @transfer — and any wider case the analysis can prove, not merely suspect. These block the build. Memory corruption is never a warning.
• Likely-wrong a warning. In the undecidable zone (Rice), where a pointer escapes and might be used after free, or an alias is ambiguous, the analysis is honest that it is guessing: it warns, and the program still compiles. --strict-mm (a -Werror=mm dial) promotes these to errors for the author who wants the rigor.
• Could-be-tighter a hint. “this pointer never escapes — it could be @consume”, “this is autofree-able” — off the critical path, opt-in.

Two things keep the tool from being either useless or tyrannical. Strictness is a build dial, never source you rewrite: --strict-mm (the -Werror=mm) promotes the whole warning tier to errors for the entire compilation at once — a project turns the rigor up with one flag, and a build that wants it finer sets it per module in the project config, never by annotating functions one at a time. You do not touch a line of code to make the analyzer stricter, and there is no per-function keyword to sprinkle (that would be exactly the tax this language refuses). And every warning is suppressible at its site: the author who knows a specific finding is a false positive silences that one by writing the audited assume "reason" trailer on the flagged operation itself — free(p) assume "I checked the aliasing; the alias is dead here". It is the same keyword unsafe already uses (no new one), now reading as “analyzer, I have discharged this”, and it stays greppable and non-empty like every other assume, so the suppression is itself part of the audit surface. A growing project therefore never drowns real findings under a rising tide of false ones. This is safe precisely because the tool is opt-in: it does not need to defend against a lazy developer, because a lazy developer never turns it on; it exists to serve the one who wants the extra pair of eyes, and that one is well served by being able to answer it.

Underneath, it is not a fixed checker but a framework: the compiler supplies the sound core and the heuristic tiers, and the comptime contracts of section 14 let a codebase add its own invariants — the author writes the memory analysis their domain needs, checked at compile time, rather than accepting one fixed borrow discipline. The stdlib seeds this with predicates like mem.is_pointer_free[T]() (true when T holds no pointer of any kind — safe to bit-copy, nothing for the collector to trace), a comptime fn over the type’s reflected structure; drop it in a contract, @requires(mem.is_pointer_free[T]()), and a violating instantiation is a compile error, not a runtime trap. It is the opposite of Rust’s trade: the rigor is the thing you summon, not the thing that chases you.

In practice the tool has three surfaces: -Wmm on any build turns the warnings on; mk analyze runs the whole thing and prints a report (errors, then warnings, then hints, with a count), producing no binary, so a project can gate CI on it; and strict-mm true in mk.project persists --strict-mm for every build of that project, the config knob the “build dial, not source you rewrite” rule points to.

MM boundaries: returns from processes

When a process returns a value:

• Data received via @transfer, not mutated returns with its original mm
• New data without annotation uses the caller’s mm (the child process’s heap was discarded)
• New data with explicit annotation uses the specified mm

return x               // x returns with its original mm (it was passed via @transfer)
return new_val         // new_val uses the caller's mm
return new_val @mm(gc) // explicit mm

Per-process memory limits

spawn worker(data)       // no limit (default)

@limit(16mb)
spawn worker(data)       // fixed limit

The limit budgets the process’s total memory, not one kind of allocation: everything it keeps alive counts, strings, slice and List backings, the payload of its structs and enums, its mm.alloc blocks under every strategy (gc, arena, none), and its own copy of the module’s mutable globals. It is judged on live memory: what the process has already dropped does not count against it, so before an allocation is refused the runtime collects the process’s garbage and checks again. A loop that builds and discards a string per iteration runs under a small limit indefinitely; one that keeps every string it builds hits the limit.

The process’s stack is not counted by default: it has a bound of its own (below), and a process that runs out of it dies on its own with Crashed("stack overflow"). When an application wants the one number to cover the stack too, it asks for it at the spawn:

@limit(16mb, stack: true)
spawn worker(data)       // the limit also counts the stack the process actually uses (its deepest point so far)

A limit can also be put on a block, for the process that runs it: @limit(N) { ... } makes the current process’s budget the smaller of its own and N while the block runs, and the previous budget comes back however the block is left (the end, a return, a break). It only narrows: a block inside a process spawned with @limit(64kb) cannot grant itself more. It is still the process’s total memory that is judged – what the process held before entering the block counts – and crossing it is the process’s OutOfMemory, exactly as for a spawn’s limit (in main, the program fails). stack: true belongs to the spawn, where the stack is reserved.

@limit(64mb) {
    doc := parse(input)    // this step may not take the process past 64 MB
}

What the process “keeps alive” is what its variables in scope hold: a value counts while a variable that is in scope holds it, an expression’s temporary until the end of the statement that made it, a block’s locals until the block is left (a loop body’s, at the end of each iteration), a parameter until its function returns. A value nothing in scope reaches any more is garbage and never counts, even before it is collected.

Where the limit is judged. The limit is checked after every statement and on entry to every function, so a process dies on the statement that crossed it and nothing after that statement runs. A point that nothing could have allocated before since the last judgment is not re-judged (memory that only shrank cannot be over a limit it was under), so code that only computes pays nothing, and code that allocates pays a load and a branch per allocating statement. On top of those, three points are judged whatever the build:

• at every mm.alloc, and at every loop iteration and every call of a recursive function that allocates;
• before every operation that can block: a send, a receive, <->, select, p.wait(), runtime.wait_children(). A process over its limit dies before it parks, rather than waiting for a message while holding more than its budget;
• at the request itself when a single allocation is larger than the whole limit: a block that alone exceeds the budget can never fit, however much garbage a collection would free, so the process dies on the spot, even for a temporary the next statement would have dropped. The sizes are those of the real requests: a concatenation’s bytes, a List’s doubled backing, an interpolation’s buffer as it grows, a transcoding buffer, each string and backing of a value copied in from another process (a received message, spawn arguments).

With stack: true, the stack in use is measured at those same points.

A build can relax the statement and function-entry points with --no-strict-limit: the limit is then judged only at the three points above, and a straight-line run of statements that builds values without looping, calling a recursive function or blocking may briefly hold more than the limit before the next one. Both the interpreter and the compiled program judge at exactly the same points in either mode, so a program’s output under @limit does not depend on the backend.

If the process exceeds the limit: the scheduler interrupts the allocation, the process dies, and the OOM reason reaches the supervisor as the error value of the catch |e| (section 8), which decides the strategy (restart smaller, degrade, propagate).

Process stacks

Each process has its own stack. It is reserved, not allocated: the runtime reserves address space for it and the machine hands out memory only for the pages the process actually reaches, so a process that uses 8 KiB of stack costs 8 KiB however much was reserved, and a deep recursion grows into its reservation without anything being copied or moved. The reservation is 8 MiB by default (what main, and a thread in most systems languages, gets), configurable for the whole program by a build flag (--stack-size=64mb) and per spawn:

@stack(64mb)
spawn parser(input)      // a deeply recursive worker gets more room

Running past the reservation kills that process, as a crash its supervisor sees as Crashed("stack overflow"); in main it is the program failing. On WebAssembly, where linear memory is committed up front, a spawned process’s stack defaults to 256 KiB (main still gets 8 MiB, or --stack-size when larger), and since wasm has no guard page every recursive function checks its stack on entry: a recursion past it dies the same way, as a stack overflow of that one process. A supervisor that restarts the process re-creates it with the same reservation, and with the same @limit and @mm its spawn declared: a restart is the spawn again, not a looser copy of it. When a process that went deep dies, the pages it touched go back to the machine before its slot is reused, so one deep recursion does not keep its memory for whoever comes next.

The compiler sizes stacks from the call graph where it can. For a process whose calls have no recursion, no call through a function value and no call into C, the deepest stack it can ever need is known at compile time (every frame’s size is): that process gets exactly that reservation, and a guarantee that it cannot overflow. Anything else falls back to the default or to its @stack. On targets that commit memory up front (WebAssembly’s linear memory), the computed size is what saves memory, and a stack there can grow by being copied to a larger one.

OOM is a process event, not a per-call error

Every allocation can, in theory, fail, but OOM is not threaded per-call in the high-level operations (List.push, string.append, Buffer.write, encode). That would be coloring: if every push/concat returned Result[_, error{OOM}], the allocation failure would infect every signature that touches a collection, exactly what the colorless of this section avoids (the allocator travels with the object via @mm, not in the signatures; threading OOM would require bringing it back). The rule is BEAM’s: the allocation that fails kills the process, and the supervisor handles it (section 8). The error appears once, at the supervision boundary (as the value of the catch |e|), not at each allocation site.

And there is a physical reason for this not to be a loss: on an OS with overcommit (the Linux default), you do not even catch the OOM for real at the call site: alloc returns success and the OOM killer kills the process on a memory access further ahead, not on the call. OOM is only catchable/recoverable when there is a budget below the machine limit: an arena with a cap, a @limit, a fixed buffer, or a target without overcommit (embedded). The ruler:

• Unlimited allocation that fails = the machine ran out = crash (and, on the common OS, not even detectable at the point). Handling is the supervisor.
• Allocation with a budget that fails = you hit your ceiling = recoverable.

The hatch for the recoverable case is to descend to mm.alloc, which returns Result[Ptr, error{OOM}] (the MemoryManager interface, above), for the allocator author and for the “try to fit this budget; if not, degrade” pattern (allocate a large buffer and, on failure, stream instead of dying). Two worlds without conflict: high-level colorless-that-crashes (the 99% case), low-level explicit-Result (the MM author and budgeted-OOM).

This is convergent design: Rust also decided allocation infallible by default (push/Box::new abort) with try_reserve as the fallible opt-in; here you gain BEAM’s supervisor as the place to handle it, which Rust does not have. And preventing OOM, instead of handling it, is the orthogonal layer of backpressure: a bounded channel blocks the sender when it fills, throttling the producer before memory blows up (section 4). Throttling is prevention (upstream); the supervised crash is what is left when prevention was not enough.

No shared memory between processes, and what processes share instead

There is no raw shared memory, and no @shared. A process never holds a writable reference into another process’s memory. That is what makes data races impossible, and it is also what lets the language do without lifetimes: no reference ever has to be proven not to outlive the memory of a process that may die. Memory that more than one process can see is in exactly one of two categories:

1. Immutable: a Shared[T] (below). Nobody writes it, so every process can read it at once, with no copy and no lock. Its one mutable part is the atomic cells it may contain (atomic.Atomic[T], below): memory changed only by atomic operations, which by definition cannot race.
2. Owned by the runtime, with a copy at the boundary: a channel (its buffer belongs to the runtime, not to any process) and a Table[K, V] (below). Values go in and come out by copy, so nobody holds a reference into the structure.

There is no third, safe category of mutable memory shared between processes. “Writing” shared data is publishing a new version of it, or asking its owner to. The only way to get raw writable shared memory is the unsafe escape hatch at the end of this section.

Module-level variables are per process, too. A top-level var/let is not a global shared by every process: each process has its own copy. A spawned process starts with a copy of its spawner’s module variables as they were at the spawn, deep-copied like a spawn argument; after that, neither side sees the other’s writes. A process restarted by its supervisor starts again from the copy its spawn took, not from what the dead incarnation left behind: that copy is part of its initial state (section 8).

A module-level binding cannot hold a raw pointer. A top-level let/var whose type is or contains *T or [*]T (directly, or inside a struct, an enum, a List, an Optional, an array or a tuple) is a compile error: a raw global. Copying a process’s globals cannot copy what a pointer points at, so the child would inherit an address into its spawner’s heap: shared memory by accident, a dangling pointer once the spawner dies, and a stale one once a moving collector compacts. A pointer the whole program needs lives in main and is passed down as a parameter; data each process keeps for itself lives in a List or slice global, copied like everything else; data every process reads lives in a Shared[T].

Shared[T]: immutable data every process reads

A large read-only dataset (a lookup table, a model’s weights, a parsed configuration) is the one place where copying per process is the wrong answer: a thousand processes reading the same 500 MB table must not mean 500 GB of copies, nor a message round trip per lookup. Shared[T] is the answer, and it is a type, not a decorator, because the guarantee has to travel with the value: a function that takes a Shared[Table] knows it cannot write it, and a Channel[Shared[Table]] knows that what crosses it is a handle.

weights := Shared.new(load_weights())               // copied ONCE into memory no process owns, then frozen
weights := Shared.new(@transfer load_weights())     // or adopted without even that copy
spawn worker(weights)                               // crosses as a small handle: O(1), whatever the size

• Creating it copies the value once into a region the runtime owns, outside every process’s heap, and freezes it. T must be plain data: no *T/[*]T, no channel, no closure (atomic cells are allowed: they are what stays mutable). With @transfer, the region adopts the value’s blocks and nothing is copied at all.
• Passing it, through a channel, a spawn argument or a global, copies the handle, never the data. A thousand processes hold a thousand handles to one region.
• Reading it reads the region directly, at ordinary memory speed, with no lock: nobody writes.
• Writing it is a compile error. A value obtained from a Shared cannot be bound to a var, passed as mut, or stored into a mutable aggregate without an explicit copy. The exception is a field of type atomic.Atomic[T] (below), which is changed through its atomic operations: shared counters, flags and sequence numbers without a message or a lock (Erlang’s atomics/counters modules are the same idea).
• Its lifetime is the set of its handles. The runtime counts them: a handle goes away with the process that holds it, or when the collector drops the value that held it, and when the last one goes the region is freed. That is why it needs no lifetime in the type: the region cannot be freed while anyone can still read it, and nobody can write it.
• By name: Shared.publish(name, s) makes a value findable, and Shared.lookup[T](name) -> Optional[Shared[T]] finds the version published under that name now (checking at run time that its type is T).
• It belongs to no process, so it counts against no process’s @limit; the runtime reports it in runtime.stats(), with an optional program-wide cap. The moving collector never moves it (it is outside the heaps). Over a network channel it is serialized like any other value.

Writing shared data: publish a new version

A shared value is changed by publishing a new version. Readers that hold the old version keep reading it, unchanged, until they let it go; whoever looks the name up afterwards gets the new one. There is no moment where a reader sees half an update, and no pause for anyone.

decl Config { rates: Map[string, f64]; version: int }

fn main() {
  Shared.publish("config", Shared.new(load_config()))     // version 1
  loop w in 0..100 { spawn worker() }
  ...
  Shared.publish("config", Shared.new(load_config()))     // reload: version 2 replaces it under the name
}

fn worker() {
  loop {
    job := next_job()
    cfg := Shared.lookup[Config]("config").or_panic()     // the version that is current NOW, in O(1)
    handle(job, cfg)                                       // this job finishes on the version it started with
  }
}

When the writers are many, they ask the owner: one process keeps the data in an ordinary private, mutable value, receives updates as messages, applies them, and publishes. Readers never send a message; writers never touch the shared copy (the read-copy-update pattern):

enum PriceUpdate { Set(symbol: string, price: f64) }

fn price_owner(updates: Channel[->PriceUpdate]) {
  var prices: Map[string, f64] = Map.new()                 // private and mutable: only this process sees it
  loop {
    u := -> updates catch |e| { break }
    match u {
      Set(sym, p) => prices.put(sym, p)
    }
    Shared.publish("prices", Shared.new(prices))           // in production: per batch or per tick, not per update
  }
}

// a writer, anywhere:   updates <- PriceUpdate.Set("ACME", 189.5)
// a reader, anywhere:   p := Shared.lookup[Map[string, f64]]("prices").or_panic()

Publishing copies the new version; for a large table that changes a little at a time, a persistent structure (a map whose new version shares every unchanged part with the old one) makes a publish cost what changed, not the whole table.

Large mutable tables shared between processes

A table that many processes both read and write is built in one of four shapes, from the simplest to the most concurrent:

• An owner process: one process holds the table; the others send Get/Put requests over channels (<-> for a request and its reply). Simple and consistent; every read is a message round trip.
• Shards: N owner processes, and a key goes to owner hash(key) % N. Reads and writes to different shards run in parallel.
• A published snapshot: the owner above publishes a Shared version; readers read locally, with no message. The best shape for many reads and few writes, at the price of readers seeing the last published version.
• Table[K, V], the runtime’s table: a table that belongs to the runtime, outside every heap, synchronized internally (a lock per shard). t.put(k, v) copies the value in, t.get(k) -> Optional[V] copies it out, and t.update(k, f) is an atomic read-modify-write of one key. Because everything crosses by copy, no process ever holds a reference into the table: no alias, no race, no lifetime. A value that is itself a Shared[X] costs one handle per copy. The handle to a Table crosses processes like a channel’s does.

hits := Table[string, int].new()
loop w in 0..8 { spawn worker(hits) }
// in a worker:
hits.update(path, fn(n) => n + 1)       // atomic for this key
seen := hits.get(path)                  // a copy: Optional[int]

Queues between processes

A queue that one process fills and others drain is a channel: it is already the runtime-owned structure that is written and read concurrently. A bounded buffer gives back-pressure (a producer waits when the consumers fall behind), several receivers share the work, and when the producer is gone the receives end with error.ProcessDown. A large payload crosses as a Shared[T] or by @transfer, so the message is small whatever it carries.

fn producer(out: Channel[<-Task]) {
  loop i in 0..1000 {
    out <- Task{ id: i; img: Shared.new(@transfer load(i)) }   // the message carries a handle
  }
}
fn worker(in: Channel[->Task], results: Channel[<-int]) {
  loop {
    t := -> in catch |e| { break }        // ProcessDown: the producer finished
    results <- process(t.img)
  }
}
fn main() {
  tasks := Channel.new(64)
  results := Channel.new(64)
  spawn producer(tasks)
  loop w in 0..8 { spawn worker(tasks, results) }
  ...
}

The escape hatch: raw shared memory under unsafe

The rare structure that genuinely needs writable memory shared by processes (a lock-free ring buffer, a memory-mapped device, memory shared with C code) uses memory managed by C (@mm(c), section 17) under unsafe. The raw pointer crosses into another process only inside an unsafe ... assume "reason", and the accesses go through atomic operations. It is unsafe by definition: races, ordering and the region’s lifetime are the programmer’s responsibility, exactly as with any memory obtained from C, and the assume reason is what a reviewer reads.

Atomic operations: atomic.Atomic[T]

An atomic cell is a memory location read and written only by atomic operations. It lives in the core package atomic:

use atomic.{Atomic, Order, fence, spin_hint}

Atomic[T]                                      // the cell
Order { Relaxed; Acquire; Release; AcqRel; SeqCst }
fence(order)                                   // a memory barrier on its own
spin_hint()                                    // "I am spinning": PAUSE on x86, YIELD on ARM

(Order, not Ordering: Ordering is already the result of a comparison.)

What T can be. Integers of 8, 16, 32, 64 and 128 bits, signed and unsigned, usize/isize, bool, every fixed-width float (f16, bf16, f32, f64, f128, f256), and raw pointers *T/[*]T (only under unsafe, since a shared pointer only exists in C memory). A heap-backed number (BigInt, Decimal, BigFloat) is not a cell: sharing one is Shared[T]’s job. An integer of an odd width (u3, i24) is a compile error.

Lock-free where the hardware has the width. Where the target has a native atomic instruction for the width (8 to 64 bits everywhere; 128 bits on x86-64 and AArch64), the cell is that instruction: lock-free, the same size and alignment as T, and laid out like C’s _Atomic T, so it can sit in a @repr(c) struct shared with C. Where it does not (f256 everywhere, 128 bits on a target without the instruction), the cell carries its own small lock inside it (a sequence word: readers retry instead of blocking, writers take turns). It still works between processes and across operating-system processes sharing the memory, because the lock travels with the cell rather than living in a table of this process; but it is not lock-free, and it is not C’s layout, so it cannot appear in a @repr(c) type. atomic.is_lock_free[T]() answers at compile time, for code that must assert it.

A cell is a location, not a value: it moves, it is never copied. Assigning a cell, passing it by value or sending it over a channel is a compile error, because the copy would be a second, independent cell (operations on it would silently miss the original) and the copy itself would read the cell with a plain, racing load. A cell is used in place: as a field of a Shared, an element of [*]Atomic[T], a field of a heap object, or through a pointer. Reading its value is fine (n := c.load(.Acquire) copies the number, not the cell); so is making a new cell from it explicitly (Atomic.new(c.load(.Acquire))), and so is moving one (a temporary, or @transfer): Shared.new(Stats{ hits: Atomic.new(0) }) moves the freshly built struct into the shared region, where nobody else ever saw it.

The order is explicit and comptime-known. There is no default order: the order is the contract, and a reviewer has to see it. Each operation becomes one instruction with the order built in, so the argument must be known at compile time, and an invalid combination is a compile error: a load with Release/AcqRel, a store with Acquire/AcqRel, a compare_exchange failure order of Release/AcqRel.

c.load(.Acquire) -> T
c.store(v, .Release)
c.swap(v, .AcqRel) -> T                                        // returns the previous value
c.compare_exchange(expected, new, .AcqRel, .Relaxed) -> Result[T, T]
    // Ok(previous) when it swapped, Err(current) when it did not; compares the BITS of T
c.compare_exchange_weak(...)                                   // may fail spuriously: for retry loops on ARM/RISC-V
c.fetch_update(.AcqRel, .Relaxed, fn(x) => ...) -> Result[T, T]  // a compare-exchange loop around a function

// integers and floats
c.fetch_add(n, .Relaxed) -> T        // CHECKED: an overflow (a non-finite result, for a float) traps, memory untouched
c.fetch_sub(n, .Relaxed) -> T
c.fetch_min(n, .Relaxed) -> T
c.fetch_max(n, .Relaxed) -> T

// integers only
c.fetch_add_wrap(n, .Relaxed) -> T   // the hardware add (lock xadd): wraps, like `+%`
c.fetch_sub_wrap(n, .Relaxed) -> T
c.fetch_and / fetch_or / fetch_xor   // bitwise: nothing to overflow

// waiting without spinning
c.wait(expected) timeout(d)          // parks the PROCESS (not the OS thread) while the value equals `expected`
c.notify_one() / c.notify_all()

Why two adds. + traps on overflow, and an atomic add cannot trap after the fact: once the hardware has written the sum, another process may already have read the wrapped value. So fetch_add keeps the language’s rule with a loop that checks the result before writing (for a float, that the result is finite; a float never wraps, so floats have no _wrap), and fetch_add_wrap is the fast path, named as visibly as +%. compare_exchange compares bits: for a float, 0.0 and -0.0 are different values to it (there is no NaN to worry about, section 14).

wait and notify use wait queues in the runtime, keyed by the cell’s address and integrated with the scheduler: a waiting process gives its worker to other processes, the wait is a cooperative point like a channel operation, its timeout is mandatory as on <-> (timeout(_) waits with no deadline), and it can return without a notification, so it is used in a loop that re-checks the value.

use atomic.{Atomic}

decl Stats { requests: Atomic[u64]; latency_sum: Atomic[f64]; stop: Atomic[bool] }

fn main() {
  stats := Shared.new(Stats{ requests: Atomic.new(0); latency_sum: Atomic.new(0.0); stop: Atomic.new(false) })
  loop w in 0..1000 { spawn worker(stats) }
  ...
  stats.stop.store(true, .Release)                       // every worker sees it
}

fn worker(stats: Shared[Stats]) {
  loop {
    if stats.stop.load(.Acquire) { break }
    t := serve()
    stats.requests.fetch_add_wrap(1, .Relaxed)           // one instruction, no message
    stats.latency_sum.fetch_add(t, .Relaxed)             // a float accumulator: a checked loop
  }
}

Atomic cells are allowed in three places: inside a Shared[T] (safe code, above), in C memory under unsafe (the escape hatch, with any layout and with atomic pointers), and in a process’s own memory (harmless, and useless, since a process runs on one worker at a time; it lets a structure written for sharing also work locally). On targets that run one thread (today’s WebAssembly and JavaScript backends), an atomic operation compiles to a plain access, which is correct there; with threads, it becomes the target’s atomics. The interpreter performs every operation as SeqCst (stronger than asked), so a correct program behaves the same, but a bug that only a weaker order exposes does not show there: that is a job for the model checker of the verification layer (section 21).

The runtime is the same shape, one level up

MemoryManager over MemorySource is a strategy over a source: how I manage over where the RAM comes from. The runtime repeats that shape one level up. The scheduler, the channels and the process lifecycle are the strategy; the machine underneath is the source. So the runtime is not a thing the language depends on — it is an implementation of an interface, coupled at link time, and the pieces of it you never summon are pieces you never link.

The interface is split into capability modules, and the split is what makes that literal:

module	what the host provides	needed by
fatal	how this machine stops	everything (a trap has to end somewhere)
mem	raw memory — the MemorySource	anything that allocates
io	bytes out	io.*, and reporting a trap
time	a monotonic clock	timeout(...), the scheduler’s quantum
task	stacks, hardware parallelism	spawn, channels, supervision

A target implements the modules it has. A kernel in early boot has memory and a serial port but no timer and no threads: it implements fatal+mem+io and gets structs, enums, generics, defer, catch, closures and generators — the last one because a generator is a stackless state machine (section 11), so it needs no scheduler at all. When that kernel later gains a timer and a page allocator, it implements time+task and spawn, channels and supervision start working inside it, with the same compiler and no dialect.

What a target does not implement, it does not get — and that is a compile error, never a silent no-op. A spawn on a target with no task module does not become a spawn that does nothing; it fails to compile, naming the missing capability. The checker knows the target, so the diagnosis points at the spawn, not at a link error about an undefined symbol.

This is the same mechanism as dead-@mm elimination — “dead-code elimination, only over implementations of an interface” — applied to the runtime itself. Tree-shaking here is not the linker guessing what is unreachable: the dependency simply never exists.

The lower layer: the MemorySource interface

The MemoryManager (above) decides how to manage, but it needs to request raw memory from somewhere, and that somewhere changes per compilation target. Hence a second interface, further below: the MemorySource, which delivers raw pages. Same play as the decoupling of IO in Zig and of the MemoryManager itself: one more interface at the point of variation.

decl MemorySource {
    fn map(pages: usize) -> Result[RawPtr, error{OOM}]   // asks the target for raw memory
    fn unmap(ptr: RawPtr, pages: usize)
}

The stack ends up in three layers, each pluggable at its point:

your code (colorless, section 6)
   ↓ uses
MemoryManager   gc / arena / none                "HOW I manage"
   ↓ asks pages from
MemorySource    native / wasm / bare-metal        "WHERE the raw RAM comes from"

One MemorySource implementation per target:

Target	MemorySource.map uses
Linux / Mac	mmap
Windows	VirtualAlloc
WASM / Web	memory.grow over the linear memory
Bare-metal	carves from a fixed region defined at link time (no OS)

The two selections are compile-time and orthogonal: the MemoryManager comes from the @mm/flag; the MemorySource, from the target (--target=wasm selects the wasm Source). Any management over any source (GC over wasm, arena over bare-metal) because the Manager only talks to the MemorySource, never to the OS. It is the same decoupling as colorless memory, one level below.

This clarifies Zig’s allocators, which mix two layers in a single interface: the PageAllocator (asks the OS for pages) is a MemorySource; the FixedBuffer/Stack and the GeneralPurpose (heap) are MemoryManager; the heap, in fact, is a Manager that underneath asks pages from a Source. Splitting it into two is what gives the clean multi-target shipping: the Manager does not change between targets; only the Source swaps.

Honest boundary: not every strategy asks the Source. A Manager can be initialized over a buffer that already exists (on the stack, or a static array) and never touch the MemorySource, an arena over pre-existing memory. The MemorySource is the default source (where pages come from when the strategy needs more), not an obligation.

Shipping: dead-MM elimination

If no allocation in the program uses @mm(gc), the entire collector should not go into the binary. Same for arena, same for each strategy. This is tree-shaking of the MM strategy, and it falls almost for free out of the design: since each MemoryManager is an interface implementation and the set of used strategies is known at compile time (just scan the @mm(...) and the Arena.new()/GC.new() of the code), what does not appear does not link. It is ordinary dead-code elimination, over implementations of an interface, via the conditional compilation of comptime (section 10).

Strategy at compile-time, instance at runtime

The strategy (which MemoryManager) is always decided at compile time; the instance is free at runtime. Three levels, from the allowed to the barred:

• Level 0, instances at runtime (allowed, already comes for free). Creating a new arena per request and discarding it at the end is trivial, because MemoryManager is an interface. The strategy (arena) is fixed; the instance is runtime. The common, anonymous form: @mm(arena)’s argument is always a strategy keyword (gc/arena/none), compile-time-known, and a @mm(arena) { ... } block scopes a fresh, anonymous arena that is born at the { and dies at the }. You do not name or pass an allocator value (that would break colorless, see below); the region’s lifetime is the block. A sub-arena is just a nested @mm(arena) { ... }.

  fn handle(req: Request) {
      @mm(arena) { ... }      // a fresh anonymous arena; everything here allocates in it; it dies at the end
  }

• Level 1, strategy as a runtime variable (barred). Choosing which strategy via a runtime value (mm := x ? Arena.new() : GC.new()) makes mm an interface value dispatched by vtable: every allocation becomes an indirect call, and the compiler can no longer do dead-MM elimination, because any strategy could be chosen too late for the scan. Level 1 and runtime-strategy-swap are mutually exclusive.
• Level 2, loading an MM from a plugin/dlopen (barred). The compiler does not even know which strategies exist; it kills level 1 and opens ABI incompatibility. No upside, even more so on a bare-metal target.

The case that seems to ask for Level 1 is almost always two paths with fixed strategies, which preserves dead-MM elimination:

if config.low_latency {
    @mm(arena) serve()     // the compiler sees arena AND gc in the code →
} else {                   // it embeds both, but KNOWS which (if 'none' never
    @mm(gc) serve()        // appears, 'none' does not go)
}

The if chooses the path, not the abstract strategy. It gives runtime flexibility without blinding the compiler.

Freeing memory: free(p) and the mm module, anchored on a pointer

Under gc you never free: the runtime does it, automatically, on scope exit (obj.mm.free(ptr)), and the collector never frees anything a live pointer still reaches. Under arena, freeing is bulk and mostly runtime-managed (the region dies with its @mm(arena) { } block). The one place you free by hand is @mm(none) (manual, C-style): there, free(p) releases the object p points to. You write only the pointer; the compiler fills the size (free(ptr, size_of[T]()) when static, free(ptr, none) when dynamic, see the interface above), so there is no manual size to pass. free routes through the object’s own mm (colorless: the allocator travels with the object), so free(p) always frees with the right strategy without you naming it. And because it routes through the strategy, an explicit free(p) under @mm(gc) is a silent no-op — not an error: the collector owns reclamation, so the call simply does nothing. This is the colorless promise made concrete — the same code (with its explicit frees) compiles and runs unchanged under manual, arena or GC; switching strategy never forces you to add or remove a free. The manual free is meaningful under none, bulk under arena, and inert under gc, all from one written form.

The rarer whole-region operations (release a region early, reset it, query its usage) live in the mm module and are anchored on a pointer, never on an ambient “current arena” handle:

use mm

@mm(arena) {
    p := &node.val
    // ...
    mm.release(p)     // free the whole region p lives in (its arena), early
    mm.reset(p)       // empty p's region but keep the arena
    n := mm.used(p)   // bytes used in p's region
}

“p’s region” is the innermost arena p was allocated in: its block’s, its function call’s or its object’s — a nested @mm(arena) { } is a separate region, untouched by a reset of the outer one. For a pointer with no arena region (an @mm(none) allocation, or a process whose whole strategy is arena), the region is the process’s own memory: mm.release(p) frees that one allocation, mm.reset(p) empties the process’s manual memory. Every pointer into a reset or released region dangles exactly as after free (the compiler reports a later use in the local scope); naming the region again through such a pointer (mm.used(p), another mm.reset(p)) is fine — it reads the region, not the freed cells.

The design is deliberate on two points. There is no ambient handle (self, @mm.free(), a “current arena” accessor): every operation is anchored on a concrete pointer you already hold, so the answer to “which region, and where does it come from?” is always “the object p points to”, never a value that magically appears. There is no allocator-as-a-value passed to functions (the Zig pattern), because that breaks colorless (a function would come to know which memory it uses, and passing an arena buffer to a GC function becomes a mismatch, see the rationale). If you genuinely need to hold a region as a named value (rare, orchestrating memory yourself), Arena.new() is the explicit escape-hatch: you created it with your own hands, so there is nothing magical about where it came from.

Freeing a region (mm.release, or an arena block ending) while a live pointer into it survives is the use-after-free case above: the compiler catches it in the local scope (courtesy), and the general escaping case inherits arena/none’s unsafe semantics.

Wasm GC: alternative backing for gc (--gc=wasmgc)

Wasm GC (part of WebAssembly 3.0, a W3C standard since 2025) lets a module use the host’s collector instead of embedding its own: smaller bundle, without the double-GC that leaks. But it is not a MemorySource: it does not deliver raw bytes, but rather typed managed objects that the host tracks and moves (struct/array heap types). It is a third thing, a heap of host objects, and that is why it enters as the alternative backing of the gc strategy, not as a memory source.

The gc strategy now has two lowerings:

@mm(gc)          ┌─ default (every target):  your collector ──> MemorySource
   "managed" ────┤─ --gc=wasmgc (opt-in): host heap  (no MemorySource)
                 └─   except objects with & → demote to linear (your collector)
@mm(arena/none) ─► always MemorySource (linear), every target

--gc=wasmgc is opt-in. Without it, even on the web gc is your collector over linear memory, uniform with native, and a pointer in a gc object works normally. With it, @mm(gc) lowers to Wasm GC.

Why this does not change any user code: @mm(gc) always meant “managed”, not “my collector”. And what Wasm GC needs to track (the objects’ type structure) is what the type system already has; lowering is emitting the structs as heap types and letting the host collect. The trace of the MemoryManager interface becomes relative to the target: on native it drives your collector; on Wasm GC it is subsumed by the emitted type structure.

A pointer in a @mm(gc) object under --gc=wasmgc: demotes to linear. Wasm GC gives opaque managed references, not addresses, and the host can move the object, so you cannot take a raw *T into it (the pointer rule of section 6 needs an addressable place). Instead of forbidding it, the object from which & is taken falls to linear memory (it goes back to being your-collector-over-linear only for that object). Consequence: --gc=wasmgc never changes the semantics, only the backing; the same source compiles and runs with or without the flag. The demotion is static and diagnosable: the compiler knows which @mm(gc) become a pointer and can point at the guilty &. The bundle gain scales with pointer-purity: zero & in gc objects zero embedded collector.

Support and fallback. --gc=wasmgc produces a module that requires an engine with Wasm GC, a per-build choice, not a double bundle that decides at load. For old Safari or a server runtime without GC, do not pass the flag: the linear build runs everywhere. Wasm GC is in modern browsers (Chrome 119, Firefox 120, Safari 18.2) but still maturing, so the two lowerings stay in the box, and the compiler requires the right engine according to the flag.

How the collector finds its roots: shadow stack, stackmaps, and the hybrid

A precise collector has to know, at a collection, exactly which live pointers a running process holds — its roots — so it marks what they reach and sweeps the rest. There are two honest ways to find them, and the language ships both plus their union, selected with --gc-roots. The choice is a cost/coverage trade the collector’s precision never bends on: whatever the mode, a live object is never swept and a dead pointer is never followed.

• Shadow stack (--gc-roots=shadow, the default). The compiler roots every gc pointer explicitly: each function, at entry, pushes a small frame onto a per-process linked list — one slot per gc-pointer local — and pops it on return. At a collection the collector walks that list and marks *slot for every slot. It is portable (no target-specific stack unwinding), works on every backend including wasm, and roots memory pointers as naturally as register ones — a gc pointer living in an aggregate on the stack is just another slot. Its cost is the push/pop and the slot stores, paid on every call whether or not a collection ever happens.
• Stackmaps (--gc-roots=stackmaps, host-only). Instead of the program bookkeeping its own roots, the backend records where the gc pointers live at each safepoint (LLVM’s statepoint/.llvm_stackmaps), and at a collection the runtime walks the native stack (DWARF CFI) to read them. Nothing is pushed or popped on the hot path — the roots are recovered only when a collection actually runs — so call-heavy code that rarely collects pays less. The price is that it needs the gc pointers to be promoted to SSA values the statepoint can capture (sroa+mem2reg), which the language’s no &local rule makes true for ordinary scalar locals, and it needs real stack unwinding, so it is host-only for now (the linear-memory wasm target keeps the shadow stack).
• The hybrid (what --gc-roots=stackmaps actually runs). A gc pointer nested inside an aggregate passed by value stays in memory at the callee (the ABI hands it as a by-pointer/byval), invisible to the stackmap. So stackmaps mode is not sole-source: it takes the union of two complementary root sets — the promoted scalar roots from the .llvm_stackmaps walk, and the residual nested-in-aggregate roots (plus every @pin) from a slimmed shadow stack that roots only those. Neither alone is complete; together they cover the whole live set with no residual, so there is no program the mode has to refuse.

The default is the shadow stack because it is the one that works on every target with no unwinding machinery; stackmaps is the opt-in for host builds that want the calls cheaper. Both are precise; they differ only in where the bookkeeping lives (in the program vs in the backend’s metadata) and when it is paid (every call vs only at a collection).

Mark-sweep and the moving collector (--gc-collector)

The default collector is mark-sweep: it marks the live set from the roots and reclaims the rest in place, never moving an object, so a raw *T into a gc object stays valid across a collection (the pointer rule of section 6 holds for free). The opt-in moving/compacting collector (--gc-collector=moving) slides the survivors of each size class together to cut fragmentation and speed bump-allocation, at the cost of having to fix up every pointer to a moved object — which the same compiler-derived trace provides (a mirror trace that rewrites field addresses), and which the root machinery rewrites for the roots. An object that C holds by raw pointer, or that must not move for any reason, is marked @pin (section 23): the collector excludes its span from compaction, so its address is stable while the pin is held. Moving pairs with the shadow stack (it fixes up shadow slots directly); combining it with sole-source stackmaps is refused at compile time, because a statepoint’s gc.relocate would hand back the un-relocated pointer.

unsafe, union and the containment of danger

The core of the language is safe. But there exists a small family of escape-hatches (raw pointer of section 6, FFI with C, manual free of arena/none, and union of byte reinterpretation) where the compiler’s guarantees have to be suspended. Instead of a loose rule per case, all of them share one mark, unsafe, and a single model of containment.

union: byte reinterpretation

enum and union solve different things, they are not two flavors of the same. enum is “one of N variants, and the program knows which” (tagged, safe; section 2). union is “the same bytes read in N ways, and you know which” (untagged, unsafe). union is not an “unsafe enum”: it is a memory reinterpretation tool, for FFI (a C struct that is a union) and bit-tricks (reading a float as its bits).

The syntax reuses the field form (the product’s) as a mold, with overlap semantics:

unsafe union FloatBits {
    f: f32
    bits: u32
}

In a product, the fields are side by side (size = sum). In a union, they are overlapped: size = that of the largest field, and all start at the same address. Field access (read or write) is unsafe; writing one field and reading another reinterprets the bytes, and the reinterpreting read carries the assume that documents the intent (see “Containment”, below). Like every binding, a union is born with a value (there is no uninitialized var x: FloatBits): you construct it by writing one field, and reading a different field is the reinterpretation:

x := unsafe FloatBits{ f: 1.5 } assume "writes the float field"        // born with ONE field written: 4 bytes as a float
y := unsafe x.bits assume "intentional reinterpretation float→bits"   // reads the SAME 4 bytes as u32 → the IEEE pattern of 1.5

Every byte of a union is defined. Construction writes the given field at offset 0 and zeroes the bytes that field does not cover, so reading a wider field afterwards reinterprets the written bytes plus zeros: U{ b: 1 } (a u8 field) read through a u64 field is 1, at every optimization level, on every target and in the interpreter, never whatever the stack held before. With every binding born with a value and mm.alloc handing out zeroed memory, this closes the last way memory Makoto owns could be read uninitialized. It is the default and has no switch. The cost is one store of zeros over the uncovered bytes, at construction only, which the optimizer removes when those bytes are overwritten or never read; constructing through the widest field leaves nothing uncovered and costs nothing extra, which is the form to use in a hot loop. Writing a field later replaces only the bytes that field covers and keeps the rest. The byte layout is the one every supported target shares: little-endian, every field at offset 0, an integer of N bits occupying ⌈N/8⌉ bytes (zero above bit N), a float its IEEE-754 image (f16, bf16, f32, f64, f128, f256). Memory obtained from C is outside this guarantee: it holds whatever C’s allocator returned (section 17).

What makes it dangerous: there is no discriminant. The union does not keep “which field is active”. Writing f and reading bits is intentional (it is the point). But writing f and reading a field ptr: *Node that is also in the union fabricates a pointer from float bits: garbage, probable crash. The compiler does not prevent it, because it does not know which field is active. That is exactly why it is unsafe.

“What if the union knew the active field?” Then you reinvented enum. Carrying “which field is active” across boundaries and over time requires a discriminant, and union-with-discriminant is the definition of enum. You would pay the memory cost of the tag and the runtime cost of the check, losing the only two things that justify union (zero memory overhead, zero check). The choice “do I want to track the active field?” already has an answer: it is called enum. It is not a third construct: it is union (raw, you take care) vs enum (tagged, safe), the same duality of @mm(none) vs gc.

unsafe: composable modifier

unsafe is a first-class citizen: a modifier that composes in front of a block, an expression, a fn and a union, just as comptime/pub/@generator compose (Principle 3, section 14):

unsafe expr             // single operation (unsafe x.bits, unsafe raw_read(p))
unsafe { ...several... }  // block for a group of operations
unsafe fn risky() {}     // the whole function is an unsafe context, and signals the caller
unsafe union Bits {}     // marked declaration

unsafe expr for one operation, unsafe { } for a group: the same short-form/block logic of loop/match. It is the single place where the guarantees are suspended: raw pointer deref, union access, FFI, and the manual free of an arena with a live pointer (the unsafe case of @promote, above). One concept that ties the whole escape-hatch family together.

Boundary contract: @requires and the post-condition (design by contract)

The containment of danger happens at two levels: the contract at the function boundary, which makes the function safe to call, and the killing of the operation in the body (next subsection). The first is design-by-contract, and it is the layer that builds safe abstractions over unsafe primitives.

@requires(cond) declares a pre-condition on the function. It is a directive (@ sigil, like @mm/@promote), not a keyword: a contract configures the compiler, so it fits the sigil, at the cost of zero new keyword. The compiler enforces it at each call: proves statically where it can (zero cost) and inserts a runtime check with a deterministic panic where it cannot. Multiple pre-conditions stack, one per line, and the compiler tells you which one failed, better than a &&:

@requires(i < buf.len)
@requires(buf.len > 0)
fn at(buf: Buffer, i: usize) -> u8 { ... }

b := at(buf, 3)    // the compiler checks both conditions HERE, at the call

The central point: a checkable pre-condition, declared as a contract and enforced by the compiler, makes the function safe, not unsafe. The caller does not re-declare the condition (the contract is checked automatically), and at is fn, not unsafe fn. A function is safe iff every pre-condition is (a) checkable-and-contracted via @requires, or (b) guaranteed by a type invariant. If there is leftover an inexpressible residue (case B, raw pointer validity, FFI liveness), the function stays unsafe fn, and that residue is killed in the body or passed along.

The post-condition (the contract’s ensures) has two equivalent forms; you choose the one that reads better:

• In the return type (terse): the condition references the return by the type itself, and it is the form for the single return (-> u8 == buf.bytes[i]); multiple conditions over this return separate by ,. Multi-return uses the directive (below); the terse one does not try to squeeze it into the signature.
• @ensures(cond) directive (explicit): outside the signature, and the natural way with many conditions or many returns. Stacks just like @requires (one per line, and the compiler tells which failed).

In both, the return is referenced by the type (the type is the slot), which is enough as long as each return type is unique. When a type repeats (-> (u8, u8)) and there is an @ensures talking about it, the type stops disambiguating; then, and only then, the return gets a name:

// terse, type as slot (no name, the common case):
@requires(i < buf.len)
fn at(buf: Buffer, i: usize) -> u8 == buf.bytes[i]
{ return buf.bytes[i] }

// directive, stacking (distinct types, no name):
@requires(i < buf.len)
@ensures(u8 > 0)               // condition over the return 'u8'
@ensures(Node.count > 0)       // condition over the other return, 'Node'
fn lookup(...) -> (u8, Node) { ... }

// type collision WITH contract → named return (mandatory only here):
@ensures(lo > 0)
@ensures(lo < 100)             // multiple conditions for the same return = multiple lines
@ensures(hi > 50)
fn split(...) -> (lo: u8, hi: u8)
{ return (a, b) }              // 'lo'/'hi' are slot labels, not variables: the return is free

A named return is a contract label, not a variable (Model 1). The name points the slot out so the @ensures can talk about it; it does not create a variable in the body, and the return stays free (return (a, b), any expression; the compiler matches by position). It is optional in the terse form (use it if you want to be explicit) and mandatory only in the type-collision-with-contract case above. Whoever does not fall into that case never writes a return name: it does not leak (opt-in test, section 1).

The two forms are distinct constructs and do not combine into one signature: the terse inline comparison lives in the return type (-> u8 == expr), while a named return introduces a labelled slot that an @ensures directive then talks about. Writing the terse comparison directly onto a named return (fn f(...) -> (r: int) > 0) is not accepted by design — the name and the directive go together, the type-slot and the inline comparison go together. Terse exists to be concise for the single, uniquely-typed return; the moment you need a name (type collision) you are in the directive world, and the condition moves to @ensures.

Checked at each return, static where it proves, runtime panic where it does not. Contract reuse comes for free: the condition is a boolean expression, and a function call is a boolean expression, so a reusable predicate is an ordinary boolean function (@requires(in_bounds(i, buf.len))), with no new construct. There is no dedicated contract: it would not pass the opt-in test (section 1), because every reader would have to learn it for the rare gain of naming a contract, while the boolean function does the same with pieces that already exist.

And this does not contradict “assert never in the header” (next subsection): @requires/post-condition are contracts, which live in the signature in every language with DbC (Eiffel, Ada, Dafny); assert is the killing of an operation, which lives in the body. They are different levels (boundary vs operation), and that is why the @requires at the call subsumes the assert (cond) that the caller would have to write: the contract was already checked at the boundary. Honesty: safety post-conditions are sometimes inexpressible case-B (Rust’s as_bytes_mut, “the caller has to keep the slice valid afterward”); those fall to assume. The checkable post-condition is for the bulk (result in range, non-null, ordered).

Containment: every danger is killed or passed along, explicitly

unsafe is not a region of permission where danger is free and silent (the Rust model). It is an obligation to handle, analogous to catch: you cannot just do the dangerous operation and carry on as if nothing happened; you have to declare how the danger was neutralized, or pass it along explicitly. The danger stops being “allowed in a region” and becomes “a debt someone pays”. It is Principle 1 (danger is always marked) taken to the extreme: it is not enough to mark that it is dangerous, you show the kill.

Every unsafe operation requires a handler, and there are three:

Handler	When	Semantics
assert (cond)	there is a checkable pre-condition (valid pointer, index in range)	strong (default): runtime checks; if false panic, not UB. It is the same deal as or_panic: trades undefined behavior for clean failure.
assume "reason"	the danger is intentional and non-checkable (reinterpret bytes)	trusts (fallback): no check, no UB; you take the responsibility. “Safe for this reason; trust me.”
pass along	you do not kill it	the function becomes unsafe fn; the caller handles it.

They are two keywords, one intent each: assert (cond) checks (runtime verifies, panic if false); assume "reason" trusts (no check, and never licenses UB, the compiler does not optimize on top of the assertion, you just take the responsibility). The separation is deliberate: a single keyword, sometimes checking and sometimes not, would blur the most important line of unsafe, “the compiler guarantees” vs “it is a human promise”. The keyword shouts which of the two it is, instead of the reader noticing paren-vs-quotes. (assert is the common case, checkable; assume is the fallback, for what cannot be checked.)

// STRONG (default): assert + condition → runtime checks, panic if false
b := unsafe raw_read(buf.ptr + i) assert (i < buf.len)

// TRUSTS (fallback): assume + textual reason → you take it on, no check
y := unsafe x.bits assume "intentional reinterpretation float→bits"

assert (and its pair assume) mirror catch visually (they are trailers of the operation), but they have their own semantics and do not reuse catch: catch is reactive, it handles an error value that already happened (|e| is the concrete error, you inspect and react). assert is preventive, the pre-condition is checked before, and the danger never becomes a value. They are opposite tenses; fusing the two would blur the difference, and there is no “unsafe error” to discard with |_|. Same structural look (trailer = “handles what the operation above raises”), distinct concepts.

The assume shrinks to the irreducible, and that is what stops it from becoming a decorative assume "". The reason has to be non-empty and meaningful (assume "" is an error). Where a check exists, it is assert’s job: checkable bounds and validity become @requires/assert (cond). A same-width reinterpretation (fbits, both 4-byte scalars) is the classic assume, and the compiler accepts it: the widths line up, but whether the reinterpreted value is meaningful is a human judgment. Fiddling with a float’s bits in a way that leaves the IEEE layout and then reading the float back can produce a value the rest of the program does not survive, and no width check sees that. When a comptime predicate can prove the property you rely on (below), the assert path is open too; it adds a checked route, it does not take the assume away. What is left for assume is the genuinely opaque (the intent of a reinterpretation, pointer provenance, FFI liveness), where there is no operation to check, or the check would not capture the intent. You cannot force a check where there is none: that is the boundary of unsafe. What remains is the audit surface, the small, indexable and non-empty set of “here safety rests on human judgment”, where review focuses.

The reason is a compile-time artifact, so it may be any value the compiler can render at compile time — not only a string literal. A const reason reused across sites, a comptime fn that builds the string from the type it is discharging, an enum or error constant with a Display: the compiler folds each to its text where the assume is written, exactly as if you had typed the literal there. That keeps the audit surface intact — the review tool resolves the reason statically and a grep still lands on a readable string — while letting a project name its recurring justifications once. What it refuses is a runtime value (a var, a computed error): assume performs no runtime check, so a reason it could only learn at run time has nowhere to be used and, worse, cannot be read off the source, which defeats the whole point. The rule is one line: the reason must be comptime-known. (This composes with the comptime contracts of section 14 — the same comptime fn that proves a predicate can also name the reason.) When you want a failure payload rather than a static reason — return a specific error if a condition does not hold — that is not the assume; it is the ordinary assert (cond) else return MyError: the check exists, so it is assert’s job, and the error rides the normal return (there is no raise keyword; the error path is a value like any other).

Comptime predicates: proving a contract at compile time

A contract predicate is “an ordinary function” (above) — and a function can be a comptime fn (section 10). Allowing one in @requires, the post-condition, assert, and assume is the natural next step, and it changes when the contract is decided. comptime runs in the compiler’s own interpreter, so a comptime predicate can carry logic richer than a flat boolean chain — inspect a type via reflect(T), compute over constants, check a layout invariant — and the compiler evaluates it during compilation:

comptime fn is_ieee_reinterpret[A, B]() -> bool {
    // richer than a boolean &&: reflect over both types, check the bit-widths line up, etc.
    return size_of[A]() == size_of[B]() && reflect(A).is_float && reflect(B).is_unsigned_int
}

unsafe union FloatBits { f: f32; bits: u32 }

y := unsafe x.bits assert (is_ieee_reinterpret[f32, u32]())   // PROVEN at compile time

The evaluation model is static discharge with a runtime fallback, decided by whether the predicate’s arguments are compile-time known:

• All arguments comptime-known the predicate folds at compile time. If it folds to true, the contract is discharged for free — no runtime check is emitted at all. This is what upgrades an assume into a proven assert: where you used to write assume "float→bits" (a human promise, part of the audit surface), you now write assert (is_ieee_reinterpret[f32, u32]()) and the compiler verifies the promise, moving that line out of the audit surface entirely. If it folds to false, it is a compile error — the contract is provably violated, caught before the program runs.
• Some argument is a runtime value the predicate lowers to a runtime check, exactly like an ordinary assert (cond): verified at the point, panic if false. The comptime body still gives you the richer logic; only its inputs being runtime pushes the verdict to runtime. (This falls out naturally: a comptime fn folds when its inputs are constant and runs as ordinary code when they are not.)

The return is a bool, or a value the compiler reduces to one at compile time by a defined, two-valued rule: an Optional (some true, none false, the presence rule) or a Result (Ok true, Err false, the success rule). This is not runtime truthiness — the language has none, and if/assert still take a strict bool (section 14) — it is a constant reduction of a comptime-folded verdict: the predicate ran in the compiler and produced a concrete some/none/Ok/Err, which is unambiguously a yes or a no. A three-valued result is deliberately not reducible: Ordering (Less/Equal/Greater) and the ball’s Indeterminate (section 14) have no single “true” case, so a predicate that wants to compare returns the bool of the comparison (a.cmp(b) == Equal), never a raw Ordering — a contract is a yes/no, and smuggling a maybe into it is the three-valued-boolean the language rejects on purpose. On the runtime-fallback path the predicate must be a plain bool (there is no compile-time constant to reduce, and no runtime truthiness to lean on).

This keeps the audit surface shrinking in the right direction: every assume that a comptime predicate can prove becomes an assert the compiler checks, so what is left in assume is only the genuinely unprovable — pointer provenance, FFI liveness — which no amount of compile-time evaluation can reach.

assert/assume live in the operation, never in the header

assert does not go in the function signature. The other modifiers (pub/unsafe/comptime) are simple declarations, one word that flips a bit. assert (cond) carries an expression, containment logic. Putting it in the header would mix the signature (the type contract) with the implementation (the checked condition), a layer break that the others do not commit. And there is a deeper incoherence: the containment happens inside the body, where the unsafe operation is killed, not at the boundary. Putting assert in the header would be announcing at the door something that happens in the kitchen.

So: containment is a property that emerges from the body, not a mark of the signature. A function is unsafe fn (passes along) or a normal fn (safe), and its being safe despite containing unsafe operations is a consequence of having killed all the unsafe operations in the body with assert/assume, not of a word in the header:

// SAFE: no 'unsafe' in the header. It is safe because it killed the danger in the BODY.
fn read_at(buf: Buffer, i: usize) -> u8 {
    return unsafe raw_read(buf.ptr + i) assert (i < buf.len)   // containment HERE
}
read_at(b, 3)        // caller does not see unsafe

// UNSAFE: passes along. Has 'unsafe' in the header because it did NOT kill it, let it rise.
unsafe fn raw_at(buf: Buffer, i: usize) -> u8 {
    return unsafe raw_read(buf.ptr + i)   // no handler → danger rises → unsafe header
}
_ := unsafe raw_at(b, 3) assert (3 < b.len) // discards the u8 with '_'; kills at the call site

The compiler’s rule: if the body has an unsafe operation without assert, the function requires unsafe fn in the header (or it is an error). If all were killed with assert/assume, the function is a normal fn. The unsafe fn is not “one more color that you choose”: it is the forced consequence of leaving unkilled danger in the body. You do not decide to put it; the compiler requires it.

This collapses the apparent explosion of “function types”. The real modifiers are four orthogonal bits, each a simple word, and assert/assume are not among them:

pub?  comptime?  @generator?  unsafe?   fn

pub unsafe fn is not a new kind of function: it is fn with the subset of marks turned on, the cartesian product of orthogonals (Principle 3), not coloring. And assert/assume appear in two places, both “operation”, never “signature”: killing an intrinsic operation (unsafe x.bits assume "...") or a call to an unsafe fn (unsafe raw_at(b, 3) assert (3 < b.len)). Zero header involved.

The unsafe block: scope, values and multiple asserts

unsafe { } is not a region of permission (Rust): it is an expression-scope that groups operations, and each dangerous operation inside it is killed individually. This answers a handful of questions that look separate but have the same root: where the assert is determines what it can talk about.

The block reads variables from the outside (normal lexical scope; passing values in is just referencing them, there is no isolated sandbox) and returning a value out is by explicit return, never implicit (a block without return is worth nothing); since the unsafe {} here is in an expression position (result := unsafe {...}), the return delivers the value to whoever receives it, instead of leaving the function. Each unsafe operation carries its own assert, and there are multiple asserts per block: one per operation, or one shared trailer for operations that share the same pre-condition:

result := unsafe {
    a := raw_read(p)         assert (p_valid)       // pre-condition of THIS read
    base := a * stride                               // variable created INSIDE the block
    b := raw_read(q + base)  assert (base < len)     // later assert sees 'base'
    return a + b                                     // value goes out by return (expression → goes to 'result')
}

The rule that ties everything: an assert is the pre-condition of the operation it kills, checked before it. Hence three consequences:

• A variable created inside the block can be talked about by an assert that comes after it (it already exists, it is the case of base above), but not by the entry trailer (unsafe { … } assert (c)), which is the entry pre-condition, checked before the block, when what is inside has not yet been born.
• The values that enter an operation are the subject of its assert. Its result, no: the assert runs before, so it does not talk about its own return. A guarantee about a result is a post-condition, not an assert: the assert covers the input (before), the post-condition covers the return (after), the two tenses an operation has.
• The shared trailer (unsafe { … } assert (c)) is the entry pre-condition valid for all operations in the block, and it coexists with pointwise asserts where one operation’s pre-condition differs from the rest.

Why unsafe is the only coloring the language accepts

The contagion of unsafe (“calling unsafe fn requires an unsafe context”) is coloring, with the same structure as async infecting the call stack: the property rises up the call tree. Denying it would be dishonest. The right question is not “how do I avoid it?”, but rather “why do we kill the coloring of async/MM but accept (even want) that of unsafe?”. The answer is a distinction that separates good coloring from bad:

Implementation coloring (noise, kill it) vs. contract coloring (safety information, preserve it).

• async colors how the function runs underneath (suspends or not). It is an implementation detail: you should not have to know whether a read_file uses epoll. The color leaks internals and forces you to propagate it.
• MM colors which strategy manages the memory. Again, implementation: the consumer should not care whether an object is arena or GC.
• unsafe colors that the function has pre-conditions the compiler does not verify and that you are obligated to guarantee by hand. This is not implementation, it is the contract. deref of a raw pointer gives you use-after-free if you do not guarantee validity, and only you, in your context, can guarantee it. The color is not a detail that leaks; it is an obligation that has to reach you, otherwise you take on a risk without knowing. Suppressing the contagion would not remove noise; it would hide danger. It would be like removing the “fragile” warning from the box because the label is annoying.

And there is the decisive operational difference: async is uncontainable (it rises to main, with no stop button); unsafe is containable. Any function that fulfills the pre-conditions absorbs the danger and stops the propagation right there, exposing a safe interface on top, which is exactly what read_at does above (kills with assert, and is itself a safe fn). The contagion rises only up to the first layer that encapsulates the danger safely, normally quite deep (the bit-trick function, the one that talks to C). In practice, unsafe lives on small islands with safe boundaries, not on a whole painted call stack. It is Principle 1 operating transitively, with a point of containment where someone proves the pre-conditions hold, and that “containment point” is the key concept.

union and the GC

A union with a pointer field is opaque to the GC. The derived trace (above) works because the compiler knows which fields are pointers and visits them; in a union, it does not know whether the pointer field is active, it may be overlapped with float bits. If the GC traced that field, it would read float-bits as a pointer collector corruption. The rule:

union without pointers (pure scalars, f/bits) trivially traceable (the derived trace is “visit nothing”), fine in any MM. union with a pointer out of the GC: it has to live in @mm(none)/arena, and the pointers inside are your responsibility. Compile error if allocated under @mm(gc).

The justification is surgical: knowing the active field is possible locally (flow analysis, at compile time; the compiler tracks “which was the last write” inside a linear unsafe, the same analysis as the never-mutated var and the @transfer, and can warn “you wrote f and read ptr, are you sure?”) but impossible globally (heap, runtime; depends on a write in another scope/instant). The GC operates always in the global case (it traces the heap much later, without the context of the last write). So flow knowledge improves the local diagnostics, not the traceability; the GC boundary holds. Locally clever, globally cautious.