Roadmap & research
The rule is: grow the logic only alongside a decision procedure. Everything below is either shipped, in the next tranche, or genuinely open research — and the open parts have a validation plan that doesn't need a referee.
One path through every layer: first-order
Int / Boolean functions, if /
case-on-Boolean path conditions, PrimOp resolution for
Ord / Ring / Semiring / EuclideanRing / Eq / HeytingAlgebra, aliases +
function specs, Z3 verdicts with spans and countermodels, golden test.
Multi-alternative Int-literal cases and guards;
let; dependent specs across argument binders;
calls to spec'd functions — preconditions checked at
the call site, postconditions assumed via fresh result variables;
recursion by assuming the function's own spec;
assume specs for imports and FFI; a
docs.json signature cross-check that fails drifted specs
before solving; verify-all as a spago backend;
--include corpora and lib/prelude.lps;
--smt2-dir replayable artifacts.
Status 2026-07-04: landed same day as the slice. Call
facts are scoped per path, so an assumed postcondition can't leak into
a sibling branch. Remaining leftover — recursive let with
local function specs — folds forward into Phase 3.
Monomorphic inductive ADTs: data and
measure declarations, datatypes as opaque SMT sorts,
constructor binders contributing discriminator and measure facts,
measure refinements instantiated at each application site to keep the
logic quantifier-free. Arrays arrive as a built-in
element-erased sort with a built-in length measure and
trusted Data.Array specs.
Status 2026-07-04: P2 proves
count / append / singleton and
refutes badCount; Arrays proves literal
lengths, growth, and valid indexing, and refutes badMid.
Remaining: selector-style field access, flat records, polymorphic
element sorts.
Abstract refinements, refinement inference for lambdas,
and specs for map / filter /
fold. Not built yet.
Bounded refinements, per-instance specs, and refinements over row-polymorphic records. Genuinely open — the metatheory here isn't settled. Not built yet, and described as research, not a promise.
The open work — row-polymorphic record refinements especially — is in scope to attempt, under one honest constraint: there is no expert on hand to referee the metatheory. So the acceptance test is not a proof. It is a human-checkable test corpus.
Before any research implementation, write (code, spec, expected verdict) triples small enough that a careful reader can judge each by eye — “this should obviously be SAFE / UNSAFE,” no theory needed. UNSAFE cases in equal number to SAFE.
Include cases engineered so a specific tempting-but-unsound shortcut — refinement leaking across row extension, width subtyping forgetting a refined field, alias capture in record update — would flip one expected-UNSAFE to SAFE. Each trap is named in a comment.
3 · The corpus is the contract. An implementation is accepted only when the corpus passes and every trap still refutes — and rejected wholesale the moment any trap blesses. This is differential-conformance thinking: an executable, inspectable artifact standing in for the review we don't have. The corpus outlives any one implementation attempt.
The SMT transport is designed to be swappable — a z3-WASM build runs the same obligations in the browser with no binary, for per-binding verified-feedback in an editor.
A Minard overlay showing which functions are verified — coverage as a map layer over the codebase.
CoreFn is backend-agnostic, so a proof about the core holds for any
backend's output. A pattern that proves
{ v : Int | 0 <= v && v < 128 } is a MIDI-safe
pattern whether it runs on JavaScript or on the Erlang backend — directly
relevant to the live-coding stack, where verified refinements would mean
verified-safe musical patterns on the BEAM.