Reads like the math. Checks like a proof.

Functions are expressions

A function is a name, typed parameters, a result type and one expression. There are no statements, no mutation of variables and no early returns, so every function reads top to bottom and means exactly one thing.

fn square (x : i64) -> i64 = x * x

fn clamp (v : i64, lo : i64, hi : i64) -> i64
  = if v < lo then lo else if v > hi then hi else v

let name = value in body binds an immutable name. Comments start with ;.

Refinements and proofs

A refinement narrows a type with facts the compiler must prove: i64{0 <= i, i < n}. Arrays carry their length as a name, Arr T n, so facts can mention it. Inside the function the facts are known; at every call site they become obligations.

fn at (a : Arr i64 n, i : i64{0 <= i, i < n}) -> i64 = a[i]

fn main () -> i64 = at(arr(k in 0..4) k * k, 2)

The compiler discharges 0 <= i && i < len(a) inside at, and proves 2 < 4 at the call. Remove the refinement and a[i] becomes a compile error with a counterexample. check cond in body keeps a deliberate runtime test where a proof is not possible.

Loops with explicit state

A loop names its state, a condition, the next value of every state variable and its result. Refinements on loop state become invariants the compiler checks initially and after each step.

fn starts_with (a : Arr u8 n, b : Arr u8 m) -> bool
  = m <= n && loop (i : i64{i >= 0} = 0, ok = true)
                while ok && i < m
                next (i + 1, a[i] == b[i])
                yield ok

Both indexes are proven from i < m <= n; no bounds check is emitted.

Records and layout

Records are values. with builds an updated copy. The compiler chooses their layout: an Arr Body n of numeric records is stored as one buffer of field planes, so loops stream contiguous memory and vectorise while the program only ever sees records.

type Body = { x : f64, y : f64, z : f64, vx : f64, vy : f64, vz : f64, m : f64 }

fn drift (bs : Arr Body n, dt : f64) -> Arr Body n
  = arr(i in 0..n) let b = bs[i] in
      b with { x = b.x + b.vx * dt, y = b.y + b.vy * dt, z = b.z + b.vz * dt }

Parallel by default

arr(i in a..b) e builds an array and sum(i in a..b) e reduces. Their bodies are pure, so the compiler outlines them and runs them across cores, with no threads, locks or annotations. Small ranges stay sequential to avoid the overhead.

fn accel (bs : Arr Body n, i : i64{0 <= i, i < n}) -> Vec3
  = let xi = bs[i].x in let yi = bs[i].y in let zi = bs[i].z in
    sum(j in 0..n)
      let dx = bs[j].x - xi in let dy = bs[j].y - yi in let dz = bs[j].z - zi in
      let d2 = dx * dx + dy * dy + dz * dz + 0.01 in
      let inv = bs[j].m / (d2 * sqrt(d2)) in
      Vec3 { x = dx * inv, y = dy * inv, z = dz * inv }

A scalar sum also runs 16 iterations at a time in vector lanes, even when each iteration contains a data-dependent loop, a case LLVM cannot vectorise on its own.

Memory without annotations

The compiler owns memory. Arrays and records have value semantics; an array used once as a whole moves instead of copying, and set(a, i, v) then updates it in place. Whatever still owns a buffer at the end of its scope frees it.

There is no garbage collector, no reference counting and nothing to annotate: no lifetimes, no borrow markers. The allocator is written in Neo itself, over memory mapped straight from the kernel.

Generics, enums and Result

Records and functions take type parameters, specialised at compile time. Enums need exhaustive match.

import "std:option"
type Box<T> = { value:T }
fn identity<T>(value:T) -> T = value
fn main() -> i64
  = let box=Box::<i64> { value=identity(42) } in
    match Some(box.value) { None => 0, Some(value) => value }

Errors are values. let x = f()? in rest continues with the success value or returns the error; it is an ordinary branch, not an exception.

import "std:result"
fn positive(value:i64) -> Result<i64,Arr u8 _>
  = if value>0 then Ok::<i64,Arr u8 _>(value) else Err::<i64,Arr u8 _>("negative")
fn convert(value:i64) -> Result<Arr u8 _,Arr u8 _>
  = let number=positive(value)? in
    check number>0 in Ok::<Arr u8 _,Arr u8 _>("done")

Effects and capabilities

Plain functions are pure, and pure calls with literal arguments run at compile time. Anything that touches the world is an effect function that names its capabilities (fs, net, time, env, process, unsafe), checked through every call. Resources like files are scoped with using and released exactly once.

import "std:file"
effect(fs) fn main() -> unit
  = using file=open_file("/dev/null",0) in
    let status=file_status(file) in check status.ok in
    let result=read_file(file,32) in check result.ok in
    let output=print_out(concat("read ",int_text(len(result.value))," bytes\n")) in noop()

Modules and the standard library

import "helpers.neo" loads a file; import "helpers.neo" as helpers qualifies its names. The standard library covers strings, strict JSON, files, HTTP server and client, DNS, vectors and maps, Option and Result, channels, time and experimental TLS.

Module list →

Runtime and binaries

Neo compiles through LLVM to one native executable. On Linux it is static, with no libc, loader or shared libraries: the runtime talks to the kernel directly. The HTTP server is part of that runtime: one worker per core, io_uring on x86-64 Linux, pipelining and batched responses, all behind a single call with a pure handler.

fn handle (req : Arr u8 n) -> Arr u8 _
  = "HTTP/1.1 200 OK\r\nContent-Length: 13\r\n\r\nHello, World!"

effect fn main (port : i64{port > 0, port < 65536}) -> i64 = serve(port, handle)

How fast it is →