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. Side effects are visible in types; optional contracts are checked where the compiler can prove them.
// 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 express optional contracts. Oracle's default verifier handles trivial cases; richer proofs require the optional Z3 backend. Unproven conditions use runtime checks in supported modes; these checks are stripped 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). #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. Oracle proves what its selected backend can handle; runtime fallback checks are stripped in release builds.
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
Start with an Oracle 0.1.0 alpha binary bundle for Windows or Linux x86_64. A system C compiler is required; you do not need to build the Rust compiler first.
Download Oracle and view Carina
Setup instructions & first program · Verify downloads with the release's SHA256SUMS
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.