Keywords

Verum distinguishes reserved keywords — which cannot ever be used as identifiers — from contextual keywords, which are keywords only where the grammar expects them and ordinary identifiers elsewhere.

Reserved — only 3

These may never appear as identifiers:

Keyword	Use
let	Variable binding (let x = ...).
fn	Function definition (fn foo() { ... }).
is	Type-definition separator (type T is …); pattern test.

The parser recognises these three tokens unconditionally.

let let = 42;               // SYNTAX ERROR — `let` is reserved
let fn = foo;               // SYNTAX ERROR — `fn` is reserved
let is = true;              // SYNTAX ERROR — `is` is reserved

let fn_pointer = foo;       // fine — a name that BEGINS with a keyword
let is_valid = true;        // fine, for the same reason

A keyword is a whole token. fn_pointer and is_valid are ordinary identifiers, and the compiler accepts them.

Contextual — 109

Contextual keywords take the keyword role only when the grammar expects them. In any other position they are ordinary identifiers.

For example, async is a keyword only immediately before fn or at the start of a block expression:

async fn fetch() { ... }        // keyword
let async = 42;                 // identifier — legal
print(async);                   // identifier — legal

Below is the full contextual keyword list, grouped by purpose. The authority is the lexer: crates/verum_lexer/src/token.rs carries 112 #[token("…")] keywords, three of them reserved, so 109 are contextual. This page names every one.

Visibility

pub    public    internal    protected    private

Used at the start of items. private is explicit (matching the absence of any visibility).

Declarations

type    module    mount    link        implement   context   protocol
extends const     static   meta        ffi         extern    pattern
using   layer

Each introduces a top-level or contained item; see the corresponding item production in the grammar. link is the second spelling of mount — the grammar's mount_stmt accepts either. using [...] declares the contexts a function demands, and is the keyword the whole context system turns on; layer groups provide statements into a named bundle (layer AppLayer { provide Ctx = expr; }).

volatile is a pointer-type modifier rather than an item keyword — *volatile UInt32, for MMIO — and belongs with the type system below.

Control flow

if    else    match    return    for    while    loop    break    continue    in

in appears in for p in iter, provide X = v in { ... }, and quantifier bindings (forall x in S. P).

Async and structured concurrency

async    await    spawn       defer    errdefer    try
yield    throws   select      nursery  recover     finally
biased   on_cancel

• biased — marker on select for prioritised branch order.
• on_cancel — handler attached to a nursery block.

Function modifiers

pure    mut    const    unsafe    move    ref    default    cofix

• cofix — coinductive fixpoint; see language/copatterns.
• default is contextual: a method marked default inside implement is overridable by specialisations. Elsewhere — including as a variable name — it's an ordinary identifier.

Metaprogramming

meta    quote    lift    stage

• quote { ... } — quasi-quotation.
• lift(expr) — cross-stage lift.
• stage — appears only in $(stage N){ expr } and quote(N){ ... }.

Paths and self

self    super    crate    Self

• self — the current instance (lowercase), or the current module inside paths.
• Self — the implementing type (uppercase), inside protocols and impl blocks.
• super — the parent module.
• crate — the cog's root module.

Contracts and verification

where    requires    ensures    invariant    decreases    result

• requires — precondition.
• ensures — postcondition; result refers to the return value.
• invariant / decreases — loop contracts.

Proof DSL

theorem    lemma       axiom        corollary    proof
calc       have        show         suffices     obtain
by         qed         induction    cases        contradiction
forall     exists      tactic       from         implies
assumption

Tactic names are keywords too, not identifiers:

auto    blast    simp    smt    ring    field    omega    trivial

See language/proof-dsl and reference/tactics.

Type system

