Skip to main content

Built-in Functions

A small set of functions is provided by the compiler rather than the standard library. They are spelled as ordinary function calls — Verum has no !-suffix macros like Rust — but their implementation is hard-wired.

This page is the authoritative registry, organised by category.

Grammar reference:

builtin_call = builtin_name , '(' , [ argument_list ] , ')' ;

builtin_io            = 'print' | 'eprint' ;
builtin_assertion     = 'assert' | 'assert_eq' | 'assert_ne' | 'debug_assert' ;
builtin_control_flow  = 'panic' | 'unreachable' | 'unimplemented' | 'todo' ;
builtin_async         = 'join' | 'try_join' | 'join_all' | 'select_any' | 'ready' | 'pin' ;

I/O​

print​

fn print(args: ...Display);

Writes its arguments to standard output, separated by spaces, followed by a newline. Accepts any number of values implementing Display.

print("hello");                     // hello
print("x =", x, "y =", y);          // x = 3 y = 4
print(f"value: {x}");               // value: 3   (format string)

print is a built-in — functions calling it do not need a using [...] clause. Standard output is one of a small set of built-in effects (print, eprint, println, assert, panic, unreachable, todo, unimplemented) that bypass the user-ctx mechanism. User-declared contexts (Logger, Database, Clock, ...) still require their explicit using [...] declaration.

eprint​

fn eprint(args: ...Display);

Identical to print, writing to standard error.

eprint(f"Error: could not open {path}");

Assertions​

Assertions are runtime checks that call panic on failure. Under @verify(static) or @verify(formal), the SMT engine also checks them at compile time — a failing assertion with a provable counter-example is a compile error.

assert​

fn assert(condition: Bool);
fn assert(condition: Bool, message: Text);

Panics unless condition is true.

assert(x > 0);
assert(list.len() > 0, "list must be non-empty");

assert_eq / assert_ne​

fn assert_eq<T: Eq + Debug>(left: T, right: T);
fn assert_ne<T: Eq + Debug>(left: T, right: T);

Panics with both values formatted when inequality is detected (or equality for assert_ne). Faster than writing assert(a == b) — the failure message includes the actual values.

assert_eq(result, expected);
assert_ne(connection_id, 0);

debug_assert​

fn debug_assert(condition: Bool);
fn debug_assert(condition: Bool, message: Text);

Same as assert, but elided in release builds (verum build --release). Use for expensive invariants in hot paths.

debug_assert(balance >= 0, "invariant broken after ledger update");

Control flow​

These functions return the never type (!). The compiler treats their callers as diverging — no further code in the scope is reachable.

panic​

fn panic(message: Text) -> !;
fn panic(args: ...Display) -> !;

Terminates the current task or process with an error message. In a thread, unwinds (if unwinding is enabled) and propagates to the nursery; in #[no_std], aborts.

panic(f"unexpected state {state}");
panic("not implemented for tagged variant");

unreachable​

fn unreachable() -> !;
fn unreachable(message: Text) -> !;

Panics with an "unreachable code reached" message. Use in match arms that exhaust the input but cannot be proven exhaustive to the compiler, or at points invariants guarantee never execute.

match tag {
    Kind.Read  => handle_read(),
    Kind.Write => handle_write(),
    _ => unreachable(),
}

unimplemented​

fn unimplemented() -> !;
fn unimplemented(reason: Text) -> !;

Panics with "not yet implemented". Semantically equivalent to todo(); use unimplemented when you plan to leave the body unimplemented (e.g. an interface stub the user must fill).

todo​

fn todo() -> !;
fn todo(note: Text) -> !;

Panics with "todo". Use during development to leave placeholders. The verum lint tool reports todo() calls as warnings.

fn render(shape: Shape) -> Pixels {
    match shape {
        Shape.Rect(r) => rect_pixels(r),
        Shape.Ellipse(_) => todo("ellipse rendering"),
    }
}

Async primitives​

All async built-ins require an async runtime context; see async-concurrency.

join​

async fn join<A, B>(a: Future<A>, b: Future<B>) -> (A, B);
async fn join<A, B, C>(a: Future<A>, b: Future<B>, c: Future<C>) -> (A, B, C);
// …up to 8-ary

Runs all futures concurrently. Returns their results as a tuple once all have completed. If any future panics, the others are cancelled and the panic is re-raised.

