Manual memory management has one honest description: every malloc is a debt, and C makes you keep the ledger in your head. Forget an entry and you leak. Pay twice and you corrupt. Use a cell after paying and you have use-after-free — the bug class security advisories never run out of.

The industry’s escapes are famous. A garbage collector takes the ledger away — and with it, control over when. A lifetime type system makes the ledger sound — and famously steep. Mica takes a third road: the compiler keeps the ledger. Allocation stays explicit, release stays explicit, and the obligation in between is tracked through your control flow like an uninitialized variable would be. Forgetting is not a leak at run time; it is an error at compile time, and the error names the line that borrowed.

The example is examples/HeapEndToEnd. Build and run it:

make -C examples/HeapEndToEnd run

The debt, stated by its own error message

Allocate a cell and print it, releasing nothing:

p := new int64;
value p := 5;
WriteLn("%lld", value p);
obligation error 13102: heap cell is not released on every path: last use at
line 9, the path leaving at line 10 releases nothing — dispose it, defer the
dispose, return it, or bind it to an owner with 'until'

Read the end of that message again, because it is the whole article: dispose it, defer the dispose, return it, or bind it to an owner with until. Four roads. The example walks one section per road, and the compiler accepts it without a warning.

Note also what class of message this is: not analyzer error, but obligation error — a separate analysis that reads your control flow as written, path by path, and reports the allocation a failing path belongs to.

Road one: dispose it

counter := new int64;
value counter := 41;
value counter := value counter + 1;
WriteLn("  the cell held %lld", value counter);
dispose counter;
  the cell held 42

new and dispose are the explicit pair, and between them the cell is yours. The pointer mechanics are the ones you already know — value on both sides — and the straight-line shape is the one the analysis verifies most directly.

What it will not accept is the pair in the wrong order. Use after the release:

obligation error 13105: heap cell is dereferenced after it was already
released on every path reaching here — the cell allocated at line 7 is used
after its dispose; move the use before the release

Release twice:

obligation error 13104: heap cell is disposed again after it was already
released on every path reaching here — remove the repeated dispose of the
cell allocated at line 5

Use-after-free and double-free — the two memory bugs with their own CWE numbers — are compile-time reports here, each pointing at the allocation it indicts and at the move that fixes it.

Road two: defer the dispose

Straight lines are rare. Bodies branch, and every branch is a path the release must cover:

function Classify(limit : int64) : int64;
var
    scratch : pointer int64;
begin
    scratch := new int64;
    defer dispose scratch;

    value scratch := limit * 10;

    if value scratch > 100 then
    begin
        Classify := 1;
        leave;
    end;

    Classify := 0;
end;
  Classify(5) = 0
  Classify(50) = 1

One defer dispose at the top holds for every exit — the early leave and the fall-through release the same cell exactly once, and neither path can forget, because neither path carries the release. This is the same defer that ran a generator’s cleanup and a task’s: one mechanism, and the obligation analysis knows it discharges the debt.

Road three: return it

A builder that must hand its cell to the caller does not “escape the analysis” — it transfers the obligation, visibly, through the type:

function MakeNode(w : int64, l : int64) : pointer Node;
var
    n : pointer Node;
begin
    n := new Node;
    n.weight := w;
    n.tag := l;
    MakeNode := n;
end;
settings := MakeNode(70, 7);
total := settings.weight + settings.tag;
WriteLn("  made a node, weight+tag = %lld", total);
dispose settings;
  made a node, weight+tag = 77

The return moves the debt: MakeNode now owes nothing, and the caller owes a dispose. Delete the caller’s dispose settings and the 13102 report appears — at the caller’s exit, because that is where the unpaid debt now lives. A function whose result is an owning pointer is handing over an obligation, and its signature says so.

Road four: bind it to an owner

The deepest road, and the one that scales. Sometimes the maker of a value is not its natural owner — a helper builds items for a pool, and the pool should own them:

procedure Pool();
var
    a, b, made : pointer int64;

    procedure MakeItem(v : int64);
    begin
        made := new int64 until Pool;
        value made := v;
    end;

begin
    MakeItem(10);
    a := made;
    MakeItem(20);
    b := made;

    WriteLn("  pool total: %lld", value a + value b);
    WriteLn("  pool ends; its items drain here, unwritten");
end;
  pool total: 30
  pool ends; its items drain here, unwritten
  back from the pool

until Pool binds each allocation’s lifetime to the named enclosing activation. The items are fully owned the moment they are made — however deep the call that made them — and they drain, wholesale, when Pool exits. No list of things to free, no cleanup loop: the activation is the owner, and its exit is the release.

You have seen this shape twice already. It is the arena’s activation reclaim with a named owner instead of the implicit one, and until program — the pool called program — is where the previous article’s pinned value came from. One mechanism, three spellings, and the obligation analysis reads all three.

The honest backstop: the checked tier

Every proof has a boundary, and Mica states its own. Hide the release behind a value no analysis can know:

procedure Touch(release : bool);
begin
    if release then
        dispose p;
end;

Now Touch(True) followed by a read of p is a use-after-dispose the compiler cannot prove — the flag is runtime data. The program compiles. And this is where the tiers divide:

mica --optimize checked ...
Mica runtime failure: reason=use_after_dispose (11)
Mica runtime context: file=H4.mica, line=17, column=27
Mica runtime source:     WriteLn("%lld", value p);

Under --optimize checked, every release poisons the cell’s header, and every dereference tests for the poison — so the read that slipped past the proof is caught at run time, at its exact line, instead of returning stale bytes that propagate silently. The analysis proves what is provable; the checked tier guards what is not. The shape the proof cannot reach has a tier where it cannot hide.

What this does not do

Owning pointers are expected to form a tree. The drain that reclaims an owner’s cells follows owning fields leaves-first, so a genuine cycle of owners — two cells whose owning fields point at each other — is a misuse of the model. The checked tier traps it deterministically (cyclic_ownership, at the drain, naming the source position) instead of overflowing the stack; a release build keeps the lean drain and its behaviour on that misuse is undefined by design. The legal back edge inside an owned structure is an borrowed pointer, which the drain skips — that is the ownership article’s subject.

The checked guard belongs to the checked tier. A release build keeps the lean dereference, so an unproved use-after-dispose there is stale memory, exactly as the tier’s name promises nothing else. Develop and soak under checked; ship checked where that class of risk is unacceptable.

A pointer stored into long-lived shared state degrades the proof. The analysis classifies such cells honestly as manually-verified rather than proven, and the staged contract reports the ones it cannot see discharge. The four roads above are the shapes it proves outright — which is a design nudge, not a limitation you fight.

No reclaim before the owner exits. until Pool items live until Pool ends, even ones done earlier — wholesale drain is the deal. An item with a genuinely shorter life takes road one inside its own scope.

This article stopped at owning. One pointer owned each cell here; nothing was shared, borrowed, or handed out for a while. The alias forms — reading without owning, and the rules that keep a borrow from outliving its cell — are the ownership article, next in this section.

What the compiler proved

Every allocation in the example is matched — by a dispose, a defer, a transfer, or an owner — and the compiler verified all four before the program existed. The three classic heap bugs appeared in this article only as quoted refusals, each naming its allocation. And the one shape no analysis could see was caught at its line by the checked tier, loudly, on the first run.

The ledger C keeps in your head, and Rust keeps in the types, Mica keeps in the compiler — and shows you, in its own error message, exactly the four ways to balance it.

Next

Ownership, borrowing and alias — reading without owning: the borrow that cannot outlive its cell, the parameter that promises not to dispose, and the back edge that gives owned structures parents.