NanoLang: A Small Language Built to Be Written by LLMs and Proved in Coq

The problem NanoLang picks: machine authorship, not human ergonomics

Most language design optimises for what a person can hold in their head. NanoLang inverts that. Its README states it is "a programming language designed for machines to write and humans to read", and the repository topics include llm, domain-lang and vibe-coding. The stated requirements are that the language demand tests, use unambiguous syntax, and carry a formally proved core. The target author is a coding model; the target reader is whoever reviews the generated code afterwards. That framing explains several decisions that would look odd in a general-purpose language. Shadow test blocks sit next to every function and the compiler warns loudly when one is missing, so a generated function arrives with its own assertion attached. Prefix calls such as (+ a b) are described as unambiguous, with infix a + b offered as a second notation rather than the only one. Type annotations are optional where inference is local, but explicit annotations are required at function boundaries, which keeps signatures legible to a reader who did not watch the code being written. The intended user is therefore not an application team looking for a faster Python. It is someone studying how a language can be shaped around a non-human author, or someone who wants a small effectful language with a mechanised metatheory to experiment with.

Shadow tests are a warning, not a gate

The single most distinctive mechanism in NanoLang is the shadow block. The README's hello example places a shadow greet block directly under the function it tests, containing assert (== (greet "World") "Hello, World"), and main gets its own shadow main { assert true }. The compiler tracks shadow coverage and warns when a function lacks one. It does not fail the build on the absence. That gap matters more than it first appears. If the language's premise is that a machine writes the code, the test block is the part that constrains the machine, and a warning is a weak constraint: a model that emits a function without a shadow block still gets a compiled binary. The README is honest about this rather than overselling it, which is worth noting, but anyone adopting NanoLang for its test discipline should read the compiler's warning behaviour as advisory. The example also shows the shape of a shadow block: it is a named block, not an annotation, and its asserts are ordinary expressions evaluated against the function under the same name. That is a clean design for a small language, and it is the feature most likely to be copied elsewhere regardless of what happens to NanoLang itself.

Two execution paths: transpile to C, or run verified NanoISA bytecode

NanoLang has two backends and they are not equivalent in maturity. The README says the project "transpile[s] to C when you need native performance" and calls C "my production native path". The other path is NanoISA, described as a verified bytecode VM: a stack machine with 161 portable opcodes in an 8-bit opcode space, which verifies bytecode before running it and isolates FFI calls in a co-process. It can also run as a daemon. The shared IR story is that NanoLang and Nano Forth both lower to NanoISA, and that future LLVM, WebAssembly and JVM targets would translate from NanoISA so every frontend shares one typed and verified boundary. PTX, OpenCL and RISC-V are listed as direct experimental targets during that migration. Read that list as a roadmap, not a status report: nothing in the supplied material shows those general targets existing. The data flow for a NanoLang program is therefore source, then either C code generation with constant folding, dead-code elimination and profile-guided inlining on the native path, or lowering to NanoISA for the verified VM. The VM path is where the isolation claims live, and it is also where the project's security posture is concentrated.

Getting a binary: make build, then nanoc

The quick start is short and uses only the standard toolchain. Clone the repository, run make build, and the compiler lands at ./bin/nanoc. Compilation is ./bin/nanoc hello.nano -o hello, and the resulting binary runs directly. BSD users are told to use gmake instead of make, which is the only platform note in the visible README. The hello example exercises most of the surface syntax in twenty lines: fn with a typed return, string concatenation through the prefix form (+ "Hello, " name), a shadow block with assert, and a main returning int. The broader language overview shows let for immutable bindings, let mut for mutable ones, f-strings such as f"Result: {(add 2 3)}", the pipe operator with 5 |> add 3 |> double, and pattern matching with guards, or-patterns and a wildcard. Async functions lower to a CPS state machine at compile time. Algebraic effects use effect, perform and handle. For editor support, the repository ships a Language Server, a Debug Adapter Protocol server and a VS Code extension source tree under editors/vscode/ with semantic tokens, packaged with vsce package. There is also a browser playground built on CodeMirror 6 with a share permalink. None of this is verified here beyond what the README states; the commands are quoted as given.

The Coq suite is the part that is hard to fake

Formal verification claims are easy to make and hard to check, so the specific wording matters. The README says type soundness, progress and determinism are proved in Coq with no Axiom declarations, and that the big-step to small-step equivalence proof is complete and Admitted-free, including tuple value reconstruction in formal/Equivalence.v. It also says the proofs live in a formal/ directory with its own README. Those are checkable statements: Axiom and Admitted are keywords a reader can grep for, and the file path is named. This is the strongest claim in the repository because it is the one a sceptic can falsify in an afternoon by opening formal/Equivalence.v and searching for the two keywords. It is also the reason the project is worth more than its size suggests: a small effectful language with a mechanised metatheory is a useful artefact for people who study language design, independent of whether anyone writes production NanoLang. The caveat is scope. Proved core semantics do not extend to the C backend, the FFI boundary, the POSIX fabric, or the editor tooling. The proof covers the language's core, and the README is careful to say so.

