Skip to main content

Language Tour

Twelve minutes. Twelve features. No fluff. A fast syntax survey — every snippet is real Verum, not pseudocode, but several are deliberately abbreviated to keep the feature in focus (an async example that elides its own helper types, for instance). Treat this page as a map, not a copy-paste source; follow the linked chapter under each section for the complete, worked version.

1. Types and functions​

type Vec2 is { x: Float, y: Float };

fn dot(a: Vec2, b: Vec2) -> Float {
    a.x * b.x + a.y * b.y
}
  • type T is { ... } declares a record.
  • Function bodies are expressions; the last expression is returned.
  • No trailing semicolon on the return expression.

2. Sum types​

type Tree<T> is
    | Leaf
    | Node { value: T, left: Heap<Tree<T>>, right: Heap<Tree<T>> };

fn depth<T>(t: &Tree<T>) -> Int {
    match t {
        Tree.Leaf => 0,
        Tree.Node { left, right, .. } => 1 + max(depth(left), depth(right)),
    }
}
  • type T is A | B | ... declares a sum.
  • Heap<T> is an owned heap allocation. Tree<T> is self-referential and therefore indirect.
  • match on a sum type with wildcard field binding ...

3. Generics and protocols​

type Eq is protocol {
    fn eq(&self, other: &Self) -> Bool;
    fn ne(&self, other: &Self) -> Bool { !self.eq(other) }
};

implement<T: Eq> Eq for List<T> {
    fn eq(&self, other: &List<T>) -> Bool {
        self.len() == other.len() &&
        self.iter().zip(other.iter()).all(|(a, b)| a.eq(b))
    }
}
  • type P is protocol { ... } is an interface.
  • implement<T: Bound> P for X { ... } provides the implementation.
  • &Self is the receiver type; no self: noise.

4. Refinement types​

type Percentage is Float { 0.0 <= self && self <= 100.0 };
type UserId     is (Int) { self > 0 };

fn average(x: Percentage, y: Percentage) -> Percentage {
    (x + y) / 2.0     // SMT discharges the refinement on the result
}

Refinement predicates are part of the type. They are checked at the boundaries where values flow from unconstrained to refined, and erased at runtime when the proof succeeds. The SMT capability router (verum_smt.BackendSwitcher) picks the backend — a single adapter or a portfolio — based on the theory mix of the predicate.

5. Three-tier references​

fn managed(x: &T)         { /* 1.2–1.7 ns CBGR check (measured) */ }
fn proven (x: &checked T) { /* 0 ns — compiler verified */ }
fn escape (x: &unsafe T)  { /* 0 ns — you swear it's OK */ }

Start with &T. Profile. When escape analysis proves a reference cannot dangle, promote it to &checked T. Use &unsafe T only when you have an obligation the compiler cannot verify and you are willing to discharge it by inspection. The CBGR check lives in verum_cbgr and measures 1.2–1.7 ns today against a 15 ns design target.

6. Explicit contexts​

public context Database { fn load(auth: Int) -> Int; }
public context Logger { fn info(msg: &Text); }
public context Clock { fn now() -> Int; }
public context RateLimiter { fn check(ip: &Text); }

public type Request is { path: Text, client_ip: Text, auth: Int };
public type Response is { body: Text };

fn build_response(user: Int, req: Request) -> Response {
    Response { body: f"{user}: {req.path}" }
}

fn handle(req: Request) -> Response;
    using [Database, Logger, Clock, RateLimiter]
{
    let now = Clock.now();
    Logger.info(&f"request at {now}: {req.path}");
    RateLimiter.check(&req.client_ip);
    let user = Database.load(req.auth);
    build_response(user, req)
}

No globals. No @Autowired. Contexts are declared in the signature, propagated through the call graph, and erased when statically resolved.

7. Async + structured concurrency​

async fn fetch_all(ids: &List<Id>) -> List<Data>
    using [Http, Logger]
{
    nursery {
        let handles = ids.iter()
            .map(|id| spawn fetch_one(*id))
            .collect();
        handles.iter().map(|h| h.await).collect()
    }
}
  • async fn and .await.
  • nursery { ... } is a structured-concurrency scope: all spawned tasks are joined or cancelled before nursery returns.
  • Contexts automatically flow across spawn.

8. Verification​

@verify(formal)
fn binary_search(xs: &List<Int>, key: Int) -> Maybe<Int>
    where 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()
        decreases hi - lo
    {
        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
}
  • where ensures ... is a postcondition.
  • invariant and decreases make the loop discharge automatically.
  • @verify(formal) requests SMT-level verification.

9. Dependent types and cubical HoTT​

/// Dependent pair: a length-indexed list.
type Vec is n: Int, data: [Int; n];

