The same program, the same machine, the same bug — a field read through a pointer whose cell was already released — compiled twice:
--optimize release,full_optimizations,checked
Mica runtime failure: reason=use_after_dispose (11), token_stream_index=67
Mica runtime context: file=Workbench.mica, line=22, column=14
Mica runtime source: seen := q.item;
exit=1
--optimize release,full_optimizations
free(): double free detected in tcache 2
Aborted
exit=134Read the two reports closely, because the difference is sharper than
“one has more detail”. The checked build names the first wrong act — the
read through the released cell — with its reason, file, line, column, and the
offending source line printed back. The build without checked reports the second
symptom: by the time glibc notices anything, the wrong read has long since
happened, and what the allocator reports is a later consequence, somewhere
else, with no line and no name. One is a compiler telling you what you did.
The other is an allocator telling you it noticed something, somewhere, after
the fact.
This page is the reference behind that difference: what each tier proves and guards, and the complete list of runtime traps — every reason the runtime can name, its trigger, and the tier it runs on.
The tiers
The command line defines the spellings; this table defines the semantics. Every tier compiles the same language and refuses the same programs — the compile-time proofs run everywhere. The tiers differ only in what is guarded at run time and what the generated code spends on it.
debug (O0) | debug,checked (O0,checked) | O1, O2 | O1,checked, O2,checked | |
|---|---|---|---|---|
| Compile-time proofs | all | all | all | all |
| Always-on traps (below) | yes | yes | yes | yes |
| Checked-tier traps (below) | no | yes | no | yes |
| Optimization | none | none | standard (O1) or full (O2) | standard or full |
| Debuggability | every variable observable, every line breakable | same | optimized | optimized |
Three rules complete the model:
checkedis a flag, not a profile. It joins whichever profile the set names:O2,checkedis the shipped program with every guard on, anddebug,checked(orO0,checked) the build where every variable is observable at the trap. Alone,--optimize checkedmeansrelease,checked, as every set that names no profile means release. A trap names the same act at the same source position on every tier: the tested program is the shipped program, at the guards’ own price. The guards and the optimizer do not contend — the middle end proves a transformation trap-free before it applies it, and a guard it cannot prove away stays.debugalone carries none of the heap guards: run a program atdebug,checkedbefore you trust it.- What the checked tier guards, the release tier leaves undefined — by design, and the line is drawn where the machine’s own answer is defined. A release-tier signed overflow wraps, a release-tier bit shift past the width produces the machine’s documented result, a release-tier float-to-integer cast saturates. What is never left undefined, on any tier, is the list in the next section.
O3is refused by name. The transformations that would distinguish it fromO2— vectorization, loop unrolling — do not exist yet, and an alias that silently meantO2would be a promise the compiler does not keep. You get an explanation, not a build.
Traps on every tier
These guards are part of the language’s semantics, not a diagnostic mode.
They run in debug, checked, O1, and O2 alike, because for each of
them the alternative is not “a faster program” but a program whose behaviour
has no defined reading at all — or one that differs between architectures.
| Reason | Fires when |
|---|---|
division_by_zero | an integer division or modulo meets a zero divisor. Guarded on every tier because the two architectures disagree without it — one faults, one silently yields zero — and Mica’s answer is the same trap on both |
signed_arithmetic_overflow | the one always-on case: MIN / -1, the single signed division that cannot be represented. All other overflow guarding is checked-tier |
nil_dereference | a read or write through a nil pointer. The compiler owns this check rather than borrowing the MMU’s page fault, so the answer is the same on hosted and freestanding targets |
index_out_of_range | a variable index misses its array’s bounds. Constant misses were already compile errors |
tensor_shape_mismatch | two tensor operands whose extents live in their values disagree at an operation — unequal elementwise extents, a matrix pair sharing a total but not a shape, a product’s inner dimensions, a dot’s lengths, or a dynamic value against the static shape it meets. Always on, one compare on the agreeing road: the mismatch that would otherwise read past the shorter backing |
allocation_failure | the allocator cannot satisfy a request — including a fixed-arena budget exceeded, and a stream’s ring whose computed capacity is below one or larger than memory can hold. An allocation that failed has no value to continue with |
map_key_missing | a map read names a key the map does not hold |
file_read_past_end | a typed read reaches past the end of its file |
file_write_failed | the operating system refuses a write |
stack_overflow | recursion exhausts the stack. Reported by name, as a trap, instead of the anonymous segmentation fault other toolchains leave you |
foreign_pointer_release | a dispose meets a pointer that Mica’s allocator did not produce |
explicit_panic | the program says so |
Traps on the checked tier
These guard the cases where the release tiers accept the machine’s own defined answer. The checked build refuses the answer and names the act.
| Reason | Fires when | The release tiers instead |
|---|---|---|
signed_arithmetic_overflow | an add, subtract, or multiply leaves its type’s range | wrap |
unsigned_arithmetic_wrap | an unsigned add, subtract, or multiply wraps | wrap |
bit_shift_out_of_range | a shift count reaches the operand’s width | the machine’s documented result |
cast_out_of_range | a narrowing integer cast loses the value, or a float-to-integer cast misses the target’s range | truncate; the float source saturates |
cast_invalid | a float-to-integer cast meets NaN | yield zero (the saturating conversion’s answer) |
floating_arithmetic_invalid | a float operation produces NaN from non-NaN operands | propagate the NaN |
floating_arithmetic_overflow | a float operation produces an infinity from finite operands | propagate the infinity |
ordinal_out_of_domain | a value converts into a subrange, enum, bool, or unicode scalar it does not fit — including the surrogate window | store the bits |
use_after_dispose | a read or write through a pointer whose cell was released | undefined |
double_dispose | a cell is released twice | undefined |
cyclic_ownership | a cycle of owners reaches the drain | the drain follows the cycle until the stack runs out, and the always-on guard reports stack_overflow |
assertion_failed | an Assert does not hold | asserts are not compiled |
Two footnotes to that table. Undefined in the heap rows means exactly what the opening demonstration shows — not “probably crashes”, but “whatever the allocator’s internal state makes of it, reported late or never”. And the heap rows are the unprovable remainder: most use-after-dispose and double-dispose programs do not compile at all — the checked-tier trap exists for the cases a runtime condition hides from the compile-time proof.
What the checked tier costs in memory
A checked run answers a stale pointer, and it pays for the answer in memory. Every cell it releases is kept, poisoned, so that a read through a pointer to it is recognized rather than served; and every block it can serve no further cell from is quarantined for the rest of the run. A checked program’s storage therefore grows with the work it does — by design, and for as long as the run lasts.
That is the price of the guarantee, and the guarantee is not weakened to lower it. What it changes is the budget. A program given the fixed arena its release build runs in will exhaust that arena under a checked build, and the exhaustion reads exactly like a leak — which is the opposite of what it is. So the report says so: the allocation failure closes with a note naming the checks.
Mica runtime failure: reason=allocation_failure (8), token_stream_index=43
Mica runtime context: file=table.mica, line=18, column=14
Mica runtime source: a := new Ints reserve 200;
Mica runtime note: this program is built with memory checks, so every cell it releases is kept poisoned and every block
it can serve no further cell from is quarantined for the rest of the run. Its storage grows with the
rounds by design, and a budget sized for the release build is too small for a checked one.Give a checked run room: the hosted heap, or a fixed arena sized for the whole run rather than for the live set. The release build is the one the budget is measured with.
What a trap is — and what it is not
Mica separates two kinds of going wrong, and the boundary runs straight through this page.
A failure is a value: a file that is not there, a key that might be
missing, input that does not parse. Failures travel the fails channel, are
declared in a function’s signature, and handling them is the program’s
ordinary business — the failure channel article
covers the whole discipline. A map read whose absence you expect belongs
there, and the standard library gives you the failing spelling.
A trap is the runtime’s verdict that the program itself is broken: the trap list above is not a list of conditions to handle but a list of bugs with names. There is no catching a trap, no resuming past one, and no trap handler — the program stops, names the reason, the file, the line, and the column, and exits nonzero. If a trap fires, the fix belongs in the source, not around it.
That is also why the trap report is deliberately spare: reason, place, offending line. Everything a bug report needs, nothing a control flow could consume.
Reading a trap report
Mica runtime failure: reason=index_out_of_range (12), token_stream_index=88
Mica runtime context: file=/work/Sieve.mica, line=31, column=18
Mica runtime source: flags[candidate] := false;
exit=1Line one names the reason — the spelling in the tables above — and its
number. Line two places it: file, line, column. Line three quotes the
offending source line. The process exits 1 for every trap — including a
stack overflow, which arrives through the signal road but reports and exits
like every other reason. A genuine segmentation fault, by contrast, is
deliberately not dressed up as a trap: it kills the process with the real
signal at the real address, so nothing about a crash is disguised.
A second release met inside a container’s release walk carries one more line. Releasing a container releases every cell its owning slots hold, so lines two and three name the release that started the walk, and the walk line names where the walk met the cell again: the release of the cell’s type, at that type’s declaration.
Mica runtime failure: reason=double_dispose (10), token_stream_index=128
Mica runtime context: file=Boxes.mica, line=31, column=5
Mica runtime source: dispose box;
Mica runtime walk: this release's walk met it in the drain at file=Boxes.mica, line=7, column=5
exit=1Every reason in the tables above is produced, on both architectures, by the compiler’s own test suite — the tables are generated evidence, not aspiration. No trap is listed that has not been fired.