This document covers the surface language: syntax, semantics, modules, and the intentional omissions.
For constructor-specific rules, see constructors.md.
For namespaces, services, and standard library APIs, see services.md.
For Oracle laws and trace assertions over classified effects, see oracle.md.
Primitive: Int, Float, String, Bool, Unit
Compound: Result<T, E>, Option<T>, List<T>, Vector<T>, Map<K, V>, (A, B, ...), Fn(A) -> B, Fn(A) -> B ! [Effect]
Each primitive has exactly one spelling — the string type is written String, never abbreviated.
There is no dedicated Set type — use Map<T, Unit> (see Sets below).
User-defined sum types: type Shape → Shape.Circle(Float), Shape.Rect(Float, Float)
User-defined product types: record User → User(name = "Alice", age = 30), u.name
Declare them with the type name on its own line and the members indented beneath — one variant per line for a sum type, one field: Type per line for a record:
type Shape // sum type
Circle(Float)
Rect(Float, Float)
Point // zero-arg variant — a bare singleton (Shape.Point)
record User // product type
name: String
age: Int
Unit means "no meaningful value". It is similar to void, but still a real type; diagnostics render the value as (). Effectful functions such as Console.print commonly return Unit.
All bindings are immutable. No val/var keywords — they are parse errors.
name = "Alice"
age: Int = 30
xs: List<Int> = []
Optional type annotation provides a hint to the type checker; the annotation wins over inference when both are compatible. Binding to an empty list literal without a type annotation (x = []) is a type error.
Duplicate binding of the same name in the same scope is a type error.
Arithmetic: +, -, * — operands must match (Int+Int, Float+Float, String+String). No implicit promotion; use Float.fromInt / Int.fromFloat to convert. The / operator is Float-only; integer / is a type error. For integers use Int.div(a, b) : Result<Int, String> (Euclidean; b == 0 → Result.Err) and Int.mod(a, b) : Result<Int, String> — there is no integer %. Int is arbitrary-precision (ℤ): no overflow, no wraparound.
Bit-level operations live in the Bits namespace, not in the operator set: Bits.and, Bits.or, Bits.xor, Bits.not are Int -> Int under infinite two's complement (Bits.not(x) == -x - 1, Bits.and(-1, x) == x), and Bits.shiftLeft(x, n) / Bits.shiftRight(x, n) / Bits.low(x, width) are x * 2^n / floor(x / 2^n) / x mod 2^width, returning Result<Int, String> because a negative count is refused. Bits is a namespace, not a type: nothing here is a machine word, and Int still never overflows or wraps — width is requested explicitly through Bits.low, never implied. See docs/services.md.
Literal-divisor discharge: when the divisor of Int.div / Int.mod is a syntactic nonzero integer literal — Int.div(x, 2), Int.mod(x, -3) — the call cannot fail, so it types as plain Int and every backend emits the division directly (no Result, no unwrapping). The boundary is exactly "a syntactic integer literal other than 0, optionally under one unary minus": a 0 literal, an identifier, a named constant, or a constant expression like 8 + 8 all keep the Result<Int, String> type unchanged. Parentheses are transparent here, because the parser erases them around a single expression: (16), (-16) and -(16) are the same syntax tree as 16 and -16, so all three discharge — while (0) is still zero and (k) is still an identifier, and both keep the Result type. This is a typing rule for these two functions only, not a general constant-propagation or refinement mechanism.
Literal smart-constructor discharge: the same idea extends to a validating smart constructor over a List<Int> carrier — the shape stdlib/bytes.av uses. When the argument is a syntactic list of integer literals and every element is inside the interval the refinement itself proves, the call cannot reach its Result.Err branch, so it types as the refined type and constructs the value directly: Bytes.fromList([0, 10, 255]) : Bytes, no ? and no match. The empty list Bytes.fromList([]) discharges too. The boundary is narrow and entirely syntactic on the argument side: there must be exactly one argument, it must be a list literal written out at the call site, and every element must be a plain integer literal with at most one unary minus. What decides is the function the call resolves to, never how it is spelled: Bytes.fromList(...) from outside and a bare fromList(...) inside the defining module both reach the constructor and both discharge, while a module that declares its own fromList shadows the imported one as usual — that call means the local function and is not discharged at all. Everything else keeps Result<Bytes, String> unchanged — an identifier (Bytes.fromList(values)), a computed list (Bytes.fromList(List.concat(a, b))), a computed element (Bytes.fromList([n * 2])), an out-of-range literal (Bytes.fromList([65, 256])), a negative one (Bytes.fromList([-1])), or a literal beyond i64. The bound is never hardcoded: it is read off the refinement's own validating predicate, so a user-defined refinement with a different range discharges against that range, and a record with no smart constructor never discharges at all. Programs run under --self-host are refused with an explicit error when they contain a discharged call, because the self-hosted resolver does not yet carry the rule.
Unary minus negates a numeric expression: -n (equivalent to 0 - n), and numeric literals may be written negative (-3, -1.5).
Comparison: ==, !=, <, >, <=, >=.
Error propagation: expr? — unwraps Result.Ok, propagates Result.Err as a RuntimeError.
Independent products: (a, b)! — product of independent computations. (a, b)?! — same, with Result unwrapping (all must succeed or first error propagates). Elements cannot reference each other; independence is structural. Composes recursively for fan-out parallelism. See independence.md.
Expressions inside {} are evaluated at runtime:
greeting = "Hello, {name}! You are {age} years old."
Interpolation renders primitives only: an embedded expression must be an Int, a Float, a Bool or a String. Embedding anything else — a list, a record, a tuple, a Map, an Option/Result, a Vector, a refinement or other named type — is a type error, because an interpolation site is a display site and Aver requires every conversion to String to be named in the source. There is no built-in renderer for compound values and none is planned: write a function that returns String and interpolate its result ("cart: {cartLine(item)}"), or convert at the call site with an explicit conversion such as String.fromInt(n). The rule is the same one that makes Console.print(list) a type error; the interpolated form is only sugar over the same display.
An embed whose type inference never pinned is rejected too, with a diagnostic saying the type could not be determined. This happens when the value flows from a still-open generic — matching on a bare Option.None or a bare [] binds the arm's variable to a type nothing in the program fixes. Give the subject a concrete type (match someOption where someOption: Option<Int>) and the embed becomes an ordinary primitive or an ordinary compound, with the ordinary answer in each case.
UpperCamel callee = constructor, lowerCamel = function call. Records use named args (User(name = "A", age = 1)), variants use positional args (Shape.Circle(3.14)), zero-arg constructors are bare singletons (Option.None, Shape.Point).
All constructors are namespaced — no bare Ok/Err/Some/None:
Result.Ok(42)
Result.Err("not found")
Option.Some("hello")
Option.None
match is the only branching construct (no if/else). Patterns:
match value
42 -> "exact" // Int literal
"verack" -> "known command" // String literal
_ -> "anything" // wildcard
x -> "bound to {x}" // identifier binding
[] -> "empty list" // empty list
[h, ..t] -> "head {h}, {List.len(t)} more" // list cons
Result.Ok(v) -> "success: {v}" // constructor
Result.Err(e) -> "error: {e}"
Shape.Circle(r) -> "circle r={r}"
Shape.Point -> "point"
(a, b) -> "pair: {a}, {b}" // tuple destructuring
((x, y), z) -> "nested: {x}" // nested tuple
Constructor patterns are always qualified (Result.Ok, Option.None, Shape.Circle). Records do not support positional destructuring in patterns; bind the whole record and use field access (user.name, user.age).
Nested match in match arms is supported. Arm body must follow -> on the same line — extract complex expressions into a named function.
An arm may be a literal instead of a binding; it fires when the subject equals it. This is how you dispatch on a command name or a tag byte — there is no else if to reach for, and no reason to spread the decision over a chain of single-purpose helper functions:
fn handle(command: String) -> Int
? "Dispatch on the wire command name."
match command
"verack" -> 1
"version" -> 2
"inv" -> 3
"tx" -> 4
_ -> 0
fn varIntWidth(head: Int) -> Int
? "253 introduces two more bytes, 254 four, 255 eight."
match head
253 -> 2
254 -> 4
255 -> 8
_ -> 1
Int, String, Float and Bool literals are all valid patterns. Bool is the only one a match can exhaust by listing (true and false), so it is the only one that needs no catch-all; an Int, String or Float match must end in a wildcard _ or an identifier arm, or the checker rejects it with Non-exhaustive match: missing catch-all (_) pattern. Repeating a literal is rejected too — the later arm can never fire, and the error names the line that already covers it.
Three things that look like literal patterns are parse errors:
- a negative number —
-1 -> …does not parse, because the-is a separate token and a pattern is not an expression. Branch on a comparison instead (match n < 0withtrue ->/false ->), or normalize the subject before the match. - an integer beyond 64 bits, even though
Intitself is arbitrary-precision. The error points at the replacement:match n == 1267650600228229401496703205376. - an interpolated string —
"{x}" -> …is rejected, because a pattern is a constant. Compare with==when the expected value is computed.
Float literal patterns compare exactly, so 0.1 + 0.2 does not match a 0.3 arm. Use them only for sentinels you produced yourself; otherwise branch on a comparison.
Creates a new record with overridden fields, preserving all other fields:
updated = User.update(u, age = 31)
m = {"key" => value, "other" => 42}
=> is required inside map literals; : stays type-only.
Effects are exact method names:
fn main() -> Unit
! [Console.print, Disk.readText]
Console.print("starting")
_ = Disk.readText("data.txt")
Both granular and namespace shorthand declarations are supported. ! [Disk.readText] declares a single effect, while ! [Disk] covers all Disk.* effects (namespace shorthand). aver check suggests narrowing when a shorthand could be more specific. effects X = [...] aliases are no longer supported.
Programs access CLI arguments via the Args service:
fn main() -> Unit
! [Args.get, Console.print]
args = Args.get()
Console.print(args)
Run with: aver run file.av -- arg1 arg2 arg3
Arguments after -- are available as List<String>. Without --, the list is empty. Args.get() requires ! [Args.get] — argument access is visible in the signature like any other effect.
aver run starts from main by default. To record or run any other top-level function, pass -e '<call>' (repeat for a batch) or --input-file PATH: aver run file.av -e 'load("PL")' --record recordings/. Arguments are limited to literals in 0.10.1; wrap complex inputs in a helper function.
fn add(a: Int, b: Int) -> Int
a + b
fn fetchUser(id: String) -> Result<HttpResponse, String>
? "Fetches a user record from an API."
! [Http.get]
Http.get("https://api.example.com/users/{id}")
? "..."— optional prose description (part of the signature)- deeper-indented string lines continue the same description:
? "Starts the CLI." "Dispatches one argv command." aver checkwarns when non-mainfunctions omit the description! [Effect]— optional effect declaration (statically and runtime enforced)- method-level effects are supported:
Http.get,Disk.readText,Console.print - top-level functions are first-class values and can be passed where
Fn(...)is expected mainoften returnsUnit, butResult<Unit, String>is also common;aver runtreatsResult.Err(...)returned frommainas a runtime failure- function bodies use indentation
- the last expression in a function body is the return value
Regular verify blocks live directly under the function they cover:
verify add
add(0, 0) => 0
add(2, 3) => 5
Law-style verify blocks express finite universal checks over explicit domains:
verify add law commutative
given a: Int = -2..2
given b: Int = [-1, 0, 1]
add(a, b) => add(b, a)
If the identifier after law is the name of an existing pure function and the law body compares foo(args) against fooSpec(args), Aver treats that as a spec law. verify fib law fibSpec is the preferred way to say "fib should match fibSpec".
This is an intentional style choice. In Aver, the author should usually write a simple spec function and a law relating the implementation to that spec, instead of writing proof-oriented invariants directly in surface code.
verify is deterministic, not random. Regular cases run exactly as written. verify ... law ... expands the cartesian product of explicit given domains, capped at 10_000 cases.
Oracle laws cover classified effectful functions:
fn fairDie(path: BranchPath, n: Int, min: Int, max: Int) -> Int
? "Deterministic Random.int stub."
4
fn pickOne() -> Int
? "Rolls once."
! [Random.int]
Random.int(1, 6)
verify pickOne law usesOracle
given rnd: Random.int = [fairDie]
pickOne() => rnd(BranchPath.Root, 0, 1, 6)
Inside verify <fn> law <name>, given binds an effect method such as Random.int or Http.get to one or more Aver stub functions for checked samples, while proof export can quantify over the oracle itself. Use cases-form verify <fn> trace when you want .result and .trace.* assertions over the collected trace of classified effect emissions.
Effects outside Oracle's classified set still belong in record/replay, especially ambient state, persistent protocol sessions, terminal modes, and server callbacks. See oracle.md for the supported effect set, stub signatures, and trace API.
aver check expects pure, non-trivial, non-main functions to carry a colocated verify block.
decision blocks are first-class top-level syntax for design rationale:
decision UseResultNotExceptions
date = "2024-01-15"
reason =
"Invisible exceptions lose control flow."
"Result keeps failure explicit at the call site."
chosen = "Result"
rejected = ["Exceptions", "Nullable"]
impacts = [charge, refund, settle]
author = "team"
chosen, rejected, and impacts may reference validated symbols or quoted semantic labels. Decisions are exported through aver context ... --decisions-only.
All user-defined functions are top-level. At call time, a function sees globals + its own parameters — no closure capture at definition time.
Top-level functions are still first-class values, so higher-order builtins such as HttpServer.listenWith(port, context, handle) work without introducing lambda syntax or hidden captures.
There is no lambda syntax. List processing is typically written with recursion and pattern matching rather than callback-based helpers.
This means Fn(...) -> ... is a real type, but a function value may appear only as a function parameter — i.e. a named function (or builtin / constructor) passed directly in call-argument position, exactly as HttpServer.listenWith(port, context, handle) does. A Fn(...) type used as a function's return type, a record or variant field, a collection or tuple element, or nested inside another Fn, and binding a function value to a local (g = double) — are all rejected at type-check time. Function values therefore never escape callback-argument position, so the concrete callee at every call — and with it the set of effects it can perform — stays statically knowable, which is what the effect system, the Oracle, and aver verify rely on. If you need to select between functions dynamically, branch at the call site or model the choice as a sum type and match on it.
fn applyTwice(f: Fn(Int) -> Int, x: Int) -> Int
f(f(x))
fn inc(n: Int) -> Int
n + 1
Most application code in Aver stays first-order and explicit. Use function parameters when they make an API cleaner, not as a default abstraction tool.
Aver has no dedicated Set type. The idiomatic way to express a set is Map<T, Unit> — a map whose values carry no information. All Map.* operations work on sets:
seen: Map<String, Unit> = {}
seen2 = Map.set(seen, "alice", Unit)
Map.has(seen2, "alice") // true
Map.len(seen2) // 1
seen3 = Map.remove(seen2, "alice")
Map.set(s, k, Unit) adds an element, Map.has(s, k) checks membership, Map.remove(s, k) removes an element, and Map.len(s) returns cardinality. Map literals with Unit values work as set literals: {"alice" => Unit, "bob" => Unit}.
When targeting formal verification backends, the codegen automatically lowers Map<T, Unit> to the native set type:
| Backend | Aver type | Target type | Map.set(s, k, Unit) |
|---|---|---|---|
| Dafny | Map<T, Unit> |
set<T> |
s + {k} |
| Lean | Map<T, Unit> |
Finset T |
AverSet.add s k |
fn sum(xs: List<Int>) -> Int
match xs
[] -> 0
[head, ..tail] -> head + sum(tail)
hasAlice = List.contains(["alice", "bob"], "alice")
ages = Map.fromList([("alice", 30), ("bob", 25)])
maybe_age = Map.get(ages, "alice")
// Vector: indexed dense data (grids, buffers, lookup tables)
grid = Vector.new(100, 0) // 100 zeros
updated = Vector.set(grid, 42, 1) // Option<Vector<Int>>
value = Vector.get(grid, 42) // Option<Int>
Self and mutual tail recursion is optimized automatically. A transform pass after parsing rewrites tail-position calls into a trampoline — no stack growth for recursive functions in tail position. Tail position = last expression in function body, or each arm body in a match at tail position.
This is intentionally narrower than “all recursion”. Non-tail recursion can still be expensive on large inputs, so aver check warns when a recursive function still has non-tail recursive callsites after TCO. In practice, long linear traversals are best written in accumulator style when scale matters.
Module imports resolve from a module root (--module-root, default: current working directory).
Each module file must start with module <Name> and contain exactly one module declaration.
module Payments
intent = "Processes transactions."
effects [Disk.readText]
depends [Data.Fibonacci]
exposes [charge]
effects [...] declares the module's effect boundary — the union of the effects its functions may perform, in the same granular/namespace-shorthand form as function-level ! [...]. It goes after intent. aver check warns when a module with functions omits it; a pure module declares effects [] explicitly.
exposes opaque makes a type visible in signatures but blocks direct construction, field access, and pattern matching from outside the module. The type can still be passed around, returned, and stored.
module Pricing
exposes [mkDiscount, percent]
exposes opaque [Discount]
record Discount
percent: Float
fn mkDiscount(p: Float) -> Result<Discount, String>
? "Only way to create a Discount from outside."
match p < 0.0
true -> Result.Err("Discount cannot be negative")
false -> Result.Ok(Discount(percent = p))
fn percent(d: Discount) -> Float
? "Public accessor."
d.percent
From outside the module:
Pricing.mkDiscount(50.0)— works (returnsResult<Discount, String>)Pricing.percent(d)— works (returnsFloat)Discount(percent = 50.0)— compile error (opaque: cannot construct)d.percent— compile error (opaque: cannot access fields)
With --module-root examples:
depends [Data.Fibonacci]→examples/data/fibonacci.av, call asData.Fibonacci.fn(...)depends [Modules.Models.User]→examples/modules/models/user.av, call asModules.Models.User.fn(...)
Type errors block run, check, and verify. No partial execution. The checker covers function bodies, top-level statements, effect propagation, and duplicate binding detection.
| Absent | Reason |
|---|---|
if/else |
match is exhaustive — no silent missing cases |
for/while |
Use recursion, pattern matching, and explicit list operations |
| Streams / channels / async iterators | Recursive ?! over lists gives streaming, backpressure, and fan-out parallelism with no new concepts |
| Async runtime | Aver doesn't try to make streaming a primitive. Its parallelism model is explicit independence (?!), not a full async runtime. If you need stream abstractions, you can build them — but the language itself stays small and reviewable |
null |
Option<T> with Some/None only |
| Exceptions | Result<T, E> only — errors are values |
| Global mutable state | No shared mutable state by design |
| Closures | All functions are top-level — no captured variables, explicit is better than implicit |
| Magic | No decorators, no implicit behaviour, no runtime reflection |
Bitwise operators (&, |, ^, ~, <<, >>) |
The operations exist, named, in the Bits namespace. Keeping them out of the syntax is the same choice as / and %: a bit-level reading of an integer is worth spelling out. Bits is a namespace, not a type — its arguments and results are ordinary Int values, read as an infinite two's-complement bit sequence for one call. Fixed width is requested explicitly via Bits.low, never implied by a register size. Writing one of these operators reports which function replaces it |