The Mica Compiler

Mica proves at compile time what other systems languages leave to the debugger: heap lifetimes, data-race freedom, and array bounds — with no garbage collector, no borrow checker, and no lifetime annotations.

Mica is a statically typed systems language with an optimizing native backend. It compiles to Linux x86_64 and AArch64 ELF binaries with DWARF v5 debug information, links directly against any C library on the system in both directions, and carries no runtime you did not ask for.

It is its own language, influenced by Pascal, Ada, and C: readable declarations, explicit types and no hidden control flow from the structured school; Ada’s engineering seriousness about what a compiler should prove; C’s directness at the machine and at the library boundary. The type system, the memory model, the failure channel and the concurrency model are Mica’s own. What the language deliberately leaves out is as designed as what it includes — see refusals as design.

At a glance

The condensed version of everything on this site is the facts sheet — one page, every figure generated from the repository.

A first look

program FailsChannelBasic;

imp
    WriteLn : std;

type
    ParseError = error (BadDigit, Overflow, EmptyInput);

var
    n : int64;

function ParseDigit(c : int32) : int64 fails ParseError;
begin
    if c < 0 then
        fail EmptyInput;
    if c > 9 then
        fail BadDigit;
    ParseDigit := c as int64;
end;

function ParsePair(a : int32, b : int32) : int64 fails ParseError;
var
    left : int64;
    right : int64;
begin
    left := ParseDigit(a) on fail leave;
    right := ParseDigit(b) on fail leave;
    ParsePair := left * 10 + right;
end;

begin
    n := ParsePair(4, 2) on fail use -1;
    WriteLn("%lld", n);                     { 42 }

    n := ParsePair(4, 77) on fail use -1;
    WriteLn("%lld", n);                     { -1 }
end.

Errors that a caller is expected to handle travel on a dedicated channel declared in the signature. Bugs do not: they are a separate mechanism that terminates deterministically. The two never share a path. See the failure channel.

What makes it different

The full list is the capability catalog. These six are the ones we would lead with in a technical evaluation.

Sharing has to be written down

Concurrency is a visible block with a structural join, and every touch of shared state must be spelled synchronized. Touch a global or an ancestor activation’s cell without the mark — directly, or through a call several frames down — and it is a compile error, not a lint. Taking a bare address of a shared cell inside the region is rejected too.

The practical effect is that unmarked code is not shared code, so a reviewer’s search space collapses. Deadlock freedom follows from construction: owners form a chain, and locks are acquired in chain order.

The same source compiles for a single carrier or for many, with no source change ever, and a single-carrier build produces byte-identical output to the sequential one. → Compile-time data-race freedom

Heap lifetimes proven by flow analysis

Every allocation creates an obligation attached to the allocation value. Wherever the compiler can follow the pointer, it must see that obligation discharged on every path, and an undischarged cell is a build error.

The part we care most about is the honest half. Where a pointer’s flow escapes what the analysis can follow, Mica does not guess — the site degrades to manually-verified and the compiler tells you what it could not prove, rather than demanding an annotation. That is a zero-false-positive posture a borrow checker structurally cannot offer. → Heap lifetime proof

Allocator selection is a link-time decision

The intermediate language never names malloc; it emits allocator intrinsics. Which deployment class those bind to — hosted, or a freestanding fixed-arena with no OS heap at all — is decided when you link, and code generation is byte-identical across both, down to matching object-file hashes. Regions are scheduled by the compiler per allocation site from the lifetime it proved, and run inside either class. One source tree serves a Linux server and a statically budgeted embedded target. → Allocator as a link decision

Determinism as a shipped guarantee

Parallel linear algebra is bit-identical to serial at every carrier count, because work is partitioned by whole output rows and never within an accumulation. Parallel reductions are refused rather than silently provided. Floating-point contraction decides identically on both backends, so a program produces bit-identical results across architectures at a fixed optimization set. → Determinism

The C boundary is a typed surface

An imported C function is a failing function. Its error convention — negative errno, NULL, or a sentinel value — is declared once in a contract and lifted at the call site into the language’s failure channel. No -1, no NULL, no MAP_FAILED, and no errno in user code. Curated contract packs cover the C standard library, POSIX, and Linux. → The C boundary

Zero dependencies, one vendor

184,558 lines of pure Go, an empty dependency set, and the GNU assembler and linker as the only external tools. Every phase — scanner, parser, type system, semantic analysis, intermediate language, inlining, SSA optimization, register allocation, two native backends, ELF and DWARF emission — is ours. Adopting Mica means trusting one vendor, not a dependency tree. → Zero-dependency implementation

Where to go next

Figures as of 2026-08-05, compiler 6.12.8.