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

The fastest way to get started is the installer script:

curl -sSf https://nv-lang.org/install.sh | sh

This installs the nova compiler and the nv package manager to ~/.nova/bin. Add that directory to your PATH:

export PATH="$HOME/.nova/bin:$PATH"

Alternatively, download a pre-built binary from the releases page or build the compiler from source by following the contributor guide.

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

Hello, World

Create a file named hello.nv:

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

Compile and run:

nova build hello.nv
./hello

Notice that main declares Io before the return arrow — even the top-level entry point is honest about its effects. () is the unit return type (no value returned).

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[bytes]
    set(key str, val bytes, ttl Duration) -> ()
}

fn get_profile(user_id u64) Cache Db -> Profile
{
    let key = format("profile:{}", user_id)
    if let Some(raw) = cache.get(key) {
        return Profile.decode(raw)
    }
    let p = db.load_profile(user_id)
    cache.set(key, p.encode(), Duration.minutes(5))
    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

Contracts are checked in three modes: static (SMT solver, compile-time, no cost), dynamic (runtime assertion in debug builds), and erased (zero overhead in release builds). The mode is selected per-clause with an optional @static, @runtime, or @erased attribute; the default is @static with automatic fallback to dynamic if the solver cannot decide.

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

Types

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

• Primitives: bool, i8–i128, u8–u128, f32, f64, str, bytes
• Algebraic types: struct for products, enum for tagged unions
• Option and Result: Option[T] and Result[T, E] are built-in enums, no null
• Generics: parametric polymorphism with trait bounds
• Traits: structural interfaces with default implementations

Concurrency

Nova's runtime multiplexes fibers (lightweight green threads) across OS threads using a work-stealing scheduler. You spawn a fiber with spawn and communicate over channels:

fn process_batch(items []Item) Db -> []Result[Output, Err]
{
    let (tx, rx) = channel.bounded(items.len())
    for item in items {
        let tx = tx.clone()
        spawn { tx.send(process_one(item)) }
    }
    rx.collect(items.len())
}

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, bytes), basic traits (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.