This is part 5 of the series. Part 4 wrote one program as one block; this part takes the same program and names its work — a function for the rule, a procedure for the table, a function for the walk, and one function that hands back two facts. The subject does not change on purpose, because the claim of this part is checkable only if nothing else moves:

Refactoring under the value rule changes nothing observable. From the second line on, this program’s output is byte-identical to part 4’s — and you will verify that with diff, not by trusting this page.

The example is examples/Procedures in the tutorial repository.

Getting the file

make -C examples/Procedures run

The output is part 4’s, except its first line says Procedures — the walk, the tally, the unwound peak, every number the same. That is the lesson, and the rest of the page is how the language keeps it true.

The example, walked

A function states the rule once

function NextStep(x : int64) : int64;
begin
    if x mod 2 = 0 then
        NextStep := x / 2
    else
        NextStep := 3 * x + 1;
end;

Part 4 spelled the halve-or-triple rule everywhere it was needed. Now it has a name, a parameter, and a result — a function answers a value, and the answer is written by assigning to the function’s own name. There is now exactly one place this arithmetic can be right or wrong, and every loop in the program steps through it.

A procedure owns its work — and its copy

procedure PrintOpening(start : int64);
var
    n : int64;
    k : int64;
begin
    n := start;
    ...

PrintOpening prints the opening table and answers nothing — that is what procedure means. Its var section declares locals that exist only while it runs. And start is a snapshot: the call PrintOpening(27) copied the value in, and nothing the procedure does to its copy can reach the caller. The first experiment below makes that visible.

Do the work, print the findings, answer the one fact

peak := WalkAndReport(27);

WalkAndReport walks the whole thing — steps, peak, the magnitude tally from part 4, printing as it goes — and returns one value: the peak, the fact the rest of the program still needs. A function answers one value; when the work produces one headline fact and a page of reporting, this split is the honest one.

Two facts, and the arrow you must write

Sometimes one computation honestly yields two facts. The unwinding of the peak produces the odd core and the halving count, and Mica’s spelling for the second result is deliberate:

function OddCore(x : int64, count : pointer int64) : int64;
...
    value count := h;
    OddCore := n;

and at the call site:

core := OddCore(peak, address halvings);

count : pointer int64 announces, in the signature, that this function writes into somebody’s variable. address halvings is the caller lending that variable, visibly, at the call. Inside, value count := h writes through the lent arrow. Three spellings — pointer in the type, address at the call, value at the touch — and all three are readable exactly where a reader would look. No call in Mica can change your variable without your address on it.

const: the promise of a read-only parameter

Between the plain snapshot and the lent pointer stands a third mode, and it is a promise rather than a mechanism: const on a parameter says this callee only reads.

function SumOf(const x : Big) : int64;

Any assignment to a const parameter is refused where it stands:

analyzer error 5146: left side of an assignment cannot be a constant
parameter: 'x' with passing mode 'by_constant_address'

The mode named in that refusal is the compiler keeping the copy cost off a promise the caller already made. A small value under const travels exactly as the snapshot does — read-only, mechanism unchanged. A plain aggregate larger than the two-register line (16 bytes) travels as one constant address into the caller’s own storage: no copy is made, because a callee that provably cannot write needs none, and nothing changes at the call site — the argument is spelled the same, and no address appears, because nothing is being lent for writing.

So the guidance is one sentence: write const on any parameter the body only reads — it documents the intent, the compiler enforces it, and for a large record or a big tensor it also makes the call cost one address instead of a copy.

Try it

1. Prove the byte-identity. Run both programs and compare everything after their title lines:

make -C examples/Choices && make -C examples/Procedures
examples/build/Choices/Choices       > /tmp/choices.txt
examples/build/Procedures/Procedures > /tmp/procedures.txt
diff <(tail -n +2 /tmp/choices.txt) <(tail -n +2 /tmp/procedures.txt) && echo same

same. Named work, identical answers.

2. Overwrite the snapshot. Inside PrintOpening, right after n := start;, add start := 999; and rebuild. One line of output changes:

The first eight steps from 999

— the header, which reads the copy. Every other number stays 27’s: the walk below the header, the whole-walk section, the tally. The procedure freely overwrote its own start, and the only place 999 exists is where the copy itself is read. The caller never noticed, because there is nothing to notice — the argument went in by value.

3. Drop the consent. In the OddCore call, change address halvings to just halvings and rebuild:

analyzer error 5180: incompatible parameter and argument data types at position 2 in call to OddCore: expected ptr.int64, got int64

The signature said lend me a variable; the call handed over a number. The compiler holds the boundary: sharing happens only where both the signature and the call spell it.

What the compiler proved

Every call in this program either copied a value in, returned a value out, or crossed the one arrow that both sides wrote down. The diff in experiment 1 is the behavioral half of the proof; experiment 3 is the compiler refusing the only way it could have silently been otherwise.

Next

The first failure — part 6: a function that admits in its signature it can fail, a call site made to say what happens then, and a missing file that arrives as a name instead of a number. Every example behind the series lives in the tutorial repository, in learning order, each with a header that says what it teaches.