Functions

Anatomy

pub async fn fetch_user<T: Parse>(id: UserId) -> Result<T, Error>
    using   [Http, Logger, Cache]
    throws  (NetworkError | ParseError)
    where   ensures result is Ok(u) => u.id == id
{
    Logger.info(f"fetching user {id}");
    let bytes = Http.get(f"/users/{id}").await?;
    T.parse(&bytes)
}

From outside in:

• pub — visibility.
• async — returns a Future<Result<T, Error>>.
• fn — function.
• <T: Parse> — type parameters with bounds.
• (id: UserId) — parameters with refined types.
• -> Result<T, Error> — return type.
• using [...] — context clause (effects / capabilities).
• throws (...) — typed error boundary.
• where ensures ... — postcondition (refinement on the return value).
• { ... } — body.

Function modifiers

Order matters. The full list, from the grammar (function_modifiers in verum.ebnf):

Modifier	Meaning	Implies
pub / internal / pub(super) / pub(in path)	visibility	—
pure	compiler-verified no side effects	using [!IO, !State<_>, !Random]
meta / meta(N)	compile-time executable at stage N	pure; may using meta contexts only
async	returns Future<Output = T>	caller must .await or spawn
cofix	coinductive fixpoint (corecursive)	must satisfy a productivity check
unsafe	may perform unchecked operations	callers require unsafe { ... } block

The compiler checks legal combinations:

Combination	Valid?	Note
pure async	✓	pure w.r.t. effects; .await is a suspension, not a side effect
pure unsafe	✗	unsafe admits arbitrary effects
meta async	✗	meta fn runs at compile time — no executor
async unsafe	✓	rare: raw async IO kernels
meta(2) pure	✓	multi-stage compile-time, still pure

What pure rejects today

Two parts of this are settled by design, and a third is a measured gap worth knowing before you lean on the modifier.

By design, pure permits Fallible and Divergent. A function that returns an error or panics is still pure: both outcomes are deterministic functions of the input. So neither ? nor panic trips the check, and that is intentional rather than an oversight.

The violation is E503. Measured on the current binary:

body of a pure fn	result
spawn { 1 }	error<E503>
(spawn { 1 })	error<E503>
let _ = (spawn { 1 }, 0).1	error<E503>
let _ = f"{spawn { 1 }}"	error<E503>
if a < 0 { panic("neg") } else { a }	accepted — Divergent is allowed

The wrapper rows are listed because until recently they were not reported: property inference treated 45 of the language's 73 expression forms as pure without inspecting their contents, so one pair of parentheses was enough to hide an impure operation from the check. Those four rows are now a conformance pin in both directions — the same wrappers around genuinely pure expressions must stay silent.

The three rows this page used to list as a gap now fire. Re-measured 2026-09-03 on verum check, each probe differing from its control in one value:

body of a pure fn	result
a + b (control)	accepted
print("x")	error<E503>: pure function \f` has side effects: IO`
*x = 1 through a &mut parameter	error<E503>: ... side effects: Mutates
a call to a non-pure function	error<E503>: ... side effects: IO
a pure method calling an impure method on the same type	error<E503>: ... side effects: IO

Writing a local is still not an effect — a loop accumulating into let mut acc is as pure as the fold it is written out from. The distinction the compiler draws is whether the assignment reaches its target through a reference the caller handed in.

Properties travel across call sites by a fixpoint over the module's functions, so declaration order does not decide the answer: an impure callee defined below its pure caller is still caught. Method properties are keyed per name, and a probe with A.reset impure and B.reset pure confirms that calling B.reset from a pure fn stays accepted — the two do not collide.

The negative-context form is not a substitute for pure, and the measurements say so rather than the reasoning. Re-measured 2026-09-03, each with a control that must stay silent:

probe	result
fn ok() using [C] { needs_c() } (control)	accepted
fn f() using [!C] { print("x") }	accepted — the exclusion is not checked against the body
fn g() using [!C] { needs_c() }	accepted — declaring !C does not refuse a call that requires C
fn h() { needs_c() }	error<E613>: context \C` used but not declared in function signature`

The last row used to be listed here as unreported; it is reported now, and it is the row that matters most — a context requirement does propagate to a caller that declares nothing. What a negative context still does not do is contradict the body: !C neither refuses a call requiring C nor rejects an effect of that shape.

One caveat about the spelling. IO is not a declared context anywhere in core/ — the declared set is Logger, Database, Clock, FileSystem, Random, Config, Cache, Metrics, Tracer, Auth and their kin. A positive using [IO] is refused with error<E605>: undefined context: IO. A negative using [!IO] used to be accepted — negative contexts were not validated against the declared set — but that gap was closed (T1095), and both directions now refuse an undeclared name: measured 2026-09-04, using [!IO] gives the same error<E605>: undefined context: IO.

So pure's documented expansion to using [!IO, !State<_>, !Random] names one context that exists and two spellings that do not — and writing that expansion by hand is now refused in both polarities. pure itself is unaffected, because it is checked by property inference (the table above) rather than by the context system: pure fn double(n: Int) -> Int { n * 2 } checks clean.

