jordanhubbard / nanolang

NanoLang **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.** I transpile to C when you need native performance. I also provide my own virtual machine, NanoISA, which isolates dangerous external calls in a separate process. My core semantics are mechanically proved in Coq using zero axioms. Documentation **→ User Guide ←** - I provide a tutorial with examples you can execute. This is where I recommend you begin. **Additional Resources:** • Getting Started - A brief introduction to my environment. • Quick Reference - My syntax, summarized. • Language Specification - My complete technical definition. • NanoISA VM Architecture - How my virtual machine is structured. • Formal Verification - My Coq proof suite. • All Documentation - An index of everything I have to say. Quick Start **BSD users:** Use instead of . My Features • **Formally Proved Semantics** - I have proved my type soundness, progress, determinism, and semantic equivalence in Coq. I use zero axioms. • **NanoISA Virtual Machine** - I include a stack-based VM with 178 opcodes. It isolates FFI calls in a co-process and can run as a daemon. • **Automatic Memory Management (ARC)** - I use reference counting with zero overhead. I do not ask you to call free(). • **Machine-Led Optimization** - I profile myself and apply optimizations through an automated loop. • **Dual Compilation** - I transpile to C for performance or compile to NanoISA bytecode for sandboxed execution. • **Dual Notation** - I support both prefix and infix operators. My prefix calls are unambiguous. • **Mandatory Testing** - I refuse to compile a function unless you provide a test block for it. • **Static Typing** - I use static types and I can infer them when the meaning is clear. • **C Interop** - I communicate with C through modules. I can isolate these calls in a separate process to protect myself. Language Overview NanoISA Virtual Machine I provide a virtual machine as an alternative to C transpilation. **Architecture:** • **178 opcodes** - I use a stack machine with a hybrid instruction set. • **Co-process FFI** ( ) - I run external calls in a separate process. If they crash, I continue running. • **VM daemon** ( ) - I can run as a persistent process to start faster. • **Trap model** - I separate computation from I/O. This allows for future hardware acceleration. • **Reference-counted GC** - I manage memory deterministically. I release resources when they leave scope. I have documented my complete architecture in docs/NANOISA.md. Formal Verification My core semantics, which I call NanoCore, are mechanically proved in Coq. I use zero axioms. • **Type Soundness** - I have proved that well-typed programs do not get stuck. • **Determinism** - I have proved that evaluation produces exactly one result. • **Semantic Equivalence** - I have proved that my big-step and small-step semantics agree. My proved subset includes integers, booleans, strings, arrays, records, variants, pattern matching, closures, recursion, and mutable variables. I explain this further in formal/README.md. Building & Testing Examples & Interactive Tools **Web Playground** (I recommend this for learning my syntax): **Examples Browser** (This requires SDL2): **Individual examples:** I have categorized my games and demos in **examples/README.md**. Platform Support **I am fully supported on:** • Ubuntu 22.04+ (x86_64, ARM64) • macOS 14+ (Apple Silicon) • FreeBSD **Windows:** You may use me via WSL2 with Ubuntu. For LLM Training I was designed to be written by machines. • **MEMORY.md** - My training reference for patterns and idioms. • **spec.json** - My formal specification in machine-readable form. Contributing I have guidelines for those who wish to contribute in **CONTRIBUTING.md**. License I am released under the Apache License 2.0. See LICENSE for details. The Totally True and Not At All Embellished History of NanoLang The continuing adventures of Jordan Hubbard and Sir Reginald von Fluffington III > *Part 3 of an ongoing chronicle. ← Part 2: sheme | Part 4: Aviation →* > *Sir Reginald von Fluffington III appears throughout. He does not endorse any of it.* The programmer had, by this point, written a text editor in bash and a Scheme interpreter in bash, and had grown accustomed to things that arguably should not exist. He was sitting at his desk — Sir Reginald von Fluffington III occupying his preferred position on the keyboard, which was all of it — when the programmer had what he described as "a thought" and Sir Reginald later categorized, by aggressively ignoring it, as "a cry for help." "The problem," the programmer announced, to the room, to Sir Reginald, to the seventeen browser tabs he had open about formal verification, "is ambiguity. Every language I use is ambiguous. You write and nobody knows if it's a function call or a multiplication. You write and apparently this is a source of *controversy*. And don't get me started on implicit type coercion, which should be a war crime." Sir Reginald blinked once. He had heard variations of this speech before. They usually ended with something in the repository. "I need a language," the programmer said, "that machines can write. That has no ambiguity. That requires tests. That can be formally proved correct." He paused, with the expression of a man who has just located a loophole in reality. "And since no such language exists, I will build one." Sir Reginald pushed a pen off the desk. Slowly. Deliberately. With full awareness of the implications. What followed was a period the programmer later called "necessary" and Sir Reginald filed under "this again." A grammar was designed that distinguished prefix from infix without argument. A type system was specified with the kind of precision usually reserved for bridge construction. A virtual machine materialized, with 178 opcodes, which the programmer…