Syntax

Verum's concrete syntax is defined by the grammar reference. This page is the reader-friendly tour, one layer below the grammar and one layer above the per-feature documentation.

Lexical structure

Keywords

Only three are reserved and cannot be used as identifiers:

let   fn   is

The remaining 109 keywords are contextual — they are keywords where the grammar expects them and ordinary identifiers elsewhere. For example, async is a keyword only before fn or at the start of a block expression; it is a valid variable name otherwise.

Contextual keyword categories (see Keywords for the full list):

Category	Members (partial)
Primary	type, where, using
Control	if, else, match, for, while, loop, break, continue, return, in
Async	async, await, spawn, defer, errdefer, yield, throws, select, nursery, biased, try, recover, finally, on_cancel
Modifiers	pub, mut, const, unsafe, pure, static, meta, cofix, extern, move, ref, default
Visibility	public, internal, protected, private
Module	module, mount, implement, context, protocol, extends, self, super, crate, as, provide, ffi
Contracts	ensures, requires, invariant, decreases, result, some
Proof	theorem, lemma, axiom, corollary, proof, calc, have, show, suffices, obtain, by, qed, induction, cases, contradiction, forall, exists, tactic
Types	affine, linear, stream, tensor, dyn, checked, view, Self, Type, Level, universe
Values	true, false, null

The complete enumeration is normative and lives in Keywords.

Identifiers

ident_start    = letter | '_' ;
ident_continue = letter | digit | '_' ;
identifier     = ident_start , { ident_continue } ;

Identifiers are sequences of Unicode letters, digits, and underscores, starting with a letter or underscore. Type names and constructors conventionally use UpperCamelCase; functions and variables use snake_case; constants use SCREAMING_SNAKE_CASE. These conventions are not enforced by the compiler.

Numeric literals

Integer and float literals may include underscores as digit separators and optional type suffixes.

42             // Int (default)
42i32          // i32
42u64          // u64
1_000_000      // underscore separator
0xFF           // hex
0o77           // octal
0b1010         // binary
0xDEAD_BEEF    // hex with separator
0xFFu8         // hex with suffix

3.14           // Float (default, f64)
3.14f32        // f32
2.7e-3         // scientific
1.5e10f64      // explicit f64

Integer suffixes:

i8  i16  i32  i64  i128  isize
u8  u16  u32  u64  u128  usize

Float suffixes:

f32  f64

String literals

Four forms:

"hello"                           // plain, escapes processed
"""raw
multiline
no \n escapes"""                  // raw multiline

b"bytes only, ASCII"              // byte string — produces &[Byte]
f"interpolated {expr}"            // format literal — splices checked

format(fmt, …args)

format("…", args…) is a compile-time desugar that rewrites into an interpolated string literal and shares the exact same lowering pipeline as f"…". Both forms produce a Text value.

format("released_{}", id)          // ≡  f"released_{id}"
format("a={}, b={}", 1, 2)         // ≡  f"a={1}, b={2}"
format("spec {:?}", v)             // ≡  f"spec {v}"  (spec is stripped)
format("escaped {{ and }}")        // ≡  f"escaped {{ and }}"

Supported placeholder forms in format:

Form	Meaning
{}	anonymous positional splice
{:spec}	anonymous with spec (spec discarded)
{{ / }}	escaped literal { / }

Positional ({0}) and named ({x}) placeholders are not supported by the format(...) desugar. Use f"{x}" directly for named splices.

Arity rule: the number of {…} placeholders must equal the number of supplied arguments after fmt. A mismatch leaves the call unchanged — type-checking will then report undefined function: format.

Format specifiers in f"…"

Unlike the format(...) desugar above — which discards specifiers — an f-string literal renders them. The following forms are applied to the interpolated value:

