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 mica-container/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.

One rule decides whether this debt exists at all: dispose follows pointers, never values. new on any type other than a dynamic array hands you a pointer to a cell, and a pointer can be copied into any place, so no scope can know when the cell ends — that is the debt, and the four roads are the ways to settle it. new Numbers reserve n on a dynamic array hands you the array value, not a pointer, and a value has one home: it lives and dies with the variable that holds it, is deep-copied on assignment, and never meets dispose. Strings and static arrays are values in the same sense. So when you read a new, look at what it gives back: a pointer carries the debt, a value carries nothing.

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:

program H4;

imp
    WriteLn : std;
var
    p : pointer int64;

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

begin
    p := new int64;
    Touch(True);
    WriteLn("%lld", value 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, saved as H4.mica, compiles. And this is where the tiers divide:

mica --compile --link --optimize checked --source H4.mica --build build
./build/H4
Mica runtime failure: reason=use_after_dispose (11), token_stream_index=47
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.

Seeing what the program holds

The four roads decide when a cell goes back; the editor shows where each one stands while the program runs. Debug the program from the editor, stop it at a breakpoint, and run Mica: Show What the Program Holds. The Mica Runtime view’s Memory section answers in three parts: what the program holds, in one sentence in the order memory is owned (“1 region holds 1.2 KB in one 64 KB block”); its cells summed by the type they hold, each type with the line that made it; and every region block drawn as two bars, each with its caption: the block’s fill, then its used part, cell by cell. A legend says what each colour means: a value in use; released, waiting for reuse; the region’s own table of free lists. Stop in road four’s Pool after its second MakeItem, and the section shows Pool’s region holding both items, two int64 cells made at one line, until Pool returns and drains them.

A program started outside the editor answers the same readings. Start it with +mica rtp=listen -mica ahead of its arguments and run Mica: Attach to Running Program; each reading stops the program for its moment and lets it run on. The site of every cell is recorded at the debug tier, so a release build names its regions and their blocks but not the cells in them.

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 O2,checked where that class of risk is unacceptable — the guards ride the optimizing lowering, and the tested program is the shipped one.

A cell that comes to rest inside something else is followed, up to a point. Store one into a record’s field, an array’s element or a field one value record down, and the analysis hands the obligation to the container that holds it: the container’s own release walks the slot, so the cell is released with it and releasing it yourself is refused. What is left are the places with no owner to follow — an element of a plain local array written under a computed index, a pointer handed to foreign code. Those the analysis classifies honestly as manually-verified rather than proven, and a checked run reports at exit any of them that were never released.

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 borrowed 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 and borrowing — 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.