async fn load_page() -> Page using [Http, Database] {
    let (hdr, body, footer) = join(fetch_header(), fetch_body(), fetch_footer()).await;
    Page { header: hdr, body, footer }
}

try_join​

async fn try_join<A, B, E>(
    a: Future<Result<A, E>>,
    b: Future<Result<B, E>>,
) -> Result<(A, B), E>;
// …up to 8-ary

Like join, but short-circuits on the first Err. All tuple items must have the same error type.

let (rows, meta) = try_join(db.rows(), db.meta()).await?;

join_all​

async fn join_all<T>(futures: Vec<Future<T>>) -> Vec<T>;

Runs a variable number of identical-result-type futures. Returns all results as a Vec<T>. Any panic propagates.

select_any​

async fn select_any<T>(futures: Vec<Future<T>>) -> (T, usize, Vec<Future<T>>);

Completes when the first future completes. Returns the result, the index of the winning future, and the remaining (unpolled) futures.

let (winner, idx, rest) = select_any(vec![fast, medium, slow]).await;
print(f"task {idx} won with {winner}");
// `rest` is still live — drop or reawait.

ready​

fn ready<T>(value: T) -> Future<T>;

Wraps a synchronous value in a Future<T> that is immediately ready. Useful for stubs and control flow that expects a future.

let fut: Future<Int> = ready(42);
let x = fut.await;      // 42

pin​

fn pin<T>(value: T) -> Pin<T>;

Pins a value to its current memory location so that self-referential futures can be polled safely. Most users encounter pin only through the async expansion — manual use is rarely needed.

Time & system intrinsics​

From core.intrinsics.runtime.time — auto-mounted in every crate. These are direct wrappers over OS clocks; cost is one syscall or a single mach_absolute_time / QueryPerformanceCounter call on the respective platform.

monotonic_nanos​

fn monotonic_nanos() -> UInt64

Nanoseconds from an opaque, monotonically-increasing reference point (kernel boot on Linux; mach_absolute_time on macOS). The returned value has no Unix-epoch meaning — use it only for differences.

let t0 = monotonic_nanos();
do_work();
let elapsed_ns = monotonic_nanos() - t0;

Immune to wall-clock adjustments (NTP step, DST, user-set). The single correct choice for benchmarking, timeouts, and rate-limiting.

realtime_nanos​

fn realtime_nanos() -> UInt64

Nanoseconds since the Unix epoch (1970-01-01T00:00:00Z UTC). Use for timestamps and logs; not for measuring intervals — the clock can go backwards.

realtime_secs​

fn realtime_secs() -> Int64

Whole seconds since the Unix epoch. Same caveats as realtime_nanos.

num_cpus​

fn num_cpus() -> Int

Logical-CPU count as the kernel sees it. Use when sizing thread pools or work-queue fan-out. Matches what the async scheduler would auto- pick when async_worker_threads = 0.

sleep_ms / sleep_ns​

fn sleep_ms(ms: Int)
fn sleep_ns(ns: Int)

Block the current thread (or task, when called from an async fn) for at least the given duration. Precision is OS-dependent — on Linux sleep_ns resolves to nanosleep; on macOS to mach_wait_until.

Use from async code sparingly — prefer cancellable sleeps exposed by the async runtime (time.sleep(...).await).

Format strings (f"...")​

Not a function, but tightly coupled to print. f"..." is a literal whose {expr} splices are type-checked. See Tagged Literals for the grammar.

Format specifications use the colon separator:

f"{value:04}"                 // pad with zeros to width 4
f"{price:.2}"                 // 2 decimal places
f"{p:>10}"                    // right-align, width 10
f"{msg:^.20}"                 // centre, truncate to 20
f"{bytes:#x}"                 // hex with 0x prefix
f"{value:?}"                  // debug form

Format spec mini-language:

[fill][align][sign][#][0][width][.precision][type]
align = < | > | ^
sign  = + | -
type  = x | X | o | b | e | E | f | F | ?

What is not a built-in​

A few things look built-in but are standard library or grammar constructs:

  • select { … } — an expression, not a call. See async-concurrency.
  • nursery { … } — an expression with options and handlers.
  • format — no such function; use f"...".
  • matches! — Verum uses the is operator: value is Some(x).
  • vec! / list! / hashmap! — use literal syntax ([1, 2], {k: v, ...}) or constructors (List.of(...), Map.of(...)).

See also​