Specifier	Effect	Example → output
{:?}	Debug representation	f"{Some(5):?}" → Some(5)
{:x} / {:X}	Hex, lower / upper	f"{255:x}" → ff
{:b}	Binary	f"{5:b}" → 101
{:o}	Octal	f"{8:o}" → 10
{:N}	Minimum width N	f"[{42:6}]" → [ 42]
{:0N}	Zero-padded width	f"{42:06}" → 000042
{:<N} / {:>N}	Left / right align	f"[{42:<6}]" → [42 ]
{:.N}	Float precision (N fractional digits)	f"{3.14159:.2}" → 3.14
{:^N}	Centre align	f"[{42:^6}]" → [ 42 ]
{:+}	Explicit sign	f"{42:+}" → +42

Numbers right-align by default; </>/^ override. Precision and width compose (f"{3.14159:8.2}" → 3.14).

The rows above are covered by formatting probes; centre alignment and the + flag, which this page listed as "still being wired up", both work.

note

{:e} is accepted and ignored

f"{31415.9:e}" prints 31415.9, not 3.14159e4 — the specifier is parsed and dropped rather than refused, so a program asking for scientific notation gets plain notation with no diagnostic. The LowerExp / UpperExp protocols exist in core/text/format.vr and nothing routes to them.

This matters most where the plain rendering is unusable: Float.max prints as 309 decimal digits.

The only doubled-quote rule for raw multiline:

r1 = """content with " inside""";        // fine — single quote ok
r2 = """""value""""";                    // """ inside: doubled as """"

Triple-quoted content is raw (\n, \t, \x00 are literal characters) except for ${...} interpolation, which always interpolates.

Tagged literals

json#"{...}"           sql#"""SELECT..."""
rx#"[0-9]+"            url#"https://example.com"
d#"2026-04-17"         ip#"2001:db8::1"

Tagged literals are compile-time validated by the tag's grammar and produce typed values (JsonValue, SqlQuery, Regex, Url, DateTime, IpAddress…). See Tagged Literals for the full registry.

Character literals

'a'          // simple
'\n'         // escape
'\\'         // backslash
'\''         // apostrophe
'\x7F'       // hex
'\u{1F600}'  // Unicode scalar by hex code point

Escape sequences

Escape	Meaning
\n	newline
\r	carriage return
\t	tab
\0	null byte
\a	bell
\b	backspace
\f	form feed
\v	vertical tab
\\	backslash
\'	apostrophe
\"	double quote
\xNN	hex byte
\u{NN..NN}	Unicode code point

Escapes process in "..." and f"..." but not in """...""" or tagged raw literals.

Boolean literals

true   false

Context-adaptive literals

A small set of non-string literals have dedicated syntax:

#FF0000             // hex colour (RGB — 6 hex)
#FF0000FFu8         // RGBA — 8 hex
@tag                // at-literal (tag value)
$identifier         // dollar literal (shell/macro variable)

Comments

// line comment
/* block comment, no nesting — terminates on first */ */
/// doc comment — attaches to the following item
//! inner doc comment — attaches to the enclosing item

Operators

Full precedence table in Operators. The high-level families:

Family	Operators
Arithmetic	+ - * / % **
Comparison	== != < > <= >=
Logical	&& || !
Bitwise	& | ^ << >> ~
Assignment	= += -= *= /= %= &= |= ^= <<= >>=
Range	.. ..=
Pipe	|>
Compose	>> <<
Arrow	-> =>
Optional	?. ?? ?
Path/member	. ::

Special operators with keyword-like behaviour:

• is — pattern test (value is Some(x), x is Int).
• as — type ascription (x as Int, x as &T).
• .await — future awaiting (fut.await).

Top-level items

A file (module) is a sequence of items. An item is any of:

mount core.io;                             // import (stdlib module)
public type Color is Red | Green | Blue;   // type definition
public const MAX: Int = 1024;              // constant
public static mut LOG_LEVEL: Int = 0;      // mutable static
module net { /* nested module */ }         // submodule
fn main() { /* … */ }                      // function (no ctx needed for built-ins)
implement Display for Color { /* … */ }    // protocol implementation
context Database { /* … */ }               // context definition
type Serializable is protocol { /* … */ }; // protocol (as a type kind)
extern "C" { fn c_fn(x: Int) -> Int; }     // FFI
ffi OpenSSL extends Crypto { /* … */ }     // FFI boundary
pattern Even(n: Int) -> Bool = n % 2 == 0; // active pattern
meta fn sql_query(input: tt) { /* … */ }   // meta (macro) definition
theorem add_comm(a: Int, b: Int) -> Bool
    ensures a + b == b + a
    proof by auto;                         // theorem
