The heap article had one pointer per cell, and it
was always the owner. Real programs are not so tidy: a routine needs to look
at a cell it must not free, a cursor structure wants a window into data that
outlives it, a tree wants parent pointers. In C all of these are the same
T*, and the difference between “owns” and “merely sees” lives in a comment,
a naming convention, or the memory of whoever wrote it. Every double-free
starts as a disagreement about that comment.
Rust made the difference a type system, famously. Mica makes it one word:
n : pointer int64 { owns: carries the release obligation }
n : borrowed pointer int64 { borrows: uses the cell, keeps nothing }— and then checks the word.
The example is
examples/Ownership.
Build and run it:
make -C examples/Ownership runLend a cell, keep the obligation
procedure Inspect(n : borrowed pointer int64);
begin
WriteLn(" borrowed and read: %lld", value n);
end;
procedure Touch(n : borrowed pointer int64);
begin
value n := value n + 1;
end;cell := new int64;
value cell := 41;
Inspect(cell);
Touch(cell);
WriteLn(" after the borrowing write: %lld", value cell);
...
dispose cell; borrowed and read: 41
after the borrowing write: 42The caller lends with no ceremony — passing an owning pointer where a borrowed one
is expected is the lend — and the callee’s signature promises it will keep
nothing. Note what Touch did: a borrow can write. Borrowing is about
ownership, not mutation; the borrower may change the cell. What it may not do is
release it or re-home it, and those are refusals, not conventions.
Try to release:
procedure Rogue(n : borrowed pointer int64);
begin
dispose n;
end;analyzer error 5200: dispose statement cannot release a 'borrowed pointer'
value of data type 'als.ptr.int64': a borrow is owned elsewhere (a
container, the program, or another scope), which releases it — dispose the
owning pointer insteadTry to smuggle the borrow into an owning slot:
k.b := n; { k.b is a plain 'pointer int64' field }analyzer error 5199: cannot store a borrowed 'borrowed pointer' value into the
owning pointer field or element 'k': an embedded pointer is owned by
construction and its owner's drain would release the borrowed cell — mark the
field 'borrowed pointer' to borrow, or store an owned pointerThese two refusals are what make borrowed a checked claim. The
obligation ledger never has to wonder whether a
callee took the debt: the parameter type already answered, and the compiler
enforced the answer inside the callee’s own body.
A view structure holds a window, not a duty
The word works in fields too:
type
Window = record
tag : int64;
seen : borrowed pointer int64;
end;w.seen := cell;
WriteLn(" window %lld sees %lld", w.tag, value (w.seen)); window 7 sees 42A cursor, an iterator’s position, a cache entry pointing at data owned by the
store — view structures are everywhere, and this is their honest type. The
5199 message above showed the other half: the same store into a field not
marked borrowed is refused, because a record’s drain frees its owning fields
and this record does not own the cell. Which duties a structure’s death
discharges is written in its field types, one by one.
(One spelling note: dereferencing a pointer field parenthesizes — value (w.seen) — so the value binds to the field, not the record.)
The back edge: parents without a cycle of owners
Here is the payoff the heap article promised. Its rule was that owning pointers must form a tree — the drain recurses owning fields leaves-first, so a cycle of owners is a misuse. But real structures are cyclic: children point at parents, list nodes point back, graph nodes interlink. The resolution is the same one word:
type
Node = record
v : int64;
next : pointer Node; { owns downward }
parent : borrowed pointer Node; { sees upward }
end;root := new Node;
root.v := 1;
root.next := new Node;
root.next.v := 2;
root.next.parent := root;
WriteLn(" child %lld sees parent %lld", root.next.v, root.next.parent.v);
dispose root; child 2 sees parent 1
one dispose drained the chain, parents includedThe data structure is cyclic — child and parent reach each other. The
owning subgraph is a tree — only next owns. And dispose root reclaimed
the entire chain in one statement, because the typed drain follows owning
fields and skips borrowed ones: the field types told it which arrows are
ownership and which are sight.
This is the idiom that replaces both C’s “remember not to free the parent pointer” and reference counting’s cycle problem. There is nothing to remember; the type remembers.
Stack cells lend the same way
Borrowing is not a heap-only idea. The out-parameter idiom was a lend all along:
local := 5;
Bump(address local); local after Bump(address local): 15A plain pointer parameter is a borrow by construction — the callee uses the
cell and keeps nothing — and the escape rules refuse the versions that would
keep it: returning address local was already a
refusal in the first article of this section, and storing a lent pointer into
state that outlives the call is refused by the same discipline.
The same word, under tasks
You have met borrowed once before, in
data-race freedom: inside a concurrent block, a bare
address of shared state is refused, and the legal spelling is a borrow
bound inside a synchronized statement, scoped to the mark that guards it.
Same word, same meaning — a view that cannot outlive what makes it safe —
with “safe” defined by the lock there and by the owner here. The two articles
describe one design.
What this does not do
A borrow does not extend a lifetime. It is a view, not a keeper: the owner’s release is not delayed because views exist. A borrow used after its cell’s owner released it is exactly the use-after-dispose story of the heap article — refused where provable, caught by the checked tier where not.
No reference counting is happening. Nothing counts the aliases. That is why they are free, and why they cannot keep a cell alive.
A borrow cannot be laundered into an owner. Not through a field (5199), not through a dispose (5200), not through a return — the borrow rides the type through every assignment.
Sharing between tasks is not this article. A borrow crossing task boundaries answers to the synchronized rules, which are stricter: there the view is scoped to one marked statement.
What the compiler proved
Two routines used a cell they provably could not free. A structure held a window whose type said “window”, and the store that would have made it an owner was refused. A cyclic data structure drained from one dispose because its owning subgraph was a tree by declaration. And nothing on this page was a convention: every claim was a type, and every violation was quoted from a compiler that refused it.
Next
What the compiler proves about your heap — the same machinery, seen from above: the full list of heap-bug classes and, for each, whether it is refused or trapped — the claims this series has been cashing one article at a time.