Proofs instead of guesses
Every array index, division and range is a proof obligation, discharged at compile time over integer constraints. An unproven obligation is a compile error with a counterexample, never a silent runtime check.
Why Neo
Languages were designed for people. Models need something else.
People need ergonomics, readability and freedom. Models need a small grammar, errors they can parse, and a compiler that refuses to guess. Neo is built for the second list, then compiled to native code that outruns optimised Rust.
What goes wrong when models write code
Models write plausible code fast. Their mistakes are the ones that pass review and fail later: an index one past the end, a divisor that is sometimes zero, an integer that overflows on real data, input that was never validated. Most languages find these at run time, if at all, and explain them in prose written for people.
Neo moves all of them to compile time. Every index, division and range is an obligation the compiler must prove. What it cannot prove comes back as data, with a counterexample and the fixes that would close it, so the model can repair its own code before anything runs.
Diagnostics are data
neo check answers in JSON: node hash, position, normalised goal, status, counterexample and suggested fixes. An agent acts on it without parsing prose.
Code named by structure
Functions and nodes are named by the hash of their structure, with variables as binder distances. Renaming changes no hash, and builds are cached by program hash.
No lifetimes to annotate
The compiler owns memory. Ownership moves along a uniqueness discipline, and updates happen in place when a buffer is unique. No GC, no reference counts, no borrow annotations to get wrong.
Parallel by default
Every sum(i in a..b) and arr(i in a..b) is outlined and spread across cores. A scalar sum, even with a data-dependent loop inside, runs 16 iterations at a time in vector lanes.
Pure unless declared
Ordinary functions are pure; side effects live in effect fn. A pure call with literal arguments is run by the compiler and replaced by its result.
One shape for everything
Every construct is an expression: let … in, if … then … else, loop … while … next … yield. A small, regular grammar leaves a model fewer ways to be wrong.
Native, static, self-contained
LLVM -O3 native code. Linux builds are static ELF files with no interpreter, shared libraries or libc. The allocator, scheduler and HTTP stack are written in Neo itself.
The loop
An agent works against the compiler, not against a test suite it has to guess.
- 01
Write
The model writes small, typed, pure functions with refinements on their inputs.
- 02
Check
neo checkreturns every proof obligation as JSON, each one proven or with a counterexample. - 03
Fix
The suggested fixes are concrete: a guard, a check, or a sharper refinement. Apply, re-check.
- 04
Ship
neo buildemits one native binary. Nothing to install next to it.
What a model gets, compared
The same mistakes, and where each language catches them.
| Neo | Rust | Go | Python | |
|---|---|---|---|---|
| Array index out of range | Compile error with a counterexample | Runtime panic | Runtime panic | Runtime exception |
| Division by zero | Compile error unless proven non-zero | Runtime panic | Runtime panic | Runtime exception |
| Integer overflow | Checked; traps unless proven safe | Panics in debug, wraps in release | Wraps silently | Arbitrary precision |
| Memory | Compiler-owned, nothing to annotate | Ownership and lifetimes | Garbage collector | Garbage collector |
| Compiler feedback | JSON obligations with counterexamples and fixes | Text or JSON diagnostics | Text | Tracebacks at run time |
| Parallel loops | Automatic for comprehensions | Opt in (threads, rayon) | Opt in (goroutines) | Opt in (processes) |
| Shipping | One static binary, no libc | Native binary | Native binary | Interpreter and packages |
Where it stands
An early release, with real numbers and an honest list of what is missing.
Works today
- Refinement checker with JSON obligations and counterexamples
- Native code through LLVM, static Linux binaries
- Automatic parallel regions and vectorised loops
- HTTP server runtime, JSON, maps, files, processes, TLS (experimental)
- Packages, formatter, test runner, language server
Targets
- x86-64 Linux
- ARM64 Linux
- ARM64 macOS (loads libSystem, as Apple requires)
Not yet
- Self-hosting: the compiler is written in Python
- Building without Clang/LLVM
- Windows and x86-64 macOS