@framework(lurie_htt, "HTT 6.2.2.7")
axiom sheafification_is_topos<C>(c: C) -> Bool
    ensures true;                          // framework axiom
@verify(formal) fn critical() { /* … */ }  // attributed item

Visibility

public and pub are equivalent. The module access checker distinguishes these forms when a declaration reaches it:

• pub — visible to any module.
• pub(cog) — visible within the same cog; pub(crate) is an accepted spelling.
• pub(super) — visible to the immediate parent module only.
• pub(in path) — visible within the named module and its subtree.
• (none) or private — private to the defining module.
• internal and protected — limited to the defining module by the current checker. internal is not an alias of pub(cog); protected does not grant access to implementing types or submodules.

Source imports can reject restricted declarations before these rules are applied, and some project loading paths do not preserve their restrictions. See modules → visibility for the import and qualified-access limitations.

Attributes on items

Items can be prefixed with one or more @-attributes:

@derive(Debug, Clone, Eq)
@repr(C)
pub type Point is { x: Float, y: Float };

@verify(formal)
fn transfer(from: &mut Account, to: &mut Account, amount: Money)
    requires from.balance >= amount
    ensures  to.balance - old(to.balance) == amount
{
    from.balance -= amount;
    to.balance   += amount;
}

See Attributes and reference/attribute-registry.

Expression-oriented

Almost everything is an expression. if, match, {}, loop, and control-flow keywords all produce values.

let status = if code < 300 {
    "ok"
} else if code < 500 {
    "client-error"
} else {
    "server-error"
};

let count = match classify(msg) {
    Priority.High   => 10,
    Priority.Normal => 1,
    Priority.Low    => 0,
};

A block { s1; s2; expr } returns expr. A trailing ; converts expr to a statement whose value is ().

fn two() -> Int { 1 + 1 }       // returns 2
fn unit() -> ()  { 1 + 1; }     // returns ()

Divergent expressions

Expressions that never return have type ! (never). The compiler treats any expression following them as unreachable.

fn choose(x: Int) -> Int {
    if x < 0 { panic("negative") }     // panic : !
    else     { x }
}

panic, unreachable, unimplemented, todo, return, break, continue, and throw are divergent.

Statements

let x = 42;                        // binding
let (a, b) = pair;                 // destructuring binding
let mut counter = 0;               // mutable binding
let Some(user) = find(id) else {   // `let else` — diverge on pattern fail
    return not_found();
};
counter += 1;                      // assignment
(a, b) = (b, a);                   // destructuring assignment
defer cleanup();                   // always runs at scope exit
errdefer log_error();              // runs only on error exit
provide Clock = SystemClock.new(); // context provision
foo();                             // expression statement

Statements end with ; except for block-like expressions in statement position (if, match, loop, {}) which auto-terminate.

Pattern positions

Patterns appear in:

• match arms
• let bindings
• function parameters
• if let / while let guards
• for loop bindings
• let else (refutable)
• destructuring assignment targets

for User { id, name, email: _ } in users { ... }
if let Maybe.Some(x) = opt && x > 0 { ... }
while let Maybe.Some(line) = reader.next() { ... }

See Patterns for the full grammar.

Line endings and semicolons

Semicolons separate statements. The last expression in a block is its value and is not followed by ;. Adding a ; turns it into a statement evaluating to ().

fn two() -> Int { 1 + 1 }          // returns 2
fn unit() -> ()  { 1 + 1; }        // returns ()

Line endings are not significant — a Verum program is insensitive to whether statements span one line or many.

Paths

A path is a dotted sequence of identifiers that names an item:

core.io.print
core.collections.Map
core.math.frameworks.lurie_htt.sheafification_is_infinity_topos
self.field
super.function
crate.types.User

