Mandatory shadow test blocks on every function. The proved core (NanoCore) has 193 Coq theorems with zero axioms. Multi-target codegen across C, WebAssembly, LLVM IR, PTX, and RISC-V.
Camp: Verification
Also spans: Syntactic
Author: Jordan Hubbard
Implementation language: C
Compilation target: C (default), WebAssembly, LLVM IR, PTX, RISC-V
Licence: Apache-2.0
First seen: September 2025
Maturity: working compiler
Agent tooling:
- AGENTS.md
- CLAUDE.md
- MEMORY.md ("training reference for patterns and idioms")
- spec.json (machine-readable formal specification)
- .mcp.json
- .claude/, .cursor/, .factory/ config folders
- VS Code extension with LSP (nanolang-lsp) and DAP (nanolang-dap)
- Web playground with CodeMirror-6, share permalinks, live evaluation
Mandatory shadow test blocks on every function (the compiler refuses
to compile without one) plus 6,170 lines of Coq proving the language's
core. NanoCore is the proved subset, not the entire surface language —
algebraic effects, async/await, FFI, the VM, and multi-target codegen
sit outside the proof set. The first-person README persona ("I refuse
to compile a function unless you provide a shadow test block") is
documented as deliberate design, not flourish.
NanoLang takes the verification camp's diagnosis literally: if LLMs are going to write code, the language should refuse to accept their work without tests, and the language's core should have proofs to back its promises. Every function declaration must be paired with a shadow test block; the compiler rejects functions without one. The proved core (NanoCore) has 6,170 lines of Coq across 9 files, 193 theorems and lemmas, zero axioms, zero Admitted — the proofs cover preservation, progress, determinism, semantic equivalence of big-step and small-step, and evaluator soundness against a fuel-based reference interpreter extractable to OCaml. The README announces it in first person: "I refuse to compile a function unless you provide a shadow test block for it."
"I am a minimal programming language designed for machines to write and humans to read. I require tests, I use unambiguous syntax, and my core is formally proved."
The distinctive move is the depth of what is actually proved — and the honesty about what is not. NanoCore covers integers, booleans, strings, arithmetic, conditionals, mutable variables, while loops, lambda/application, arrays, records, recursive functions, variants, and pattern matching. Algebraic effects, async/await, FFI, the VM, and the multi-target codegen sit outside the proof set, and formal/README.md says so plainly. Vera proves contracts at the function level via Z3; NanoLang proves the type system itself, from below. Same camp, complementary layers.
fn greet(name: string) -> string { return (+ "Hello, " name) }shadow greet {
assert (== (greet "World") "Hello, World")
}fn main() -> int {
(println (greet "World"))
return 0
}shadow main { assert true }
Every function needs a shadow block. shadow main { assert true } exists only because the compiler refuses to compile without it — and the trivial case still has to satisfy the discipline.
shadow block. The smallest legal program contains shadow main { assert true } — the discipline applies to the trivial case alongside the substantive one.Syntax.v, Semantics.v, Typing.v, Soundness.v, Progress.v, Determinism.v, Equivalence.v, EvalFn.v, and Extract.v. No Admitted lemmas; the proofs go through. Built on Rocq Prover (Coq) ≥ 9.0.nano_cop); if they crash, the VM survives. Trap model separates computation from I/O.--target wasm (with source-map sidecar and Ed25519 signing), llvm, ptx, riscv. Production parity is claimed for C and WebAssembly; the other backends are present in the toolchain.(+ a b) and a + b are both legal. The prefix form is described as unambiguous and is the form the formal semantics is stated against.AGENTS.md instruct agents to write in NanoLang's voice. Documented under docs/PERSONA.md as a design choice, not a quirk.v3.3.7 (April 2026), 51 tagged releases, ~2,156 commits, bootstrap 100% (the compiler compiles itself). Apache-2.0. Hardware support: Ubuntu 22.04+ on x86_64 and ARM64, macOS 14+ Apple Silicon, FreeBSD; Windows via WSL2 only. The author is Jordan Hubbard — co-founder of FreeBSD in 1993, currently Senior Director for GPU Compute Software at Nvidia — and the project's GitHub topics include thought-exercise and vibe-coding, applied by the author himself. The README's "Totally True and Not At All Embellished History" notes the language has "been used in production by exactly one person, who also wrote it." That candour matches the catalogue's tone: the engineering is real, the framing is honest about what the engineering is for.
The repository root ships AGENTS.md, CLAUDE.md, MEMORY.md (self-described as "my training reference for patterns and idioms"), spec.json (machine-readable formal specification), .mcp.json, and config folders for Claude, Cursor, and Factory. The IDE surface includes a Language Server (bin/nanolang-lsp) and Debug Adapter (bin/nanolang-dap) plus a VS Code extension; the web playground supports share permalinks and live evaluation. The agent-facing surface is wider than most catalogue entries — NanoLang ships not just orientation files but its own corpus.
<Inference> effect has no NanoLang analogue.Last modified 15 June 2026