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 u64) 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 when possible, verified at runtime in debug mode, and erased at zero cost in release builds.
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). Use realtime nogc for latency-sensitive paths.
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 HTTP server's signature tells you it binds to the network (Net), speaks HTTP (Http), and writes logs (Log) — effects appear between the parameter list and the return arrow. Nothing is implicit.
// HTTP server — effects track every dependency
fn serve_api() Net Http Log -> ()
{
let router = Router.new()
.route(Get, "/users/:id", get_user)
.route(Post, "/users", create_user)
Http.serve("0.0.0.0:8080", router.dispatch())
}Try Nova
Install the compiler with a single command — or pick your platform on the install page.
curl -sSf https://nv-lang.org/install.sh | sh
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.