Introduction

Nova is a general-purpose systems programming language designed around three core ideas: algebraic effects, static contracts, and a lightweight M:N runtime. These three primitives address the most common sources of software bugs — hidden behavior, broken invariants, and accidental blocking — at the language level rather than as library conventions.

Nova targets the space where you need systems-level control (predictable performance, explicit resource management) but also want the safety guarantees that modern type theory enables. It is not a research language — it compiles to native code and is designed to build real software.

Installation

Nova is pre-alpha — build the nova CLI from source (stable Rust 1.85+; a C toolchain — Clang, MSVC, or GCC — is needed to compile programs):

git clone https://github.com/nv-lang/nova
cd nova/nova-cli
cargo build --release

The nova CLI lands at nova-cli/target/release/nova; add it to your PATH. Full step-by-step on the install page.

System requirements: Linux x86-64 or ARM64, macOS 12+. Windows support is planned.

Hello, World

Create a file named hello.nv:

fn main() {
    println("Hello, World!")
}

Compile and run:

nova build hello.nv
./hello

The program entry point is fn main(); println writes a line to standard output.

Next steps

The language guide sections below explain effects, contracts, the type system, and the concurrency model in detail. For the formal treatment of every language construct, see the Language Specification.

If you prefer to learn by reading code, the examples directory on GitHub has annotated programs covering the main language features.

Effects

Every function that performs a side effect declares it in its type — between the parameter list and the return arrow. The available built-in effects are:

• Io — standard input/output (console, files)
• Net — network access (sockets, DNS)
• Http — HTTP client and server primitives
• Db — database connections
• Fs — filesystem access
• Log — structured logging
• Rand — random number generation
• Time — wall-clock and monotonic time
• Mut — mutation of shared state (implicit in local scope)

User-defined effects are supported. You declare an effect interface, provide a handler, and inject it at the call boundary — no global state, no hidden dependency injection framework.

type Cache effect {
    get(key str) -> Option[[]u8]
    set(key str, val []u8) -> ()
}

// Cache and Db effects are looked up from the active with-scope.
fn get_profile(user_id u64) Cache Db -> Profile
{
    let key = "profile:${user_id}"
    if let Some(raw) = Cache.get(key) {
        return Profile.decode(raw)
    }
    let rows = Db.query(sql`SELECT * FROM profiles WHERE id = ${user_id}`)
    let p = Profile.from_row(rows[0])
    Cache.set(key, p.encode())
    p
}

Contracts

Nova contracts express machine-checkable intent directly on function boundaries. Three kinds:

• requires <expr> — precondition; must hold when the caller invokes the function
• ensures <expr> — postcondition; must hold when the function returns normally
• invariant <expr> — type invariant; must hold for every value of a type

The compiler checks contracts via an SMT solver at compile time — proven contracts are erased in release builds at zero runtime cost. If the solver cannot decide, the contract automatically falls back to a runtime assertion in debug builds. The #must_verify attribute on a function requires static proof — compilation fails if the solver cannot prove it.

fn sqrt(x f64) -> f64
    requires x >= 0.0
    ensures  result >= 0.0
{
    // compiler knows x is non-negative here
    x.sqrt()
}

Types

Nova has a static, inferred type system with algebraic data types, generics, and protocols.

• Primitives: int, i8 i16 i32 i64, u8 u16 u32 u64, f32 f64, bool, char, str
• Algebraic types: one type keyword — type X { ... } for records (products), type X | A | B for sum types (tagged unions); no struct/enum
• Option and Result: Option[T] and Result[T, E] are built-in sum types — no null
• Generics: parametric polymorphism with protocol bounds
• Protocols: structural interfaces — any type with matching methods conforms automatically

Concurrency

Nova's runtime multiplexes fibers — lightweight threads scheduled by the runtime — across OS threads using a work-stealing scheduler. You spawn a fiber with spawn and communicate over channels:

// parallel for runs each iteration as a fiber, collects results
let squares = parallel for i in 0..8 { i * i }
// squares == [0, 1, 4, 9, 16, 25, 36, 49]

// spawn for fire-and-forget work; supervised waits for all fibers
let mut count = 0
supervised {
    spawn { count = count + 1 }
    spawn { count = count + 1 }
}
// count == 2

Memory

Nova uses managed memory by default. The current runtime integrates Boehm-Demers-Weiser GC; a concurrent, generational GC is on the roadmap.

For latency-sensitive code, annotate a scope or function with realtime nogc to opt out of GC pauses. The compiler enforces that no GC-managed allocations occur inside such scopes.

fn process_audio_frame(frame AudioFrame) Dsp -> AudioFrame {
    realtime nogc {
        // only stack allocation allowed here
        frame.apply_eq()
    }
}

Standard Library

core

The core module is always in scope. It provides the fundamental types (Option, Result, Vec, Map, Set, str, []u8), basic protocols (Eq, Ord, Hash, Display, Debug), and the macro system.

io

Standard input, output, and file I/O. Requires the Io effect. Includes stdin(), stdout(), stderr(), File.open(), File.create(), and buffered readers/writers.

net

TCP and UDP sockets, DNS resolution, and TLS. Requires the Net effect. All socket operations are fiber-aware — blocking calls yield to the scheduler transparently.

collections

Extended data structures beyond the core: BTreeMap, BTreeSet, LinkedList, Deque, PriorityQueue, and persistent/immutable variants.