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
ensures result.is_ok() ==> result.unwrap().id == id
{
Log.info("fetching ${id}")
match Db.find_user(id) {
Some(u) => Ok(u)
None => Err(NotFound)
}
}Why Nova
Three language-level primitives that change how you reason about programs.
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.
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.
Go-style 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.
Effects in action
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())
}Install the compiler with a single command. Runs on Linux and macOS.
curl -sSf https://nv-lang.org/install.sh | sh
Nova is open source and built in public. Follow the design process, file bugs, contribute code, or just watch the compiler grow.