Axiom 0.5.0
0.5.0 — 2026-08-30
The effect system finished against its own design — six of the seven
items that design listed, landing in three days — and the first
compiler change the concurrency work needs. Two of them can fail a
build that passed under 0.4.3, which is why this is 0.5.0 and not
0.4.4: Err is no longer a built-in effect name, so
(handle x (Err) 0) draws AX3016 where it used to compile clean, and
(effect IO (op :: ...)) is now AX3054, an error, where it used
to be accepted and unusable. Neither touches the standard library's
public surface — compat/0.5.0.axsym is byte-identical to
compat/0.4.3.axsym, all 591 rows — so no compat/BREAKING line is
owed; the breaks are in the language, and this paragraph is where they
are declared.
Three new diagnostics (AX3053, AX3054, AX3056), one of them a
warning by design and not as a staging step. The effect fixpoint
became a worklist and took the declaration order a generator emits from
56.05 s to 0.10 s at 8,000 functions. The emitted runtime's eight
mutable globals learned a storage class they do not yet use, byte for
byte. And two measurement artifacts that had been quietly steering the
work — the sentinel census and the bootstrap memory ceiling — were
repriced against what the code does rather than what a comment said.
Forty-five gates build the compiler under test, up from forty-two;
fifty-three run in the battery.
Known and shipping, both documented, neither a regression. A
closure application does not release its owned argument — 96 bytes per
operation, measured, with stdlib/Fallible.ax's header carrying the
number and the reason its operation takes one argument. And
sysWriteAllFd answers a short non-negative count when write makes
no progress, which its own doc comment names as "the classic way to
silently truncate output"; it needs write to answer exactly 0 for a
non-zero count, which a regular file cannot do and a non-blocking
socket reports as -EAGAIN instead. Both predate every release from
0.2.0. A third, smaller: ;@axiom:unhandled(trap) is a contract and
is not yet in the compat surface's key list, so check-compat.sh
cannot see one being removed from a third-party effect —
check-test-runner.sh guards the standard library's own.
-
The documents made true (effects item 7). This repository's style is
falsifiable claims with the probe that established them, which makes a
false claim a defect rather than a typo — the documents are the
specification, and work is planned from them. Seven were measurably
false, and each is corrected where it stood:
;@axiom:effect(IO)does not become a custom effect.
docs/agent-harness.mdcarried it as a Hazard: "silently
reinterpreted as a custom effect namedIOand reportedmissing IO". Measured — it checks OK, andsymbolsgives it
#effect=IO #effects=IO. Custom tag values match declarations
case-insensitively, so the value folds to the built-in and there was
never a trap to case-fold around.
"OnlyIOis declarable" was the wrong word, in four places
(README.md,docs/reference.md,docs/agent-harness.md,
explain AX3042). OnlyIOis required:;@axiom:effect(mut)
over a body that writes a field checks OK, and over one that does not
it isAX3010, an error.Alloc,Mutand every custom effect are
declarable and checked. What is special aboutIOis that its
absence is itself a claim.
The effect census was stale in five places —README.md,
docs/agent-harness.md,explain AX3042and twotypecheck.axhelp
strings all read 3,040 / 1,911 / 1,382 / 299. Recomputed:
3,421 / 2,095 / 1,664 / 332.
The AXSYMKINDtable was missing two of its eight letters.
docs/diagnostics.mdand.claude/skills/axiom-helper/SKILL.mdboth
listedF D C S A T;E(effect declaration) andM(macro) have
been emitted since 2026-08-26.
COMPAT-3's recorded hole is closed. It read "Thirteen public
names are outside the symbol stream…symbols.axhas no arm for
TAG_D_MACRO". It has had one since 2026-08-26,compat/UNCOVERED
has been empty since and says so in its own header, and the rule
now explains why an empty file is worth keeping: it is the assertion
that nothing has left the stream, which a deleted file could not
make.
check-agent-policy.shcalledAX3010a warning. It has been an
error since 2026-08-25 — a forged claim fails the build before the
gate reads a line of stderr.
And a note this month's own work left stale:typecheck.ax's
never-inferred list still describedErras a spellable built-in.
AX3054's commit retired it four commits ago.
README.md's Effects row said Complete while the design it was
measured against had seven open items. It now says what holds — the
handler checked against its operation's arrow, per-effect
over-approximation,AX3053,AX3054, the worklist — and what does
not: a closure application still does not release its owned argument,
96 bytes per operation. Gates:check-doc-drift,
check-tools-selfhost(explain.golden),check-render-selfhost. -
The sentinel census counts what the code does, not what a comment
says.compat/SENTINELSsizes the-errno/-1→Result
migration andscripts/check-compat.shgates its direction — a module
may never gain a sentinel. The metric matched a doc-comment against
six phrases. Audited 2026-08-30, it was wrong in four ways that
compound:
It rewarded silence.netListenforwards__syscall3and hands
back a raw fd-or-negative-errno. It was uncounted, because nobody had
written the sentence. Writing the house line above it would have taken
stdlib/Sys.axfrom 3 to 4 and failed the gate for a commit that
changed no contract. A gate that goes red when you document an
existing sentinel is a gate asking you not to.
It undercounted by roughly four times — 13 public functions over 7
modules by prose, 38 over 7 by body, withstdlib/Sys.axalone
going 3 → 26, because almost everynet*/sys*call forwards a
syscall result and almost none says so in the house phrasing.
One of its six patterns matched nothing at all:answers 0, or
appears nowhere instdlib/(the tree writes "Answers"), so its only
0-sentinel arm was dead.
And it counted a constant.sysRandomNumis
(pub fn (sysRandomNum) 33554932)— thegetentropysyscall
number, no bad path — counted because the comment walk climbed a
; ---section banner into prose aboutgetentropytwelve lines
above. That was the whole of the oldSys/Platform.darwin.ax 1, and
docs/error-model.mdhad already inherited the error and named it one
of five failures.
The new rule reads the declared return type and the body. A public
declaration counts when its return carries no channel — not
(Result …),(Option …)orBool, parsed rather than
substring-matched — and its body answers a designated value: a
(- 0 n)in return position, or an unwrapped forward of a
__syscallN/platform*primitive. It is classifiedfailurewhen it
reaches a syscall andabsenceotherwise, which isERR-REC-3's own
line:Resultis for failure, "not found" is absence and wants
Option. Both numbers are gated per module, which the old file could
not do — it had aResultskip and noOptionskip, so an
in-place port ofstrFindByteto(Option Int)would have left its
count exactly where it was, the regression theResultskip existed to
prevent.
It excludes, mechanically, what the audit had to argue about: a named
constant (fallibleSkipped,intMin, andpollReadFilter, which
is-1because that isEVFILT_READ) — a literal body with no branch
to be the bad path of; a value the caller supplies (symTagFrom
andnetAddrTexteach hold a(- 0 1)that is the seed argument of
a fold, and each answers aString) — decided by reading the enclosing
form's head; a call that never comes back; and a syscall that
cannot fail. It follows one hop through a thin private forward,
becausepathLastSlashis(pathLastSlashFrom p …)and every-1is
in the helper — but not through a body with a branch of its own, which
is consuming the sentinel (pathExt,mapGet).
docs/error-model.mdclaimed "theResultmigration is complete."
Withdrawn. 29 public functions still hand a caller a negative errno,
26 of them in one module, and none is free:netSocketTcphas 17 call
sites, seven of which never test the result at all — which is the
reason the migration exists, not an argument against it.
AndOptionis not free either, measured over 20,000,000 calls at
--opt 2: a-1return costs 1.4 ns, a(Some v)10.4 ns,
7.4×. The arena bump moves zero bytes for that loop — the block is
recycled through its size class — so a bytes-only measurement reports
Optionas free and is wrong; the cost is instructions, and
strFindBytehas 62 call sites on the compiler's own scanning path.
The floor also grew teeth: it failed only when fewer than three
modules matched, so the census could have collapsed from 13 functions
to 3 and still printedok. It is a function count now, under today's
38 by the margin a real port would move it.
What the rule still does not reach is stated rather than left to be
found: the literal-0sentinel (vecGet,vecPop,vecLast,
strByte,jsonGet,jsonArrGet); 114 public macros, among them
println, whose value iswriteStr's bytes-or-errnoIntwith 804
expansions in the tree; and members ofpub extern,pub traitand
effectdeclarations. About 21% of the public surface is in a form
(pub ::at column 0 does not match. The number is a floor.
Gates:check-compat(30 checks, and its own negative probes
unchanged). -
The emitted runtime's mutable globals move under one predicate
(concurrency Phase 2;MM-PAR-3,MM-ALLOC-1,MM-ALLOC-2). Under
fork, memory safety across processes is free: every process-wide
mutable global is private after the fork, which is whystdlib/Job.ax
needed no compiler change at all. Under THREADS it is bought, by
making the identical set thread-local — and the set is an enumeration
of@__axiom_incodegen.axrather than a sentence anyone wrote.
There are eight: the five allocator words (@__axiom_bump,
_bump_end,_chunk,_free,_high), the 4,097-word slab array,
@__axiom_recover_top, and one@__axiom_ev_<Effect>per declared
effect.@__axiom_argc/@__axiom_argvare deliberately not among
them: written once in@main's prologue, before any thread can
exist, and never again.
The half worth more is the one that does nothing.cgThreads
answers false for every program — no__thread_spawnexists for the
predicate to find — and the emitted module is byte-identical to what
it was:self_host/main.axemits the same 198,670 lines, and a
program reaching all eight globals links 0 undefined symbols.
Darwin is why that matters: a thread-local access there is not an
addressing mode but an indirect call through libSystem's
__tlv_bootstrap, measured at 1 undefined symbol with the flag on
against 0 with it off, andaxiom_alloctouches four of these on its
fast path. A language that made every program pay that for a feature
it never used would have taken the whole tree out ofMM-FFI-1's
tier 1. This isERR-REC-6's shape: a mechanism a program does not
ask for costs it nothing, measured rather than argued.
(localexec)is mandatory, not preferred. A barethread_local
takes the general-dynamic model, which needs a dynamic resolver,
which is a dynamic link, whichcheck-freestandingrefuses at zero
undefined symbols. With it:%fs:…@TPOFFon linux-x86_64 (+0
instructions),mrs TPIDR_EL0on linux-aarch64,@TPOFFon
freebsd-x86_64 — no resolver on any of the three.
Gate:check-thread-local.sh(new), 12 checks. The ON path is
reached by ablating the flag's own body, becausecgThreadsis
deliberately not a command-line switch — whether a program spawns a
thread is a fact about the program, and a switch would let a spawning
one be emitted with shared allocator words. It requires exactly 16
changed IR lines (eight globals, one line each side) and that
argc/argvare not among them; that the program still answers the
same on one thread; that no dynamic-TLS marker appears on the three
non-Darwin targets; and that dropping(localexec)makes the
markers appear, because an assertion that a symbol is absent is
satisfied by a compiler that emits nothing. That last arm caught its
own near-miss: the marker differs by architecture — x86-64 calls
__tls_get_addr(×13) where AArch64 uses TLS descriptors (tlsdesc,
×160) and never names it — so a gate grepping only for the first
would have passed an AArch64 build importing__tlsdesc_resolve
through the PLT. Both markers are checked on both targets.
What is still owed is the predicate's body: a scan of the resolved
declarations for__thread_spawn, which does not exist yet. The
reader is wired; the writer is Phase 3. Forty-five gates call
gate_build_axc, up from forty-four. -
AX3054: an effect declared with a built-in effect's name, and the
Errphantom retired.(effect IO (emit :: (-> Int Int)))was
ACCEPTED, and the acceptance was useless in a way nothing reported. A
handle list resolves a built-in name to the BUILT-IN, so the custom
effect can never be handled. Measured on this tree before the code
existed, on that declaration with(handle (emit 1) (IO) h)around
its own call:W AX3053 `main` reaches operation `emit` of effect `IO` ... E AX3011 effect mismatch: unhandled effect `IO`Two diagnostics, neither of them about the name that caused both.
Without the handle it is quieter and worse: an untaggedmain
performing the customIOreads#effects=IOwith no#effect=io
and draws nothing at all, so the symbol row says the program reaches
the outside world when it does nothing of the kind. An error with
no warning stage, and the usual objection has no instance: there is
no correct program on the other side of it, the declaration is
unusable in every direction, and the fix is a rename. The reserved
set is read fromisBuiltinEffect— the same function a handle list
asks — so the refusal and the resolution cannot drift apart.
Erris no longer one of the names. It was accepted as a sixth
built-in effect name —(handle 5 (Err) 0)checked clean — and
nothing in the compiler ever inferred it, so the name resolved and
denoted nothing. Its own AXTAG spelling could not even reach it: the
tag path lowercases the value, so;@axiom:effect(err)looked for a
CUSTOM effect namederrand answeredAX3010 missing err. The two
spellings disagreed about whether the name existed. A handle list
namingErrnow drawsAX3016, which is what a list naming
something undeclared has always drawn, andErris an ordinary name
again —(effect Err ...)declares an ordinary effect.Divis now
the only value that resolves to a built-in nothing produces, which is
what makes359-div-not-inferred.axa class of one and is said there.
Population in tree: 0 — of 50effectdeclarations none is named
after a built-in, and no handle list writesErr, which is why
neither had ever been reported. Gates:check-diagnostics
(382-effect-name-reserved.ax, four arms of which one is a silent
control;359's golden and its prose),check-render-selfhost,
check-tools-selfhost(explain AX3054),check-doc-drift. -
The effect fixpoint is a worklist.
inferEffectsis a monotone
fixpoint over the call graph, and every round re-walked EVERY body.
One round of two passes in opposite directions (2026-08-25) collapses
a linear chain in either declaration order to a single round, which
is why both orders a human writes are fast — and its own note said
what it did not do: "a graph that is not a chain can still need
several rounds, and the general fix is a WORKLIST over the reverse
call graph." This is that.
The shape it costs, measured on one chain of N functions with the
effect at the bottom, only the declaration order varying:n callers first pairs swapped pairs swapped, after 1000 0.02 s 1.34 s 0.02 s 2000 0.03 s 3.88 s 0.03 s 4000 0.05 s 14.33 s 0.06 s 8000 0.09 s 56.05 s 0.10 s 560× at n=8000, and the pathological order now costs what the
plain one does. The order that defeats both passes at once is
f2 f1 f4 f3 f6 f5 …— a helper emitted beside each of its callers,
which is what a GENERATOR produces, not what a person writes: the
forward pass meetsf2beforef3, the reverse pass meetsf5
beforef6, and each round advanced the frontier by one pair while
paying for a full walk. 3.8× per doubling where the fixed orders are
2×.
Round 1 is the pass pair unchanged — it is also what records every
edge, sincetcNoteCallwrites into word 7 whilecollectEffects
runs — and rounds 2+ walk only the callers of what grew, through a
reverse index built once from those edges. An index rather than an
FnEntfield, because the memory note prices a new field at about 6%
of a self-check and one walk needs this.
The frontier is a LIST, not a flag per declaration, and that is
the complexity argument rather than a detail: a flag vector must be
allocated or cleared once per round, which is O(N) of bookkeeping in
a round whose real content is one body walk — so the quadratic comes
straight back after being removed from the analysis. Measured with a
flag vector per round: 0.06 / 0.17 / 0.60 s at n=1000/2000/4000,
still 3.5× per doubling. The marks vector is allocated once and left
all-zero at every round boundary, because the round that sets a mark
is the round that clears it.
Nothing about the answer moves:symbols --callsis byte-identical
over every.axfile instdlib/,self_host/,tests/and
examples/— 565 of them swept, 0 differing.
Gates:check-effect-fixpoint(new) asserts a RATIO,
swap/fwd ≤ 3, so a slow runner cannot fail it; requires
--callsoverself_host/main.axbyte-identical between the tree's
compiler and one withnextFrontierablated to "every declaration is
dirty"; and requires that ablated compiler to readswap/fwd > 10,
because assertions 1 and 2 are both satisfied by a compiler that
never had a worklist. Its first draft measuredfwdCOLD and got
ratio 0.1x— a pass arrived at by mismeasuring the denominator
tenfold — so both sides are warmed before they are timed.
Forty-four gates callgate_build_axc, up from forty-three. -
AX3053: an operation the program reaches with no handler.
docs/agent-harness.mdrecorded the gap in its own words — "there is
no whole-program discharge check, so this remains a runtime failure":
an operation reached with nohandlefor its effect anywhere compiled
clean, and the process wroteaxiom: unhandled effecton fd 2 and
exited 71. There is a check now, and it needed no new analysis. A
handleis the only construct that DISCHARGES a custom effect, so an
effect still inmain's row wheninferEffectsreaches its fixpoint
is one nothing handled — the row was already answering the question
and nobody was asking it.
A WARNING, and the reason is measured rather than cautious. On the
two closure shapes the evidence is one-sided in both directions at
once.(let ((g (lambda (x) (ask x)))) (handle (g 2) (Ask Alloc) h))
runs and answers 20 — the handler is installed whengis called
— and is reported, because a lambda's operations count where the
lambda is WRITTEN. Its mirror, a closure built INSIDE the handle and
called after the handler pops, exits 71 and is NOT reported,
because theletof ahandleform is an opaque local and the row is
a lower bound there. An error would refuse the program that runs and
accept the one that traps, which is this repository's own standing
objection to promoting a check that refuses correct programs, landing
on both sides of one rule.tests/diagnostics/severity.policycarries
the measurement beside the code.
The exemption is a claim rather than a switch:
;@axiom:unhandled(trap)above an(effect ...)declaration says
the trap is the design.stdlib/Test.axcarries it onAssertand it
is load-bearing —axiom testgenerates amainthat runs each test
inside a recovery point, so every assertion reaches thatmain
undischarged and the 71 is exactly how a failed assertion ends one
test while the rest still run.scripts/check-test-runner.shdeletes
the tag from a shadow copy ofstdlib/Test.axand requires the
warning to appear, which is what makes the tag answered rather than
assumed. The value is exactlytrap;unhandled(abort)buys no
silence, andunhandld(trap)drawsAX3039— aneffect
declaration's tags were parsed, attached to word 7 and read by NOBODY
before this, so a slip in the one key that now matters was silent.
symbolsrenders the tag on the effect's ownErow as
#unhandled=trap, the first metadata that row has ever carried.
What it cost the corpus, and what that bought. Four effect
declarations gained the tag because the trap is their subject
(Test.ax'sAssert,mixed-tests.ax'sConsole,310and401).
stdlib/Fallible.axdeliberately did NOT: its own header calls an
unhandled operation "a programmer error and not a record's fault", so
a batch loop that forgets its handler is now named at compile time —
which is whatdocs/error-model.mdERR-REC-7 wanted and could not
have.tests/stdlib/410-fallible.axgave up the two terms that
reached the operation undischarged, its recovery-point term and its
last line, because the compiler refuses to be silent about the
arrangement they demonstrated;tests/diagnostics/389-unhandled-at-main.ax
pins the replacement on that effect by name, and the runtime half is
still pinned twice (310for the status and the fd-2 lines,401
withcheck-recover.shfor the 71 a recovery point answers).
The witness path reuses the restriction track'sgraphWitnessrather
than building a second one, which took one guard: an effect OPERATION
has an FnEnt with its own effect seeded, so counted as a callee it
made every function performing an operation not the source of it and
the walk answered no path at all —main -> mid -> deepcame back
empty. A related span is attached only when the witness is declared in
the same module: a span carries no unit, and the runner's cross-module
witness rendered as143:1476-1484of the generated driver, with a
caret 1,476 columns out under an elided line. Gates:
check-diagnostics(389, eight arms of which three are silent, plus
369's new silentunhandledcase),check-test-runner(the
removal arm),check-render-selfhost,check-tools-selfhost
(explain AX3053),check-doc-drift,run-stdlib-tests,
check-lsp-selfhost(070/080carry theAX3039help sentence).
tests/fmt/corpus-fmt.goldenwas regenerated - 562 entries from 451 -
because it is keyed by SOURCE hash, so eleven edited files retire
eleven mappings, and a clean trunk already stood at 59 unpinned files
against a ceiling of 60. The formatter it was taken from is the one
the same run proved:check-fmthad just formatted all 568.ax
files and re-run every suite against the formatted copy, and
check-fmt-selfhost's zoo and parity halves - which do not read that
file - were green on the same binary. -
A curried chain's intermediate record is reclaimed (
MM-LIFE-2c
event 5b). An application through a closure gave back nothing, where
a direct call has given back its owned temporaries since
MM-LIFE-2g. Every function value absorbs exactly one argument, so a
two-argument handler is a curried chain, and the record its first
step answers — born at count 1, held by nothing else — was simply
dropped: 32 bytes per application. Both walkers now release it
once the next step has consumed it, carryingrecOwnedto tell a
record this walk made from one the caller handed in, which is never
theirs to release. Measured over 1,428 applications: 45,664 bytes
before, 80 after. The cost was not only bytes —stdlib/Fallible.ax
gives the 32 as a reason its operation takes ONE argument, so a
compiler defect had hardened into a language design decision; that
row now reads 0 and the header says which of its two stated causes
was right. The one it got wrong is corrected in the same place: the
96-byte built-message row blamed "a handler parameter's type is a
variable, so the release walk cannot classify it", and a fully-typed
NAMED function passed as a value leaks the same 96, so the type has
nothing to do with it. That half is still open. Gates:
check-closure-reclaim(new —tests/stdlib/460-closure-reclaim.ax,
63 against the unfixed compiler's 7, the difference being exactly the
three byte terms with both correctness terms green either way),
check-fallible-reclaim,check-container-reclaim,
check-steady-state,check-self-host. Forty-three gates call
gate_build_axc, up from forty-two. -
AX3056: a struct field must declare its type.
(struct Box (msg String))— no:— was accepted, the written type
skipped and the field left at the empty type variable that
typeNodeOrWildcardanswers. Nothing downstream refused it:
fldClasscannot classify a variable, so the field was left OUT of
the block's reference map and out ofMM-LIFE-2cevent 5, the retain
a store into a reference field takes — and a value stored there was
released by its own owner while the field still pointed at the block.
Measured before the code existed, with a callee storing its argument
into such a field:checkreported nothing, the field read back 38
NUL bytes where the message was, and the program exited 139.
Memory-unsafe code out of a programcheckaccepted, which is
AX3055's own sentence one form over, andAX3055was spent on it
three commits earlier. An error now, at the field's name, on all
three spellings that reach the empty variable — no:, a:whose
type is not a type, and a bare(x). Two supporting changes the
report needed:mkFieldleft every struct field spanless and a
spanless diagnostic is a suppressed one, so a field now carries its
name's span the way an effect operation's has since2c5b60d; and
the struct printer used tofpBadall three shapes, which would have
made the fixture unformattable, so it prints them as written exactly
as the effect printer does. Adatastruct-variant without the colon
was already refused (AX2003), so the class is closed. Population in
tree: 0 — every struct instdlib/,self_host/,tests/and
examples/spells the colon, which is why nothing had reported it.
A third component had to learn the same three shapes and was missed
on the first pass:field_declarationin the tree-sitter grammar
demanded(name : Type), so the Tree-sitter job went red on the
commit that carried the fixture — the second time that job has gone
red for exactly this,7f73151having been the same fix for
effect_operation. Closed in05945ed, parser regenerated. Gates:
check-diagnostics
(tests/diagnostics/388-struct-field-untyped.ax, all three shapes
and a control),check-render-selfhost,check-tools-selfhost
(explain AX3056),check-fmt,check-tree-sitter. -
The CLI says Axiom and its version (
40f1e1a, which landed after
0.4.3was cut and is recorded here rather than left unstated):
axiom --help,axiom versionand the REPL greeting were three
spellings of one fact, each a separate literal the version bump had
to rewrite. All three now compose from one literal,axiomVersionin
self_host/build.ax—Axiom 0.4.3,Axiom 0.4.3 (build …),
Axiom 0.4.3 - REPL— so the site count falls by one.
check-driver.shasks for the shapeAxiom <semver>rather than
grepping for the wordaxiom, which a banner that had lost the name
entirely would still have satisfied. Gates:check-version,
check-build-id,check-repl-selfhost,check-driver,
check-doc-drift,check-install,check-fmt.