Nothing here is asserted; it is compared against an oracle.
## The thesis.
Reviewability and correctness are treated as the same problem. If an agent writes
code and no human reads it closely, the language has to make mechanical checking
and human review cheap at once, which rules out both an untyped scripting
language whose errors surface at runtime and a proof-carrying one whose
obligations only another expert can audit.
The answer is a conservative grammar aimed at a specific failure profile: a
generator is fluent, confident, and has no memory of what went wrong last time,
so the constructs where fluent-but-wrong code still compiles are removed. No
implicit conversions, including widenings, and no `INTEGER` or `REAL`, only exact
widths, so a wire format and a type agree by construction or the program does not
build. No `NIL`: a possibly-absent pointer has type `OPT` and cannot be read
without a guard. `CASE` over a variant record must cover every arm. Every
exception a procedure can raise appears in its `RAISES` clause, derived by the
checker from explicit raises plus the declared sets of everything it calls.
`PURE` is checked by the rule that a pure procedure may call only pure ones,
which makes "no I/O" true without the checker needing to recognise I/O at all. Macros,
conditional compilation, operator overloading and Pascal's `WITH` are refused, so
a reviewer never reconstructs which text was compiled. The definition module
carries the whole contract — types, failure modes, allocation, thread-safety —
which is also what makes an interface mechanically extractable for a model.
Correctness then comes from comparison rather than specification. Rather than
asking the author to write one, an implementation is validated by running it
against the existing implementation of the same computation and requiring the
outputs to agree — and the reference is ordinary code in an ordinary language:
the Python a team is trying to replace, the Fortran kernel that has produced the
numbers for twenty years. In data science and finance that reference nearly
always already exists, so the specification burden that has historically kept
formal methods niche is absorbed by code someone already wrote and already
trusts. The discipline sits in the repository rather than the language: nothing
in the grammar names a reference, and the compiler will build a module that has
never been compared with anything.
The evidence for the premise is the project itself: a co-authorship trailer on
409 of 430 development commits from 20 August 2026. The public mirror squashes
history per release and does not show them, so the figure is the project's
account rather than something the mirror can be read for. The house rules follow
from the fact rather than decorating it — a measurement for every claim, a cited
failure for every feature, and a gate for anything that can drift are what let a
person stay answerable for code they did not type.
## What it looks like.
DEFINITION MODULE Mat ;
TYPE
Matrix ; (* opaque; lives in a POOL *)
EXCEPTION
SizeError (got, want: I64) ;
PROCEDURE New (VAR pool: POOL ; rows, cols: I64) : PTR Matrix IN pool
RAISES SizeError ;
PROCEDURE Get (m: PTR Matrix ; r, c: I64) : F64 ;
PROCEDURE SubRowVector (VAR pool: POOL ; m: PTR Matrix ;
RO v: SLICE OF F64)
: PTR Matrix IN pool
RAISES SizeError ;
END Mat.
Failure modes sit in the signature: a caller of
New that neither handles SizeError nor declares it is
rejected, while Get declares nothing because its bounds checks are
semantics rather than a contract anyone can decline. IN pool names
the arena the result comes from, and so who frees it; RO marks a
borrow the callee may not write. Nothing here names a reference implementation,
because the language has no such construct: Mat restates a
Modula-2 module kept beside it in the repository, and the comparison lives in a
shell gate that runs a C driver against goldens produced from numpy.
## Distinctive moves.
- **Checking that cannot be switched off.** No flag, pragma or build profile
removes the checks, so the code that ships is the code that was checked. The
mandatory set: bounds on every subscript and sub-slice; overflow on integer
`+`, `-` and `*`; zero and `MIN`/`-1` on `DIV` and `MOD`; range on every
checked conversion; finiteness before float-to-integer, so `Trunc(NaN)` raises
`ValueRange` rather than fabricating `INT64_MIN`; and a trap on an impossible
variant tag. Modular arithmetic must be spelled `+%`, `-%`, `*%`. The compiler
eliminates nothing statically — it emits every check and leaves the provably
redundant ones to gcc.
- **Differential execution as the acceptance gate.** Gates compare against
recorded output: goldens produced by an oracle run, checked in and never
regenerated by the gate that reads them, on the rule that a gate which
regenerates its own expectation cannot fail. Inputs are real or hand-curated
rather than generated — a seeded zarr store, a 207 MB ICOS FLUXNET CSV, 497
ERA5 GRIB messages — with no property-based generation and no fuzzing. Where
much of the verification camp makes a per-function contract mandatory, M9
requires none beyond the definition module's signature; the comparison is a
discipline the project imposes on itself.
- **Language-agnostic references.** Comparators in use are GNU Modula-2, Object
Pascal, gfortran, numpy, scipy, polars, pyarrow, the C APIs of netCDF and
ecCodes, and the Rust `zarrs` crate. Invocation is per-gate and unabstracted:
some oracles run once and their output is checked in, some are linked into the
same C driver and compared with `memcmp`, one is a live Python service the port
replays HTTP requests against, its commit pinned in a file and asserted before
any replayed byte is believed. Agreement is byte-identical where exactness is
expected, and within a stated tolerance — 1e-13 against numpy's linear algebra
— where an independent implementation orders the arithmetic differently.
- **C as the only dependency.** No LLVM, no runtime to install, no
cross-compilation story. The 0.3.1 packages were built on six distributions
spanning gcc 11.5.0 to 16.2.1, each recording its distribution, gcc version and
smoke test in a checked-in receipt, and one gate builds the whole compiler with
`fpc`, `gfortran` and `python3` replaced on `PATH` by scripts that fail loudly.
The runtime assumes POSIX rather than bare C, and every published package is
x86-64 Linux; no other platform is claimed.
- **Inherited grammar.** Seventy productions against a self-imposed ceiling of a
hundred, and sixty keywords. The departures carry their evidence: relations
bind tighter than `AND` and `AND` tighter than `OR`, because the corpus wrote
that shape six times and Wirth precedence would have rejected all six;
identifiers contain no underscores, so a foreign C name binds as a string
literal and the two namespaces never mix.
## Maturity.
Self-hosting at v0.3.1 (30 August 2026). Lexer, parser, printer, checker and C11
generator are written in M9 with the emitted C checked in, so a fresh clone
builds with `cc` alone; the bootstrap gate compares 31 modules across three
stages and requires stage 3 to equal stage 2 to equal stage 1. The standard
library is 32 modules and about 27,600 lines. There is no language server, no
formatter and no package registry. The repository carries the language report as
normative specification beside the compiler, the Object Pascal oracle, the gate
scripts and the material they compare against — the must-not-compile museum, the
checker probes, the Modula-2 and Object Pascal originals the corpus restates, the
benchmark programs — so the differential claims can be re-run rather than taken.
Three deployments, and the tutorial is the smallest and the most self-referential.
tutorial.modula9.net is written in M9: the HTTP server and the pipeline driving
`m9c`, `cc` and `bwrap` are M9, with JavaScript only for the editable cells, so
the language hosts the document that teaches it and compiles what readers submit.
Its twelve chapters are public at `atverm/M9Tutorial` and held to the compiler the
way everything else here is — twenty example programs, fourteen run and compared
byte for byte with what the chapters print and six required to fail with the
diagnostic the text quotes, plus forty-one fenced blocks that must equal the gated
file each names, and a second gate repeating the set against the compiler in the
latest release so the pages cannot describe a language the shipped package does
not have.
The other two are ports, and they verify differently. FLEXPART-M9 is a
transcription of the FLEXPART v11 dispersion model — 52 modules and roughly
30,900 lines of M9 from 45,368 lines of Fortran — running production cases through
a job queue; comparison is bit-identity, with the original subroutine copied into
the gate, compiled by gfortran, driven from the same C driver and compared by
`memcmp`. The ICOS zarr proxy is nine modules and about 11,100 lines replacing a
6,400-line FastAPI service, and its gate compares neither source nor linked
subroutines: it replays HTTP requests against the running Python and matches
status, content-type and body byte for byte, holding one deliberate divergence to
exactly. Both proxies are deployed behind one nginx switch on the same port, with
exactly one running. Both ports are in private repositories and cannot be verified
from the public one.
What they found is kept as a ledger rather than a patch set, since a transcription
that quietly corrected the model would be one whose differences nobody could bound
afterwards: 42 entries against FLEXPART v11, plus a dozen transcription mistakes
the harness caught in the port itself. Those are the more informative half,
because none was catchable statically — a module variable transcribed as both a
record field and a parameter, a loop that ran one step too many because an `exit`
sat mid-body in the Fortran. The proxy replay caught its own instance: a passport
citation carrying `á` went out as a literal `\u00e1`, a client-visible difference
every crafted test store had missed by being ASCII. The limits are stated with the
results — agreement holds only over the inputs actually run, and one untranscribed
call is invisible precisely because the data carries no message that would expose
it. The oracle itself needed pinning: gfortran 15 at `-O2` changes its own answer
under `-ftree-vectorize`, one single-precision ULP on 152 of 960 elements, so
every oracle is built `-fno-tree-vectorize` and checked against its own `-O0`
build first.
On three published benchmarks, each diffed for identical output before any clock
is read, M9 is at parity with C on floating point (mandelbrot N=4000, 0.73 s for
both) and marginally ahead of unchecked C on integer work with every check active
(fannkuch-redux n=11, 1.90 s against 1.94 s), while Rust leads both integer
benchmarks and Scala leads on allocation churn. The 3% figure is isolated by
hand-editing the generated fannkuch C into variants that change one thing each;
removing every bounds check, verified by `grep -c m9_at` reaching zero, bought
1.81 s. Figures are one machine, best of three or five, and the project publishes
its losses alongside. One finding qualifies the 3% usefully: the checks' indirect
cost is the larger one, since a checked procedure body rarely fits gcc's default
inlining budget of 15 instructions, so `m9c` ships `--param
max-inline-insns-auto=200` alongside `-O2` and `-flto` — worth 2.4× on one
measured kernel, more than deleting the checks outright would have been.
## Agent tooling.
`m9c --doc` writes a module's definition as Markdown, listing undocumented names
marked rather than omitted; the 29 generated references are checked in and held
byte-identical by a gate. `m9c --json` writes the same gather as data: per
procedure its kind, line, rendered signature, parameters as name/mode/type
triples, result, `RAISES` list and attribute. The manual page states the
motivation in agent terms — that the commonest mistake a fluent generator makes is
a real name it did not look up, and that a table of names copied into a prompt
drifts within a day. Both run the checker first, on the grounds that documentation
for a program the checker rejects describes a program that does not exist, and the
same path feeds the VS Code extension's hover and completion. A message/cause/fix
table covering every refusal the checker can produce is generated from the same
negative programs the two checkers are held to, so a refusal with no explanation
fails the build. `m9c --no-unsafe` refuses a program whose import closure declares
an `UNSAFE` or foreign unit outside the trusted library directories, which is what
lets the tutorial service compile strangers' code with the OS sandbox as a second
wall rather than the only one.
Diagnostics are human-readable text with line and column, not JSON, and there are
no stable error codes. There is no MCP server and no language server. Two Claude
Code skill files exist in the development tree and are gated there, but they are
not published, and nor is the project's own memory file.
## Design DNA
- **[Vera](https://agentlanguages.dev/languages/vera.md)** *(Verification)* — Same diagnosis, different discharge. Vera compiles per-function requires/ensures obligations into Z3 queries and degrades to runtime guards where the solver cannot reach; M9 has no obligation language and compares execution against an existing implementation in another language. Vera proves a property for all inputs it can decide; M9 observes agreement on the inputs it runs.
- **[NanoLang](https://agentlanguages.dev/languages/nanolang.md)** *(Verification)* — Closest on method, furthest on provenance. Both make execution rather than proof the primary evidence — NanoLang through mandatory shadow test blocks written alongside each function, M9 through agreement with an external implementation the author did not write. NanoLang additionally carries a Coq-proved core; M9 makes no proof claim.
- **[Faber Romanus](https://agentlanguages.dev/languages/faber.md)** *(Syntactic)* — Same two-audience premise, different lever. Both hold that code an agent authors must stay readable to a human reviewer; Faber Romanus reaches for keywords selected for token stability across models, M9 for an inherited Modula grammar that predates the problem.
## Timeline
- **Aug 2026** — Language report draft 0.1 and the first lexer land together on 20 August, each feature citing a failure observed that week while porting a zarr reader; the failures are kept as programs that must not compile.
- **Aug 2026** — Bootstrap fixpoint on 22 August: C emitted by a compiler built from its own output is byte-identical to the C it was built from.
- **Aug 2026** — v0.3.1 published on 30 August for six x86-64 distributions, alongside tutorial.modula9.net, a tutorial service written in M9 that compiles and runs reader-edited examples in a sandbox.
---
HTML version: https://agentlanguages.dev/languages/m9/
Catalogue index: https://agentlanguages.dev/llms.txt
Catalogue homepage: https://agentlanguages.dev/index.md