These are compile-time claims measured with verum check; a later phase may add its own diagnostics.

Parameters

Parameter patterns, not just names:

fn area({width, height}: &Rect) -> Float {
    width * height
}

fn process((head, tail): &(Item, List<Item>)) { ... }

The receiver parameter uses the dedicated forms:

fn method(&self) { ... }          // immutable borrow
fn mutate(&mut self) { ... }      // mutable borrow
fn consume(self) { ... }          // by value
fn checked(&checked self) { ... } // proven-safe borrow

Return

The last expression in the body is the return value. return expr; is a control-flow operator for early return.

Functions with no explicit return type return ().

Generator functions

fn* fibonacci() -> Iterator<Int> {
    let (mut a, mut b) = (0, 1);
    loop {
        yield a;
        (a, b) = (b, a + b);
    }
}

async fn* stream_events() -> AsyncIterator<Event> using [Ws] {
    while let Maybe.Some(e) = Ws.next().await {
        yield e;
    }
}

• fn* — sync generator, returns Iterator<T>.
• async fn* — async generator, returns AsyncIterator<T>.

Loop invariants and decreases

Loops inside verified functions take two clauses:

while lo < hi
    invariant 0 <= lo && hi <= xs.len()
    decreases hi - lo
{
    ...
}

• invariant — must hold at entry and after each iteration.
• decreases — a well-founded measure that strictly decreases every iteration. Proves termination.

Contracts

requires — preconditions

fn divide(a: Int, b: Int) -> Int
    requires b != 0
{
    a / b
}

Multiple preconditions comma-join on a single requires line.

ensures — postconditions

fn abs(x: Int) -> Int
    ensures result >= 0
    ensures result == x || result == -x
{
    if x >= 0 { x } else { -x }
}

Each ensures keyword takes one boolean expression; multiple clauses are conjoined by repeating the keyword. result refers to the return value. See verification → contracts for the two-gotchas summary (no where requires; one ensures per clause).

old(expr) in postconditions

old(expr) captures the value of expr at function entry — useful for "delta" contracts:

fn push<T>(xs: &mut List<T>, x: T)
    ensures xs.len() == old(xs.len()) + 1
{
    xs.data.push(x);
}

invariant + decreases — loop contracts

fn binary_search(xs: &List<Int>, key: Int) -> Maybe<Int>
    ensures result is Some(i) => xs[i] == key
{
    let (mut lo, mut hi) = (0, xs.len());
    while lo < hi
        invariant 0 <= lo && hi <= xs.len()          // true every iteration
        decreases hi - lo                             // strictly decreasing → termination
    {
        let mid = lo + (hi - lo) / 2;
        match xs[mid].cmp(&key) {
            Ordering.Less    => lo = mid + 1,
            Ordering.Greater => hi = mid,
            Ordering.Equal   => return Some(mid),
        }
    }
    None
}

The invariant must imply the postcondition when conjoined with the negation of the loop condition. The decreases expression must be a non-negative, well-founded value that strictly decreases each iteration — it proves the loop terminates.

How contracts are discharged

1. requires / ensures clauses generate SMT obligations in Phase 3a (contracts) and Phase 4 (semantic analysis).
2. invariant + decreases generate loop-local obligations in Phase 4.
3. Each obligation is dispatched to a single solver adapter or the portfolio per the function's @verify(...) strategy.
4. Results are cached keyed on SMT-LIB fingerprint and reused across incremental builds.

See verification → contracts for the full semantics and cookbook → adding verification for a guided walk-through.

Error handling

fn parse_port(s: Text) -> Result<Int, Error>
    throws(ParseError)
{
    let n = s.parse<Int>()?;
    if n < 0 || n > 65535 {
        throw ParseError.OutOfRange(n);
    }
    Ok(n)
}

• ? propagates a Result.Err or Maybe.None.
• throw E constructs and propagates an error, valid only when throws(...) is declared.

Closures

let square     = |x| x * x;
let typed      = |x: Int| -> Int { x * x };
let async_task = async |url| Http.get(url).await;

Closures capture their environment by the minimum capability needed (immutable reference, mutable reference, or by-move). Force a move with move:

let name = "Alice".to_string();
let greet = move |greeting| f"{greeting}, {name}!";
// `name` moved into the closure; no longer accessible here.

Closure types implement Fn / FnMut / FnOnce protocols:

Protocol	Captures	Can call	Meaning
Fn	&self	multiple times	read-only closure
FnMut	&mut self	multiple times	may mutate captures
FnOnce	self	once	consumes captures

In function signatures use fn(T) -> U for thin function pointers (no captures). For closures with captures, Verum has no impl Trait-in-argument-position sugar: write the bound explicitly as a type parameter, <F: Fn(T) -> U>, when the caller chooses the closure; use dyn Fn(T) -> U when you need runtime polymorphism (a heterogeneous collection of closures, for instance).

Forward declarations

In extern blocks and protocol bodies, fn ends with ; instead of a body:

extern "C" {
    fn malloc(size: Int) -> &unsafe Byte;
    fn free(ptr: &unsafe Byte);
}

type Describable is protocol {
    fn describe(&self) -> Text;
}