A language that
says what it means
Nova is a general-purpose systems language built around algebraic effects, static contracts, and an M:N concurrency runtime. Every side effect is declared. Every invariant is verified.
// Algebraic effects in signatures
fn fetch_user(id int) Db Log -> Result[User, NotFound]
requires id > 0
{
Log.info("fetching ${id}")
match Db.find_user(id) {
Some(u) => Ok(u)
None => Err(NotFound)
}
}Why Nova
Simple rules, strong guarantees
Three language-level primitives that change how you reason about programs.
Algebraic Effects
Network, I/O, randomness, time, and mutation appear directly in the function's type — between the parameters and the return arrow. No hidden control flow. No surprise await. The caller always knows what a function does.
Static Contracts
requires, ensures, and invariant clauses are checked by an SMT solver at compile time. Proven contracts are erased at zero cost; unproven ones remain fail-fast runtime checks — in release builds too.
M:N Runtime
Fibers multiplexed onto OS threads with a work-stealing scheduler. Managed memory by default (Boehm GC today, concurrent GC on the roadmap). #realtime functions for latency-sensitive paths; a GC-free nogc mode is on the roadmap.
Built for the AI era
AI writes the code. Humans review it.
More and more code is generated by AI. But humans still review it. Nova is the first language explicitly designed for this: side effects are declared in the signature, so review stays local — you read the function, not the entire call graph.
Side effects appear in the type signature — between parameters and the return arrow. Review stays local: you know what a function does without reading its body.
Swap any dependency via a with block — the same business logic runs against a real database in production and an in-memory handler in tests. No mocking library needed.
parallel for runs iterations concurrently with structured scoping. Functions don't need an async keyword — suspension is ambient. No function colouring.
Contracts are optional — add requires and ensures where you need them. The compiler proves them statically when it can; what it can't prove becomes a runtime check.
Effects in action
Every dependency visible at a glance
The first line — fn main() Net Time Detach — declares everything this program does to the outside world: the network (Net), the clock (Time), detached connection fibers (Detach). Effects sit between the parameter list and the return arrow. Nothing is implicit.
// HTTP server — every dependency in the signature
fn main() Net Time Detach -> () {
ro app = Router.new()
.get("/users/{id}", get_user)!!
.post("/users", create_user)!!
consume listener = TcpListener.bind("0.0.0.0:8080")!!
serve_router(listener, app, ServerPolicy.new())
}Try Nova
Nova is pre-alpha — build the compiler from source. Full steps on the install page.
git clone https://github.com/nv-lang/nova && cd nova/nova-cli && cargo build --release
Builds the nova CLI · prerequisites & first program
Join the conversation
Nova is open source and built in public. Follow the design process, file bugs, contribute code, or just watch the compiler grow.