The 4.x secure runtime, and the limits the README admits

Release 4.0 added what the README calls versioned service contracts, unforgeable capabilities, a POSIX fabric and a trap journal. Release 4.5 is described as a public cut covering 4.1 through 4.5, with Forth evidence, NSI, capabilities, the POSIX fabric, an isolated Nano Emacs and effects-to-policy. The documentation set is unusually explicit about what it does not claim, and that honesty is the most useful thing in the README. It states plainly: "I do not claim a kernel." It does not claim AES or PKI. The trap journal is described as a tested library that is not hooked into every VM trap in 4.5, which means the journal's coverage is partial by the project's own account. Nano Emacs is an SDL frame whose walker runs in bin/nano_emacs_worker, and the README says it does not claim GNU Emacs. The Forth session compiles colon definitions to verified NanoISA with vendored Jackson Core and Core Ext suites as evidence, and again the README says it does not claim a Standard System. Message catalogs cover six languages while JSON and TOON stay English, and the project does not call the system internationalized. Each of these is a boundary drawn in the documentation itself. For an evaluator, that list is more informative than any feature bullet, because it tells you exactly which claims have been deliberately withheld.

Where NanoLang is the wrong tool, and what to use instead

NanoLang is the wrong choice when you need a runtime you can put in front of untrusted traffic today. The trap journal is not wired into every VM trap in 4.5, the secure runtime hosts services on an ordinary kernel rather than isolating them from it, and the self-hosting bootstrap badge in the README reads "self-hosting in progress". A language that cannot yet compile itself is a language whose compiler is still a moving target, and the release cadence visible in the metadata (v3.5.0, v4.0.0, v4.5.0 within about two weeks in late August and early September 2026) suggests the surface is still shifting. If your actual requirement is a small language with a proved core and effect handlers, reach for a mature effectful language instead: OCaml 5 ships effect handlers as a supported feature and has decades of tooling behind it, while NanoLang's effect system is one item in a long feature list. If your requirement is sandboxed execution of untrusted code, WebAssembly with WASI is the comparison that matters, and the difference in approach is architectural: WASI defines a capability-oriented system interface that runtimes like Wasmtime enforce at the host boundary, whereas NanoLang's NSI contracts and capabilities are a design the project is still building out, with the trap journal explicitly not yet covering every trap. NanoLang's own README lists WebAssembly as a future target that would translate from NanoISA, which places it on the consuming side of that comparison for now.

Licence, maintenance and what to check before you commit

NanoLang is Apache-2.0, which permits commercial use, modification and redistribution with the usual conditions around notices and patent termination. This is not legal advice; read the LICENSE file in the repository if the terms matter to your organisation. The maintenance picture visible from the metadata is a single-author project with rapid releases and a last push in September 2026, so the practical question is not whether the licence allows adoption but whether one maintainer's release cadence matches your tolerance for churn. The upgrade cost is concentrated in the language surface: the jump from 4.0 to 4.5 added service contracts, capabilities, a POSIX fabric and a trap journal, which is a lot of new semantics across five minor versions, and the documentation index points to separate release notes for 4.0 and 4.5 rather than a single migration guide. Note also that the last public GitHub Release listed is v4.0.0 while 4.5 is documented as a public cut, so the packaged release and the documented state may not line up. Concretely, before adopting: check whether the self-hosting badge has changed, read docs/NSI.md against docs/RELEASE_4.5.md to see how far trap journal coverage actually extends, and run make build followed by ./bin/nanoc on a function with no shadow block to confirm whether the warning is as loud as advertised. If those three checks come back the way the README describes, you are looking at a serious research artefact. If they do not, you are looking at a thought exercise, and the repository's own topics list that possibility.

Editorial conclusion

Adopt NanoLang only if you are researching language design for machine authorship or want to read a Coq proof suite about a small effectful language; it is not a production runtime for services you depend on. Before building anything on it, verify that the self-hosting bootstrap badge has changed from in progress, check whether trap journal coverage in 4.5 matches docs/NSI.md, and confirm the shadow test warning behaviour on your own build rather than trusting the README.

Official sources

1. Issues
2. jordanhubbard/nanolang on GitHub
3. License: Apache-2.0
4. README
5. Releases