Roots:

• core — the stdlib root (the package that ships with every Verum install: core.io, core.collections, core.math, core.async, core.net, core.security, ...).
• crate — the root of the current cog.
• self — the current module.
• super — the parent module.

Generics and type arguments

Type parameters are written in angle brackets after the item name:

fn identity<T>(x: T) -> T { x }

type Pair<A, B> is (A, B);

implement<T: Ord> SortedList for List<T> { ... }

Invocation with explicit types uses the same angle brackets — both in type position and as call-site type arguments:

let xs: List<Int> = List.new();
let xs = List.new<Int>();
let n  = identity<Text>("hi");

Verum has no Rust-style turbofish: the ::<T> syntax is not a token in grammar/verum.ebnf. The grammar disambiguates foo<T>(args) from foo < T by lookahead alone.

using context clauses

The using [...] clause appears after the return type of a function or a function type:

fn fetch(url: &Url) -> Response using [Http];

fn send_to_all(msg: &Text) -> ()
    using [Database, Logger, Metrics]
{
    ...
}

A single context can drop the brackets:

fn read(path: &Path) -> Text using FileSystem;

The full syntax supports negative, conditional, transformed, and aliased context specifications:

fn pure() using [!IO, !Random, !State<_>]            // negative — must not use
fn maybe_track() using [Analytics if cfg.prod]       // conditional
fn tx() using [Database.transactional()]             // transformed
fn dual() using [Database as primary,                // aliased
                 Database as replica]

note

transactional() is the SYNTAX, not a shipped transformer

The transformed form is real grammar — transformed_context = context_path, context_transform, {…} with context_transform = '.', identifier, ['(', [transform_args], ')'] in grammar/verum.ebnf — and it parses; a conformance spec writes using TransactionalContexts = [Database.transactional(), Cache.scoped()].

But transactional is not a transformer core/ provides. Neither is scoped. The transform position accepts any identifier, and the standard library ships none to put there, so the line above shows the shape rather than a call you can make today. (It reads as a working example on this page and in core/context/provider.vr's own doc comment, which is where it came from.)

See Context System for details.

Where clauses

fn sort<T>(xs: &mut List<T>) where T: Ord { ... }

fn process<T, U>(xs: &List<T>) -> List<U>
    where T: Clone + Debug,
          U: From<T>,
          type U.Item: Display
{ ... }

@verify(formal)
fn transfer(from: &mut Account, to: &mut Account, amount: Money)
    requires amount > 0
    requires from.balance >= amount
    ensures  to.balance == old(to.balance) + amount
    ensures  from.balance == old(from.balance) - amount
{ ... }

Three where flavours for bounds / dependent typing — plus sibling contract clauses that use their own keywords:

• where T: Bound — generic constraints.
• where meta ... — compile-time invariants over generic parameters.
• requires ... / ensures ... — contract specifications. These are bare clauses on their own signature lines; each precondition takes its own requires, each postcondition takes its own ensures (no comma-joining on a single line). where requires / where ensures forms that combine the keyword with where do not parse — see verification → contracts for the full grammar and the two-gotchas summary.

Annotations and refinements

Types and functions can carry refinements (predicates that must hold):

type Probability is Float { 0.0 <= self && self <= 1.0 };

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

See Refinement Types.

Assignments

Destructuring assignment reuses the pattern grammar. See Destructuring for the full matrix of forms.

(a, b) = (b, a);
[first, ..rest] = items;
Point { x, y, .. } = origin();
(x, y) += (dx, dy);

What this page omits

Many features have their own dedicated pages. This page only covers the structural surface — the shape of the grammar and the rules for terminals. Semantics and details:

• Types: Types
• Functions: Functions
• Patterns: Patterns
• Memory: References
• Async: Async & Concurrency
• Contexts: Context System
• Proofs: Proof DSL

See also

• Grammar (EBNF) — normative grammar.
• Keywords — full keyword list.
• Operators — precedence table.
• Tagged Literals — tag registry.