Language reference: a beginner's book that quotes the sources

[Russoul]

A third rendered page alongside the theory specs and the syntax-highlighted sources: a tutorial and reference for the surface language. It assumes a functional programmer who reads mathematics, and assumes nothing about dependent types or proof assistants. Unlike docs/*.txt it is not normative — it teaches the language and links into the specs.

46 chapters in nine parts; 18 written, 28 outlines. The page reports that itself, in a progress line, and badges every unfinished chapter — so it is honest about its own state rather than looking finished and being hollow.

What is here

• docs/reference/*.md — the book. Parts I–III are complete (Orientation, Writing Nova, Data and recursion), plus The discharge engine and Types without coherence from later parts.
• tools/render-reference.py — renders it to one self-contained page, reusing render-specs.py's palette and the LSP's own token classes, so a snippet reads exactly like the same line on the sources page.
• tests/nova/docs/ — nine goldens: the quotation check, and eight fixtures pinning the worked examples.
• Flake wiring — nix/packages.nix renders reference.html into .#site, and --check is a flake check of its own.

Structure

Part
I Orientation ✅	what this is, what a checker is for, installing, your first file
II Writing Nova ✅	notation, definitions, let, operators, modules
III Data and recursion ✅	base types, pairs, sums, your own types, eliminators, clauses
IV Types that depend on values	the idea, Π, Σ, universes, implicits, indexed families, checking vs inference
V Propositions and proofs	propositions, equality, reflection, induction, chains, connectives, quotients
VI Working with the checker	the report, holes and in-place elimination, the discharge engine, using, recipes, pitfalls
VII Coming from Agda	a map, reflection instead of J, types without coherence
VIII Beyond the basics	QIITs, coinduction
IX Reference	grammar, precedence, generated names, library, tooling, glossary

Three decisions worth a reviewer's attention. Recursion is introduced as a surprise — "there is no general recursion, and the name of a definition is not in scope in its own body" is the first thing that ambushes a functional programmer, so eliminators arrive as the answer rather than as a primitive. The Agda comparison is late and optional, because a reader who has never used a proof assistant has no comparison point; chapter 1 points those who do straight at Part VII. And chapter 4 fails twice on purpose before the file is accepted, because the obligation loop is what no summary conveys — one failure carries a hint: (a licence is missing), the other does not (the mathematics needs an induction), which hands a beginner a triage rule from their first obligation.

The book quotes the sources; the suite enforces it

The reference does not copy the corpus, it quotes it, and render-reference.py --check verifies every quotation:

Fence / citation	Must occur verbatim in
```nova	src/nova/*.nova or a golden's input.nova
```report	a golden's expected
docs/*.txt, src/nova/*.nova, tools/* paths	the tree
backticked rule names (el-reflect, prop-lift, …)	the rulemap render-specs.py builds from the specs

Matching is by blank-line-separated chunk: a snippet may elide whole items, but each chunk must appear as a contiguous, dedented, verbatim run of lines. Golden inputs count as a source because a deliberately failing example cannot live in the accepted corpus. ```nova-sketch is the escape hatch for genuinely illustrative code — grammar skeletons and error cases — highlighted, exempt, and visible as an exemption in the source. Currently 98 quoted snippets, 17 illustrative.

Chapter 5 is built from a census of the corpus — Nova code uses exactly 32 non-ASCII characters, twenty of them the language — and a check verifies that every one still appears in the chapter.

It has already caught real drift, twice

The Prf retirement. The gate flagged two drifted snippets; reading the commits turned up four further stale claims in prose that no gate could catch, including a data signature using a retired spelling and advice to write El ℕ for external domains that had become exactly backwards.

The last thirty commits. The gate caught eight transcripts and two snippets. Reading the commits caught the rest: ⨯ became × and ⨯ is now unrecognised, so chapter 5's look-alike table had the advice inverted; × moved below ⊎, which deleted the precedence trap chapter 11 was built around; ASCII fallbacks mean chapter 5 no longer opens by telling a newcomer they must type Unicode; ?x holes returned, contradicting chapter 4 outright; and VS Code and neovim clients now ship from the flake.

That is the argument for the gate: mechanical drift is caught automatically, and the prose it cannot check is at least localised for a human to re-read.

Outline audit

Checked every production of the surface grammar, every CLI command and every section of NovaElaboration.txt against the chapter set. Three user-visible features had no home, all from the recent batch:

• In-place elimination — nova eliminate <file> <line>:<col> <var> fills a hole by eliminating a variable of its context and prints the file back, turning λn. ?goal into λn. (ℕ-elim ?goalZ (n ih. ?goalS) n).
• Refinement — synthetic holes are solved from the run's own constraints, so a goal reads as ?p : x ≡ y ∈ A rather than as elaborator scaffolding. Holes you wrote are never guessed at.
• Recovery — a failed item no longer hides every goal after it.

Part VI now has Reading the report and a new Holes and in-place elimination; the tooling outline lists every command and gate script.

Other things worth knowing

• Chapter order lives in PARTS in the script and files are named by slug, so inserting a chapter renumbers nothing.
• Cross-references are anchors, never chapter numbers, with a build-time dead-anchor guard — it caught seven broken links during the restructure and four more when a chapter was split.
• The snippets golden's expected is a hand-written success line; its run script says why, after regenerating it from a red run once baked a failure in.
• Code blocks bleed right of the prose column above 1200px, because real corpus lines are wider than a comfortable measure; the page body never scrolls sideways.
• Equality is written but still pitched at the old audience; it carries a %revise badge rather than pretending otherwise.

195/195 tests, six flake gates.