some                  (* existential: some T: Protocol                          *)
dyn                   (* dynamic dispatch: dyn Protocol                         *)
unknown               (* top type — the dual of `!`                             *)
universe              (* universe polymorphism: universe u                       *)
Type                  (* kind / type-of-types: Type, Type(0), Type(u)           *)
Prop                  (* universe of proof-irrelevant propositions              *)
Level                 (* universe level kind: u: Level                           *)
max                   (* level arithmetic: max(u, v)                             *)
imax                  (* impredicative max for Π into Prop                       *)
view                  (* pattern-level view operator                             *)
affine                (* affine type modifier: type affine Foo is …             *)
linear                (* linear type modifier: type linear Foo is …             *)
stream                (* stream literal / pattern prefix                         *)
tensor                (* tensor literal + type prefix: tensor<3, 4> Float32      *)
checked               (* &checked reference, capability-ref modifier             *)
with                  (* capability type: T with [Read, Write]                   *)
gen                   (* generator expression prefix                             *)
set                   (* set comprehension prefix                                *)
typeof                (* runtime type of an expression                           *)

See the following language pages for semantics:

• affine / linear — resource-kind types.
• Prop / Type(n) / universe / Level / max / imax — universe hierarchy.
• dependent functions — Π is the kernel's name for the type, not a keyword: Pi (x: A) . B is a parse error. A dependent function is written as an ordinary fn.
• tensor — shape-typed tensor types and literals.
• row polymorphism — extensible records with | r.

Values

true    false    null

• null — the Maybe.None of raw pointer types; use Maybe.None in safe code.

The bottom type

!       (* never type — used in type position: `fn diverge() -> !` *)

! is a token in both expression (negation / bitwise-not) and type position (never). The parser distinguishes by context.

Pseudo-keywords

default

Contextual keyword inside implement blocks:

implement Display for T {
    default fn fmt(&self) -> Text { ... }       // `default` is a keyword here
}

let default = 42;                               // `default` is an identifier here

self / Self

Lowercase self is a value parameter; Self is the implementing type.

implement Foo for Bar {
    fn method(&self) -> Self { ... }           // Self = Bar
}

in, as

Both contextual. in appears in patterns/quantifiers/provide; as appears in casts, aliases, and mount renames.

Both are keywords everywhere, not only where the grammar expects them:

let as = 5;                    // error<E071>: `as` is a reserved keyword
let in = 5;                    // error<E071>: `in` is a reserved keyword

for x in 0..10 { ... }         // `in` as keyword
let y = 3.0 as Int;            // `as` as cast operator

They are listed here because no production names them — see reserved by the lexer below.

Reserved by the lexer

Twenty further words are taken by the lexer and refused as identifiers, even though the productions above do not name them. The grammar carries them as lexer_only_reserved:

as · checked · cofix · coinductive · extern · false · in · inductive · inject · lift · move · private · quote · ref · throw · true · typeof · unknown · view · with

let move = 5;               // error<E071>: `move` is a reserved keyword
let view = 5;               // error<E071>: `view` is a reserved keyword
let other = 5;              // fine

So "three reserved keywords" is a statement about the grammar's reserved_keyword production, not about the names an author may bind. Twenty-three words are refused in a binding position.

Why so few reserved?

Only the three most essential tokens (let, fn, is) are fully reserved. Everything else can be an identifier in a context where the grammar does not expect it. This is a deliberate choice: keywords scale with the language's vocabulary, but the author's naming latitude should not.

You can name a variable async, impl, move, or pattern with no quoting and no escape syntax — the compiler disambiguates by position.

Operators that look like keywords

These tokens are not keywords — they are operators with spellings that resemble keywords:

Token	Kind
is	Reserved keyword; pattern test operator.
as	Contextual keyword; type cast operator.
.await	Postfix operator (dot + keyword).
in	Contextual keyword; not an operator.

Grammar reference

The authoritative keyword list is the keyword production in the grammar reference:

keyword = reserved_keyword | primary_keyword | control_flow
        | async_keywords | modifiers | ffi_keywords
        | module_keywords | additional_keywords | proof_keywords
        | lexer_only_reserved ;

Plus the token production for keyword-like literals (true, false, null) and the type production for type-system keywords (Self, Type, Level, unknown).

See also

• Syntax — how keywords appear in context.
• Operators — operator-like tokens.
• Grammar — the full grammar.