Rune

Rune is the kernel of a small, content-addressed, dependently typed language. A finished proof is a value, and its identity is the hash of its content, so verification becomes a cache that never recomputes. Dependent types are a build-time discipline; what deploys is the erasure. The parts people fight type-theory wars over (the codegen target, the resource semiring, the notion of equality) each sit behind a clean interface, so the right one lives in the right layer.

The end goal is provably correct infrastructure code. The release criterion, every version: the code listings of the book Specify & Verify elaborate, check, and run against this core, and the core contains nothing the book does not use.

v3.385.0 — complete Go+ source migration

Rune’s remaining source moved to .gp, completing the repository-wide Go+ authorship migration without changing the public module path or hash format. The patch also registers the natural-number accelerator in chapter 527 so uint32 decoding uses the intended fast path.

v3.384.0 — elaborate and store join the Go+ kernel

The typechecker (elaborate/) and the content-addressed definition store (store/) are now Go+ sources too — the whole trusted path from surface syntax to stored hash. Hand-rolled term walks became derived traversals: the placeholder scan is a TmUniverse sweep that sees the equality/cast/pair positions the old walk skipped, and replaceRef’s 19-case recursion is a one-arm TmTransform. The meta-zonker and the core checker dispatch by exhaustive match, with the new multi-pattern arms (Go+ v0.14.0) classifying rigid heads in one line. The hash corpus stayed byte-identical through every step.

v3.383.0 — the kernel is authored in Go+

The trusted core — the term language, the glued NbE value domain, hashing, conversion, quotation, and the 5,500-line evaluator — is now written in Go+ and distributed as its generated Go, so consumers never need the goplus toolchain. Tm, Val, and Neutral are enums whose lowering is byte-compatible with the hand-written sealed interfaces they replace: the hash format never moved, gated by a corpus harness (cmd/hashdump) that proved all 93,216 definition hashes across the book’s 579 listings byte-identical before and after. Every kernel case analysis is an exhaustive match — an added constructor is a generation-time error, not a runtime panic — and the two typeclass-shaped strata (the usage semiring, the equality stratum) became Go+ classes whose algebra is stated as laws with generated property tests: the strata’s first tests ever.

v3.2 — the ergonomics ladder

Seven rungs of pure surface sugar over an unchanged core — the hash format never moved:

• Infix operators — + - * / % as definable symbolic identifiers; the printer round-trips infix.
• Numeric literals — builtin nat expands digits at parse time; the printer folds successor chains back to digits.
• = sugar — x = y elaborates to Eq _ x y, metas solve the type.
• case … of | pat -> e end — desugared to one saturated eliminator application: coverage by construction, induction hypotheses via with ih, dependent motives free when the scrutinee is a variable.
• calc ladders — equational reasoning chained through subst, each step pinned to its own equation, no library dependency.
• BigInt shadow — the builtin nat compiles to machine integers, so gcd 252 105 prints 21 under node in milliseconds.

The gate: a full arithmetic chapter — addComm proved in calc, fuel-style div/mod/gcd, arithmetic facts certified by bare refl. There is also a ten-lesson course from zero to machine-checked proofs.

v3.0.0 — two equalities, one substrate

v3 ships two-level type theory the way v2 shipped quotients: a builtin content-addressed group, zero new core syntax, zero hash-format change. The strict, proof-irrelevant Eq (UIP and all) stays exactly as it was; alongside it, a fibrant universe à la Tarski houses the inner layer:

• UF, El, fib, piF — fibrant types as codes, with decoding that computes: El (piF A B) is the genuine function type, so inner functions are plain lambdas.
• Inner identity, twice — point-level pathF/pathJ (J with its β-rule), and type-level pathU with ua — univalence, postulated: the inhabitant UIP forbids globally lives locally, as a permanently neutral head. pathU A B is data, not Prop, so the two equalities never name the same relation and never contradict.
• Transport computes through ua: castU … (ua … not …) b is not b, provable by bare refl. Path induction over a ua-path and the higher coherences are the labelled frontier — postulated, not sold.
• Check, not run — honestly enforced: erasure has no meaning for ua-paths yet, so codegen skips inner-tainted definitions and refuses a tainted main rather than silently emitting the wrong function.

v2.0.0 — quotients, without growing the core

v2 proves the extension thesis: a new type former with no new core constructor, no new token of syntax, no hash-format bump.

• Quot A R as a first-class type — qin, qsound, qlift (one respect proof, paid once), qind (respect free, by proof irrelevance): a builtin group of bodiless content-addressed definitions, computing by quotient ι-rules in the evaluator.
• Eq stays uniform; UIP holds untouched. Set-level truncation ‖A‖ is the Church encoding in impredicative Prop — no former ships because no chapter needs one.
• The shadow stays boring: a quotient compiles to its carrier — qin is identity at runtime, every respect proof erases. ℤ as a quotient computes 2 + (−1) under node with the proofs verifiably absent.

v1.0.0 — the foundation

What v1 contains:

• The MLTT core with glued NbE: eval/quote over glued values, βδηι conversion with a fast syntactic path that unfolds only on mismatch.
• The proof cache: forcing a glued neutral is store.Unfold, the sole body gateway, and logs the dependency; certificates are keyed (content-hash, ‖unfolded-set‖), append-only, no invalidation logic anywhere — the Frame Lemma is a live property test.
• Elaboration: bidirectional checking, contextual metavariables, pattern unification, implicit arguments ({x : A}) and holes (_).
• Observational equality: proof-irrelevant Prop, Eq computing on type structure — funext is a reduction, not an axiom — plus cast and subst; UIP holds.
• Data by eliminators: strict positivity, generated induction principles, coverage and totality by construction; induction proofs compute.
• Quantities (QTT): 0/1/ω on binders, usage checking; the 0-fragment is the erasure boundary.
• Predicative universes: U, U1, …, cumulative, impredicative Prop.
• Codegen: erasure to a target-independent IR and a JavaScript backend — rune emit / rune run; proofs and types are absent from the output.

Install

go install goforge.dev/rune/cmd/rune@latest