Write, check, ship.

Install

One command installs Neo in ~/.neo and runs neo doctor, which names anything missing and the command that installs it. Then add ~/.neo/bin to your PATH, as the installer says.

$ curl -fsSL https://neolang.dev/install.sh | sh

Building Neo needs Python 3.11 or newer, Clang/LLVM and binutils. It targets x86-64 Linux, ARM64 Linux and ARM64 macOS. Linux binaries are static: no libc, loader or shared libraries.

$ neo init my-app
$ cd my-app
$ neo run

neo init creates a project with a manifest that names the entry file; neo build and neo run use it when no file is given.

For agents: skills.md

It is written for models, not people: short rules, exact commands and real compiler output, with nothing to skim past.

Your first program

A main without effects returns its output; the runtime prints it.

fn main () -> Arr u8 _ = "Hello, World!\n"

$ neo build hello.neo -o hello
$ ./hello
Hello, World!

The check loop

neo check proves every array index, division and range, and prints one JSON entry per obligation. Anything it cannot prove is a compile error with a counterexample and suggested fixes; it never inserts a silent runtime check. A file without main is a library: add --library.

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

$ neo check --library at.neo

{ "fn": "at", "node": "0d1e7a0fe59c", "kind": "bounds",
  "goal": "0 <= i && i < len(a)", "status": "unproven",
  "counterexample": { "i": -1, "n": 0 },
  "fixes": ["guard: if 0 <= i && i < len(a) then … else …",
            "check 0 <= i && i < len(a) in …",
            "refine the index parameter, e.g. i : i64{0 <= i, i < n}"] }

Refine the parameter and the obligation is proven; every caller now has to prove its own precondition:

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

bounds

An array index is in range.

division

A divisor is not zero.

precondition

A call satisfies the callee's refinements.

invariant

A loop state's refinement holds initially and is preserved.

check

An explicit check, kept as a runtime test.

The node hash names the expression by its structure, so it survives renames and edits elsewhere: use it to follow one obligation across iterations.

Syntax basics

Everything is an expression; there are no statements or early returns. Comments start with ;.

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

fn sum_to (n : i64{n >= 0}) -> i64
  = let total = sum(i in 0..n) i in total

• Types: i64, i32, u8, f64, bool, unit. Arrays are Arr T n, where n names the length; _ means unknown. Strings are Arr u8 _.
• Refinements: i : i64{0 <= i, i < n}. Commas mean "and"; every caller must prove them.
• Records: type Body = { x : f64, m : f64 }, built with Body { x = 1.0, m = 2.0 } and updated with b with { x = 0.0 }.
• Comprehensions: arr(i in 0..n) e builds an array and sum(i in 0..n) e reduces. Both run across cores.

Loops carry explicit state. next gives every state variable its new value, in order; yield is the result:

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

Effects

A plain fn is pure, and pure calls with literal arguments run at compile time. Side effects live in effect functions that name their capabilities, checked through every call: fs, net, time, env, process and unsafe.

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()

Refinements and comprehension bodies can never perform effects.

An HTTP server

A server is one call. The handler is a pure function from request bytes to response bytes; the runtime handles sockets, framing, pipelining and one worker per core.

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)

$ neo run server.neo -- 8080

Standard library

Import a relative file with import "helpers.neo" and the standard library with import "std:json". Declarations are public unless marked private.

Command line