/// Dependent function: return type depends on the argument's value.
fn replicate(n: Int { self >= 0 }, x: Int) -> [Int; n] {
    [x; n]
}

/// Path type from cubical HoTT — propositional equality is a type.
mount core.math.hott.{ HottPath, refl, I };

fn same_value<T>(x: T) -> HottPath<T>(x, x) {
    refl(x)
}

Σ-types (n: Int, data: [Int; n]), Π-types ([Int; n] where n is a value), and Path types (HottPath<T>(x, y) — the type of paths from x to y) coexist with refinement types and the rest of the surface language. The kernel's HoTT layer (Transp, HComp, Glue) is wired to its reduction rules in verum_smt.cubical_tactic.

The Path-type half does not compile yet

The HottPath / refl / I block above is the intended surface, not a working example. Copied verbatim into a file and run, it stops at the type checker:

error<E400>: Type mismatch: expected '@builtin_path', found 'Unit'
  --> main.vr:8:5
 7 │ fn same_value<T>(x: T) -> HottPath<T>(x, x) {
 8 │     refl(x)
   │     ^^^^^^^

It is the shipped stdlib, not the language feature. The same shape written out in your own file compiles and runs:

public type MyPath<A>(a: A, b: A) is @builtin_path;
public fn myrefl<A>(x: A) -> MyPath<A>(x, x) { @builtin_refl(x) }

Take that as a way to see the opcodes work, not as a working path type: let x: Int = myrefl(7); is accepted too, and runs — printing nil, not 7. (A normal type refuses the same line: let x: Int = wrap(7); over a Wrapped record is expected 'Int', found 'Wrapped'.) Inference has no arm for these names, so the declared return type is never checked against the body — which is the same missing piece the mounted version fails on, only failing quietly instead of loudly.

(That compiles with warning<E0410>: unknown meta-function on each @builtin_* — the parser's roster of known meta-functions has not been told about them — and runs anyway.)

What fails is the archived core.math.hott.refl, whose recorded return type comes back as Unit: ask for it directly with let x: Int = refl(7); and the answer is expected 'Int', found 'Unit'. The rest of the machinery is present — code generation binds the @builtin_* calls to CubicalExtended VBC sub-ops, the interpreter implements twelve of them, and verum_smt.cubical_tactic reasons about the types.

Σ-types, Π-types, Vec and replicate in the same block are unaffected and run.

This limitation concerns the archived signature of core.math.hott.refl; the source declaration alone does not establish that the imported return type is preserved.

10. Framework axioms​

mount core.math.frameworks.lurie_htt.{ Site, sheafification_is_infinity_topos };
//                                            ^ NOT DECLARED anywhere in
//                                              core/. `Site` is real; the
//                                              axiom name is not.

/// A theorem that invokes Lurie HTT 6.2.2.7 as a trusted postulate.
/// The dependency surfaces automatically in `verum audit --framework-axioms`.
theorem sheaf_topos_on_bures<C: Site>(c: C) -> Bool
    requires c.is_presentable()
{
    proof by {
        apply sheafification_is_infinity_topos;
    }
}

@framework(identifier, "citation") marks axioms whose justification comes from external mathematics (Lurie HTT, Schreiber DCCT, Connes reconstruction, Petz classification, Arnold–Mather catastrophe, Baez–Dolan coherence). Six stdlib packages ship 36 citation-tagged axioms. Run verum audit --framework-axioms to enumerate the trusted boundary of any proof corpus — no hidden postulates.

11. Metaprogramming​

@derive(Eq, Ord, Hash, Debug, Clone)
type Version is { major: Int, minor: Int, patch: Int };

meta fn repeat(n: Int, body: TokenStream) -> TokenStream {
    quote { for _ in 0..${n} { ${body} } }
}

fn warmup() {
    @repeat(3, { print("warming"); })
}
  • @derive(...) generates instances with a visible, deterministic expansion.
  • meta fn runs at compile time; quote { ... } builds ASTs hygienically.

12. The trusted kernel​

All of the above — tactics, SMT discharge, cubical reductions, framework axioms, derive-generated code — eventually produces a proof term. That proof term is re-checked by verum_kernel, the LCF-style kernel that is the sole trusted checker in Verum's stack. It is held to a single-reviewer / single-session audit budget and ships an extensive lib-test suite pinning every typing rule.

$ verum audit --framework-axioms    # enumerate the trusted boundary
$ cargo test -p verum_kernel        # re-run the TCB test suite

A bug anywhere outside the kernel manifests as "refused a valid program" or "certificate replay failed", never as "false theorem accepted". See Architecture → trusted kernel.

Where to next​

Every feature above has a dedicated chapter: