Heap lifetime proven at compile time

Every allocation in a Mica program creates an obligation. Wherever the compiler can follow the pointer, it must see that obligation discharged on every path — an undischarged cell is a build error, and the build aborts before code generation rather than emitting a binary. Where the pointer escapes what the analysis can follow, the obligation passes to you: the site is reported as manually-verified and the compiler stops enforcing it.

There is no garbage collector, no borrow checker, and no lifetime annotation to write. The machinery is the same dataflow analysis the backend already runs to schedule registers, turned on lifetimes.

Three ways to discharge

An obligation is satisfied by exactly one of:

1. A dominating dispose — the release provably happens on every path.
2. Owner registration — defer dispose p, or binding the allocation to a scope with new T until F, or to the program itself.
3. Transfer by return — the function hands ownership to its caller, and the obligation moves with it.

procedure Process;
var
    buffer : pointer Record;
begin
    new buffer;
    defer dispose buffer;     { the obligation is discharged here, on every path }

    if Failed() then
        leave;                { including this one }

    Use(buffer);
end;

Remove the defer line and the leave path leaks — and the compiler says so, at compile time, naming the allocation site.

The honest half

This is the part we care most about, because it is where analyses of this kind usually become adversarial.

The obligation is attached to the allocation value, not to a variable name, and the analysis tracks which names currently carry it. Where a pointer’s flow runs past what can be followed — across a call, into an aggregate, through a cast — the compiler does not guess and does not claim a proof it does not have. The site degrades to manually-verified, and the compiler narrates: one line per allocation site, stating the lifetime class it established and the allocator it selected.

Four lifetime classes are ordered by ascending assurance, so aggregating several sites is a numeric minimum rather than a judgement call:

The result is a zero-false-demand floor. Ambiguity costs you a diagnostic, never a rejected correct program and never a demanded annotation. A borrow checker, which must be conservative in the type system, structurally cannot offer that trade.

Beneath the analysis sits a runtime floor: new never returns nil (exhaustion aborts deterministically rather than handing back a null to check), and nil-dereference guards are planted in every optimization tier. A checked build turns a residual mistake into a loud, source-located trap instead of silent corruption.

See also

• Ownership without lifetimes
• Allocator as a link decision