Top AI Repos — open-source AI, indexed and scored
Top AI Repos tracks AI repositories on GitHub and answers two different questions about each one: is it moving right now, and would you bet a product on it.
Top AI Repos tracks AI repositories on GitHub and answers two different questions about each one: is it moving right now, and would you bet a product on it.
A tiny experimental language designed to be targeted by coding LLMs
| Date | Stars |
|---|---|
| 2026-07-24 | 612 |
| 2026-07-25 | 612 |
| 2026-07-28 | 613 |
| 2026-07-30 | 613 |
| 2026-08-06 | 613 |
Today
— stars today
This week
— stars this week
This month
— stars this month
Momentum
15.0
growth rate 0.00%/day
# NanoLang
[](https://github.com/jordanhubbard/nanolang/actions/workflows/ci.yml)
**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 — type soundness, progress, determinism, and the big-step ↔ small-step equivalence proof are all complete and `Admitted`-free.
## Documentation
**→ [User Guide](https://jordanhubbard.github.io/nanolang/) ←** - I provide a tutorial with examples you can execute. This is where I recommend you begin.
**Additional Resources:**
- [Getting Started](docs/GETTING_STARTED.md) - A brief introduction to my environment.
- [Quick Reference](docs/QUICK_REFERENCE.md) - My syntax, summarized.
- [Language Specification](docs/SPECIFICATION.md) - My complete technical definition.
- [NanoISA VM Architecture](docs/NANOISA.md) - How my virtual machine is structured.
- [Formal Verification](formal/README.md) - My Coq proof suite.
- [All Documentation](docs/DOCS_INDEX.md) - An index of everything I have to say.
## Quick Start
```bash
# Clone and build
git clone https://github.com/jordanhubbard/nanolang.git
cd nanolang
make build
# Create hello.nano
cat > hello.nano << 'EOF'
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 }
EOF
# Compile and run
./bin/nanoc hello.nano -o hello
./hello
```
**BSD users:** Use `gmake` instead of `make`.
## My Features
- **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/Equivalence.v`).
- **NanoISA Virtual Machine** - I include a stack-based VM with ~94 defined opcodes in an 8-bit opcode space. It isolates FFI calls in a co-process and can run as a daemon.
- **Automatic Memory Management** - I use reference counting so you never call `free()`. Heap allocations carry a small per-retain/release cost; pauses are deterministic. Note: reference *cycles* are not automatically reclaimed (there is no tracing cycle collector yet) — break cycles manually to avoid leaks.
- **Machine-Led Optimization** - I run constant folding and dead-code elimination on the AST before code generation. I also support profile-guided inlining: build with profiling, run a representative workload to produce a `.nano.prof`, then recompile with `--pgo <path>` to apply hot-path inlining.
- **Multi-Target Compilation** - I transpile to C for native performance and also emit WebAssembly (`--target wasm`), LLVM IR (`--target llvm`), PTX/CUDA (`--target ptx`), or RISC-V assembly (`--target riscv`). Each WASM output gets a source-map sidecar and can be signed with Ed25519. The C backend is the production path; the experimental WASM and LLVM backends reject the constructs they cannot yet lower with an explicit compile error rather than emitting a broken binary. The WASM backend rejects string literals, struct literals, union constructs, field access, match expressions, array literals, tuple literals, and the I/O and string-conversion builtins (these need linear memory plus a WASI host). The LLVM backend lowers string literals but rejects struct literals, union constructs, field access, match expressions, array literals, tuple literals, closures with captured variables, effects, and `par`Excerpt of 16,493 characters
Read on GitHub
2.1k
20
1
Would you bet a product on this? Bounded 0–100 and slow moving.
matched fp:d3e2f6b6b52f1894, topic:vibe-coding, readme:code generation
matched fp:d3e2f6b6b52f1894, topic:llm