Skip to main content

Frequently Asked Questions

Language​

What is the current stability?​

The documented feature set is implemented and tested: refinement types, dependent types, cubical HoTT, SMT verification, VBC interpreter, LLVM AOT — all ship in a single verum binary. 1 506 of 1 507 conformance checks pass (99.93 %). Rough edges remain around newer features (cubical normalisation, MLIR GPU). Expect early-adopter friction.

How fast is it?​

LLVM-AOT builds hold a native-C parity bar (1×) — a workload running below parity is treated as a defect to close, not a range to accept. The CBGR reference model adds 1.2–1.7 ns (measured on the production_targets bench, well under the ≤ 15 ns design target) to non-promoted dereferences — invisible in most code; measurable in tight loops (where escape analysis typically eliminates it anyway).

Can I use it for embedded / bare-metal work?​

Yes. verum.toml supports runtime = "embedded" (stack allocator, no heap) and runtime = "no_runtime" (kernel / bootloader). Generated AOT programs require direct syscalls on Linux/FreeBSD, libSystem on macOS, kernel32/ntdll on Windows, and bare-metal facilities for embedded targets. Native implementation gaps remain; consult the AOT no-libc status before relying on an artifact for freestanding deployment. The host CLI and interpreter have a separate clean-OS compatibility requirement and may use libc.

Does it have garbage collection?​

No. CBGR is the memory model: unique ownership (Heap<T>), atomically ref-counted sharing (Shared<T>), and borrowed references (&T) that carry a generation counter checked on deref (1.2–1.7 ns). No GC pauses.

What about async?​

First-class: async fn, .await, work-stealing executor, async channels / mutexes / rwlocks, structured concurrency via nursery, select as a keyword expression. See async.

Does it work on Windows / macOS / Linux?​

All three, plus WASM, embedded, and no-runtime. iOS and Android are on the roadmap.

Verification​

Is this a theorem prover?​

It is capable of theorem-prover-level proofs (see proofs), but you don't have to use that. Most code uses refinement types + @verify(formal), which feels like "very strong type checking," not "theorem proving."

Do I have to prove everything?​

No. Verification is a spectrum. Default is @verify(static) — dataflow, CBGR, and refinement checking without SMT. You opt into @verify(formal) or stronger only where it matters.

Which SMT solver does it use?​

The language layer is backend-agnostic. The current release bundles solver adapters behind the capability router — different theories (LIA / bitvectors / arrays vs strings, nonlinear arithmetic, SyGuS, finite-model-finding) route to different adapters; @verify(thorough) cross-validates across them. A Verum-native solver is on the roadmap. See SMT routing.

What happens when the solver times out?​

Default 5 s per obligation. On timeout, the fallback retries with a different solver. Configurable in verum.toml [verify] via solver_timeout_ms and per-module [verify.modules."my.module"] overrides.

Can I check proofs of an external library without re-verifying?​

Yes — proof-carrying code. A VBC archive embeds ProofCertificates for its obligations; a consumer verifies the bundle offline without running the full compiler. See proof → PCC.

Types​

Do refinement types really have zero runtime cost?​

Yes. Every refinement is erased after typechecking. The value is just an Int (or whatever the base type is) at runtime.

Can I use them for domain modelling?​

That's the primary use:

type Port     is Int  { 1 <= self && self <= 65535 };
type Email    is Text { self.matches(rx#"^[^@\s]+@[^@\s]+\.[^@\s]+$") };
type NonEmpty is List { self.len() > 0 };

See refinement patterns.

What's the difference between List<T> and Vec<T>?​

There's no Vec. Semantic honesty: types describe meaning, not layout. List<T> is the ordered- collection meaning. Today's default implementation is a contiguous growable buffer; tomorrow's might be different — without source changes.

Can I still do unsafe low-level stuff?​

Yes: &unsafe T, *const T, *mut T, *volatile T, unsafe fn, extern "C" blocks. Used for FFI, memory-mapped I/O, allocator implementations, and primitives inside core.mem.

Tooling​

IDE support?​

Full LSP 3.17. VS Code extension (verum-lang.verum), Neovim config, Emacs lsp-mode config in Installation. Features: real-time diagnostics with counter-examples, completion, inlay type hints, CBGR reference-tier hints, refinement hints, quick fixes.

Debugger?​

verum dap implements the Debug Adapter Protocol. Works with any DAP-compatible front-end (VS Code, nvim-dap, IntelliJ).

Package registry?​

verum package publish, search, and install use the project's [registry].index URL. The registry service and complete publication-to-build workflow are under development. Source publication accepts versioned registry dependencies; local and Git dependencies must be replaced explicitly before publishing. The CLI manifest rejects IPFS dependency fields. See Cog packages for supported commands and limitations.

Can I write one binary that calls out to C?​

Yes. extern "C" block with a boundary contract (preconditions, memory effects, thread safety, ownership transfer, error protocol). See FFI.

Where's cargo add?​

verum deps add <dep>. Full toolchain commands: see CLI reference.

Learning​

Where do I start?​

  1. Installation (curl ... | sh).
  2. Hello, World (5 minutes).
  3. Language tour (10 minutes).
  4. Pick a cookbook recipe that looks like your task.
  5. Read philosophy when you want to understand why.

I know Rust / TypeScript / Go. Where's the quick-reference table?​

  1. Refinement types — used everywhere; start there.
  2. Context system — using [...] replaces globals.
  3. Structured concurrency — nursery, select.
  4. Three-tier references — CBGR is invisible at first; when performance matters, promote to &checked T.
  5. @verify(formal) — annotate one critical function; see what the solver tells you.
  6. Dependent types / cubical — reach for these when you have a concrete reason.

Design​

Why no null?​

Because nullable-by-default leads to billion-dollar mistakes. Maybe<T> makes absence an explicit case that the compiler forces you to handle.

Why three reference tiers?​

Because one tier either pays the check always (1.2–1.7 ns — small, but not free in a hot loop) or zero always (too unsafe for default). Escape analysis automatically promotes &T to &checked T when provably safe; you keep the ergonomics, the compiler does the work.

Why @ not ! for macros?​

Because ! in Rust is Verum's logical NOT, and there are no macro arguments to pass positionally; the @ prefix is consistent with other compile-time constructs (@derive, @cfg, @verify, and user-defined macros @sql_query).

Why name the package manager cog?​

Because "package" is overloaded, "crate" is taken, and a cog is a thing that meshes with others to drive larger machinery. The metaphor earned its keep.

Why Latin?​

Verum means "truth." The language is built around making program truths mechanically checkable. And it's the shortest distinctive name we could find.

See also​