jordanhubbard / nanolang

What it does

• Formally Proved Semantics. I have proved type soundness, progress, and determinism in Coq with no Axiom declarations. The big-step ↔ small-step equivalence proof is complete and Admitted-free (including tuple value reconstruction in formal
• NanoISA Virtual Machine. I include a stack-based VM with 161 portable opcodes in an 8-bit opcode space. It isolates FFI calls in a co-process and can run as a daemon. Bytecode is verified before it runs.
• Automatic Memory Management. I use reference counting so you never call free(). Heap allocations carry a small per-retain/release cost; pauses are deterministic. NanoVM also collects reference cycles (src/nanovm/heap_cycles.c); generated C
• Machine-Led Optimization. I run constant folding and dead-code elimination before code generation. I also support profile-guided inlining on my native C path.
• Shared IR. I lower NanoLang and Nano Forth to NanoISA. C remains my production native path. Future LLVM, WebAssembly, JVM, and other general targets translate from NanoISA so every frontend shares one typed and verified boundary. PTX, Open