The same program, the same machine, the same bug — a field read through a pointer whose cell was already released — compiled twice:
--optimize checked
Mica runtime failure: reason=use_after_dispose (11), token_stream_index=62
Mica runtime context: file=.../Workbench.mica, line=49, column=14
Mica runtime source: seen := p.item;
exit=1
--optimize release
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 release build 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) | checked | release (O1, O2) | |
|---|---|---|---|
| Compile-time proofs | all | all | all |
| Always-on traps (below) | yes | yes | yes |
| Checked-tier traps (below) | no | yes | no |
| Optimization | none | none | standard (O1) or full (O2) |
| Debuggability | every variable observable, every line breakable | same | optimized |
Three rules complete the model:
checkedrides the debug profile.--optimize checkedmeans debug plus the checked diagnostics; there is no checked-release combination, because the checked guards and the optimizer’s freedom to reorder are contradictory goals for one build.- 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 |
allocation_failure | the allocator cannot satisfy a request — including a fixed-arena budget exceeded. 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 cycle leaks |
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 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.
Every 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.