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)

// 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

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. 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 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

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

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

There is no @shared. Every use case that shared memory would solve is addressable via @transfer + channel, with more clarity and without opening a vector of cross-corruption between heaps. If multiple processes need access to the same data, the pattern is a dedicated process that holds the data and serves requests via channel.

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

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
}

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

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

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). More: the compiler rejects the assume where the operation is probably-safe or checkable. A same-width reinterpretation without a pointer (fbits, both 4-byte scalars) is memory-safe by construction and the compiler proves it, without requiring any assert; checkable bounds and validity become @requires/assert (cond). What is left for assume is only the genuinely opaque (pointer provenance, FFI liveness), where there is no operation to check (if there were, it would be case A). 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.