Write your first program
Install the toolchain, run a small program and learn the project layout.
Your first hour →Choose your starting point
A short route into the platform, whatever you are building.
Learn the language
Explore types, protocols, pattern matching, references and explicit contexts.
Language reference →Understand the platform
Follow source through bytecode and execution, then explore verification.
Platform architecture →Start with a small, complete program
Define the states your application can be in and match on their data. Save this as events.vr; it prints user 7 joined.
# After installing Verum:
verum run --tier interpret events.vr
# Exercise the native compiler explicitly:
verum run --tier aot events.vr
type Event is
| Joined(Int)
| Left(Int);
fn describe(event: Event) -> Text {
match event {
Joined(id) => f"user {id} joined",
Left(id) => f"user {id} left",
}
}
fn main() {
print(describe(Joined(7)));
}
One platform, connected layers
Language design, execution, libraries and verification share an ambition: make the system’s intent visible and its behaviour testable.
Model meaning in types
Records and sum types describe data; protocols and generics describe reusable behaviour. List, Map, Text, Result and Maybe form a shared vocabulary across application code and the standard library.
Types and data modelling →Make dependencies explicit
The using clause names the contexts a function needs. Dependencies such as logging or a clock become visible in the interface, with the same syntax extending into metaprogramming.
The context system →Choose how invariants are checked
Refinements and contracts express properties alongside the program. Verification settings select runtime checks, static proof obligations or certificate checking; each has its own supported scope and cost.
Contracts and verification →Inspect execution and memory
The interpreter and LLVM AOT compiler consume Verum bytecode. Reference checking, native resource cleanup and async execution have distinct contracts: use the execution and reference guides to choose a mode for your workload.
Execution contracts →Compose library building blocks
Explore collections, I/O, concurrency and application libraries through one module system. Module documentation describes APIs and limitations; the presence of a module alone is not a deployment guarantee.
Standard library →Connect architecture to code
Architectural annotations describe capabilities, dependencies and boundary invariants. Explore how the platform represents these claims, checks them and records the assumptions behind them.
Architecture as types →Keep the whole system in view
Move from a language feature to its runtime contract, from an API to its implementation, and from a claim to the checks that support it. The guides connect these parts of Verum.