# Aver > Aver is a statically typed language optimized for a world where code is cheap to generate and expensive to trust. The optimization target is the reviewer, not the generator. - Website: https://averlang.dev - Playground: https://averlang.dev/playground/ - GitHub: https://github.com/jasisz/aver - crates.io: https://crates.io/crates/aver-lang - License: MIT - Written in: Rust - Backends: bytecode VM, Rust codegen, WASM, Lean 4 proof export, Dafny verification ## Before you write Aver If you only remember one section, make it this one: - Files end with `.av`, not `.aver` - Each file starts with exactly one `module ` declaration - Module metadata uses `intent =` and `exposes [...]` - Bindings are `name = expr` or `name: Type = expr` — no `let`, `val`, or `var` - Constructors are always qualified: `Result.Ok`, `Result.Err`, `Option.Some`, `Option.None` - There is no `if` / `else`; use `match` - Match arm bodies must start on the same line as `->`; for complex logic, extract a helper function - Effects are explicit: `! [Console.print]`, `! [Http.get]` - Pure functions get colocated `verify` blocks - Effectful flows should usually be tested through record/replay, not `verify` - Parse integers with `Int.fromString`, which returns `Result` - `Console.readLine()` returns `Result`, not plain `String` ## Minimal correct file ```aver module Hello intent = "Tiny intro module." exposes [greet, main] fn greet(name: String) -> String ? "Builds a greeting." "Hello, {name}!" verify greet greet("Aver") => "Hello, Aver!" fn main() -> Unit ? "Entry point." ! [Console.print] Console.print(greet("world")) ``` This shows the core pattern: - a pure function - a `verify` block directly below it - an effectful `main` ## Core syntax ### Types Primitives: - `Int` - `Float` - `String` - `Bool` - `Unit` Common compound types: - `Result` - `Option` - `List` - `Vector` - `Map` - tuples: `(A, B, ...)` - function types: `Fn(A) -> B`, `Fn(A) -> B ! [Effect]` `Unit` means "no meaningful value" and renders as `()` in diagnostics. ### Bindings All bindings are immutable. ```aver name = "Alice" age: Int = 30 xs: List = [] ``` ### Functions ```aver fn add(a: Int, b: Int) -> Int a + b fn fetchUser(id: String) -> Result ? "Fetches a user record from the API." ! [Http.get] Http.get("https://api.example.com/users/{id}") ``` Rules: - `? "..."` is the prose description — must be indented on the line directly after the function signature, no blank line between - `! [...]` declares effects — also indented, directly after `?` (or after signature if no `?`) - indentation defines the body — the first expression must follow immediately, no blank lines after signature/`?`/`!` - the last expression is the return value - there is no `return` keyword - `main` returns `Unit` or `Result` ### Match There is no `if` / `else`. All branching is `match`. ```aver match value 42 -> "exact" _ -> "anything" [] -> "empty list" [h, ..t] -> "head {h}" Result.Ok(v) -> "ok: {v}" Result.Err(e) -> "err: {e}" Shape.Circle(r) -> "circle" ``` Boolean branching: ```aver match x > 0 true -> "positive" false -> "non-positive" ``` Important: the expression for an arm must begin on the same line as `->`. Good: ```aver match x > 0 true -> "positive" false -> helper(x) ``` Avoid: ```aver match x > 0 true -> "positive" ``` ### Constructors and user-defined types UpperCamel callees are constructors. They are always qualified when namespaced. ```aver Result.Ok(42) Result.Err("bad") Option.Some("hello") Option.None ``` Sum types: ```aver type Shape Circle(Float) Rect(Float, Float) Point ``` Records: ```aver record User name: String age: Int ``` Record construction uses named fields: ```aver User(name = "A", age = 1) ``` ### Modules ```aver module Billing intent = "Billing application core." exposes [charge, refund] depends [Core.Types, Infra.Store] ``` Rules: - `module` must be the first top-level item - `intent` describes the module's purpose - `exposes` lists public functions and types - `depends` resolves from `--module-root` - opaque exports use `exposes opaque [TypeName]` ### Effects Effects can be granular or namespace-wide. ```aver fn save(data: String) -> Unit ? "Writes data to disk." ! [Disk.writeText] Disk.writeText("out.txt", data) ``` If a function calls `Console.print`, `Http.get`, or another effectful capability without declaring it, the compiler errors. Effects also propagate through calls, so callers must declare the effects required by their callees. - `! [Http.get]` allows only `Http.get` - `! [Http]` covers all `Http.*` effects Example with input parsing: ```aver fn askName() -> String ? "Reads a name or falls back to stranger." ! [Console.readLine] input = Console.readLine() match input Result.Ok(line) -> line Result.Err(_) -> "stranger" ``` ### Verify and replay Regular verify — each line is `expression => expected_value` (note: `=>`, not `=`): ```aver fn add(a: Int, b: Int) -> Int a + b verify add add(1, 2) => 3 add(0, 0) => 0 ``` **Important:** the separator is `=>` (fat arrow), never `=`. Writing `=` is a parse error. Law verify (generative testing over value ranges): ```aver verify add law commutative given a: Int = -2..2 given b: Int = [-1, 0, 1] add(a, b) => add(b, a) ``` Law verify rules: - `given` lines define value ranges - exactly one assertion line (`lhs => rhs`) - the assertion must be a single expression, not a boolean chain — if you need multiple conditions, extract a helper function Use `verify` for pure logic. Use replay for effectful flows. ```text aver run app.av --record recordings/ aver replay recordings/ --test --diff ``` ### Decisions Architectural rationale is first-class syntax: ```aver decision UseResultNotExceptions date = "2024-01-15" reason = "Exceptions hide in signatures." "Result forces explicit handling." chosen = "Result" rejected = ["Exceptions", "Nullable"] impacts = [safeDivide, safeRoot] ``` ### Operators - arithmetic: `+`, `-`, `*`, `/` (integer division truncates) - comparison: `==`, `!=`, `<`, `>`, `<=`, `>=` - error propagation: `expr?` - independence: `(a, b)!`, `(a, b)?!` **These operators do NOT exist** — do not use them: - no `%` (modulo) — compute as `a - (a / b) * b` - no `&&`, `||` (boolean and/or) — use `Bool.and(a, b)`, `Bool.or(a, b)`, or nested `match` - no `!` (boolean not) as prefix — use `Bool.not(x)` - no `+=`, `-=`, `++`, `--` (mutation operators) - no bitwise operators ### Recursion There are no loops. Use recursion and pattern matching. ```aver fn sum(xs: List) -> Int match xs [] -> 0 [h, ..t] -> h + sum(t) ``` Tail-call optimization is automatic. ## Common namespaces Useful pure functions: - `Int.fromString : String -> Result` - `Int.toString : Int -> String` - `Int.abs : Int -> Int` - `Float.fromString : String -> Result` - `String.len : String -> Int` - `String.contains : (String, String) -> Bool` - `String.toUpper : String -> String` - `String.toLower : String -> String` - `String.trim : String -> String` - `String.join : (List, String) -> String` - `String.concat : (String, String) -> String` - `List.len : List -> Int` - `List.prepend : (T, List) -> List` - `List.concat : (List, List) -> List` - `List.reverse : List -> List` - `List.contains : (List, T) -> Bool` - `Map.get : (Map, K) -> Option` - `Vector.get : (Vector, Int) -> Option` - `Result.withDefault : (Result, T) -> T` - `Option.withDefault : (Option, T) -> T` - `Bool.and : (Bool, Bool) -> Bool` - `Bool.or : (Bool, Bool) -> Bool` - `Bool.not : Bool -> Bool` Useful effectful namespaces: - `Console.print` - `Console.error` - `Console.warn` - `Console.readLine` - `Http.get` - `Disk.readText` - `Disk.writeText` - `Tcp.connect` - `Terminal.readKey` Notably absent: - no built-in `List.map` - no built-in `List.filter` - no built-in `List.fold` Write these with recursion. ## Toolchain ```text aver run file.av aver run file.av --self-host aver verify file.av aver check file.av aver why file.av aver format file.av aver context file.av --budget 10kb aver compile file.av -o out/ aver compile file.av --target wasm aver compile file.av --target wasm --wasm-opt oz aver proof file.av -o proof/ aver proof file.av --backend dafny aver replay recordings/ --test --diff ``` For AI navigation, start with: ```text aver context file.av --budget 10kb ``` Then zoom in with `--focus ` or a larger budget. ## Common mistakes 1. Writing `.aver` files instead of `.av` 2. Using `let`, `val`, or `var` instead of `name = expr` 3. Using bare constructors like `Ok(x)` instead of `Result.Ok(x)` 4. Using `String.toInt` instead of `Int.fromString` 5. Assuming `Console.readLine()` returns `String` instead of `Result` 6. Using `if` / `else` instead of `match` 7. Writing multi-line match arms instead of extracting a helper 8. Putting `verify` on effectful flows instead of using replay 9. Expecting closures or lambdas — not supported 10. Expecting mutable variables — not supported 11. Expecting `List.map`, `List.filter`, or `List.fold` to exist 12. Using `%` for modulo — not an operator; use `a - (a / b) * b` 13. Using `&&`, `||` for boolean logic — use `Bool.and`, `Bool.or`, or nested `match` 14. Writing `=` instead of `=>` in verify blocks — the separator is always `=>` 15. Using `..` without a name in list patterns — write `[h, ..t]`, not `[h, ..]` ## Further reading - Language Guide: https://github.com/jasisz/aver/blob/main/docs/language.md - Services (stdlib): https://github.com/jasisz/aver/blob/main/docs/services.md - Constructors: https://github.com/jasisz/aver/blob/main/docs/constructors.md - Common Pushback: https://github.com/jasisz/aver/blob/main/docs/pushback.md - Independence (?!): https://github.com/jasisz/aver/blob/main/docs/independence.md - Lean proofs: https://github.com/jasisz/aver/blob/main/docs/lean.md - Dafny verification: https://github.com/jasisz/aver/blob/main/docs/dafny.md