Skip to main content

Hello, World

This is a five-minute exercise. By the end, you will have:

  • Created a project.
  • Run a Verum program.
  • Seen refinement types and the SMT solver in action.
  • Understood the shape of a typical Verum file.

Prerequisite: Installation — you need verum --version to work.

Create a project​

verum new asks which language profile to use — Verum has three (application, systems, research) that pick different default verification and safety settings. Pass --profile to answer up front:

$ verum new hello --profile application
         --> Creating binary project: hello (Application)
         --> Initializing git repository

    Finished Created hello project

Project configuration:
  Language profile: Application
  Profile details:  No unsafe, refinements + runtime checks (80% users)
  Template:         binary

Next steps:
  cd hello
  verum build
  verum run

$ cd hello
$ ls
benches  examples  README.md  src  tests  verum.toml

The scaffold gives you:

  • verum.toml — the package manifest (also accepted as Verum.toml). Cog name, version, dependencies, verify defaults, build profiles, runtime settings.
  • src/main.vr — the entry point (for binaries) or src/lib.vr (for libraries).
  • tests/, benches/, examples/ — standard subtrees the build system picks up automatically.

Pick the profile that fits the project:

ProfileDefaults
applicationno @unsafe, refinements + runtime checks, safe-by-default (recommended)
systems@unsafe allowed, manual memory control, FFI enabled
researchdependent types + formal proofs + SMT verification

See Project Structure for the full manifest schema.

The default program​

src/main.vr (as generated by the application profile):

// hello — Verum application
// Profile: application (safe by default, no @unsafe)

mount core.base.{List, Text, Maybe};

fn main() {
    let greeting: Text = "Hello from hello!";
    print(greeting);

    // Semantic types: List (not Vec), Text (not String), Maybe (not Option)
    let items: List<Int> = [1, 2, 3, 4, 5];
    let sum = items.fold(0, |acc, x| acc + x);
    print(f"Sum: {sum}");
}

Two things are worth noticing:

  1. print is a function, not a macro. No !, no println!. Standard output is one of a small set of built-in operations that do not need an explicit context — see reference/builtins for the full list.
  2. Context dependencies are explicit. When your function needs a database, a logger, a clock, or anything else beyond the built-ins, you declare it: fn handle(...) using [Database, Logger, Clock]. No globals, no @Autowired. The context system chapter covers the full propagation rules.

Build and run​

$ verum run --interp
Interpreting /path/to/hello/src/main.vr
Hello from hello!
Sum: 15

--interp compiles to VBC bytecode and executes it without linking a native executable. The CLI also reports timing, which depends on your machine and program.

Without an explicit mode, project execution follows [codegen].tier in the manifest; its default is "aot". Use verum run --aot to compile and execute a native binary, or build one for later execution:

$ verum build --release
$ ./target/release/hello
Hello from hello!
Sum: 15

The release profile enables optimisation and disables debug assertions by default. To remove symbols from the executable, request stripping explicitly:

verum build --release --strip

Binary size and execution time depend on your program, target, and build configuration. Measure the workloads you intend to deploy.

Play with a format string​

Format strings use f"...":

fn main() {
    let name = "Verum";
    let version = 1;
    print(f"Hello, {name} v{version}!");
}

Output:

Hello, Verum v1!

Splicing inside f"..." runs type-checking on each expression; {name} and {version} are both inferred and converted with their Display implementations. See language/tagged-literals for the full format literal grammar, including {value:04}-style format specs.

Adding a refinement type​

Refinement types attach a predicate to a type. Every value must satisfy it — checked at compile time.

Update src/main.vr:

type Greeting is Text { !self.is_empty() && self.len() < 100 };

fn greet(name: Text) -> Greeting {
    let msg = f"Hello, {name}!";
    print(msg);
    msg
}

fn main() {
    greet("World");
    greet("Verum");
}

Greeting is a Text constrained by a refinement predicate. greet is required to return a Greeting — the compiler must prove that every return path satisfies !self.is_empty() && self.len() < 100.

For this case — a literal "Hello, " concatenated with any short name — the SMT solver discharges the obligation trivially, and no runtime check is emitted.

Seeing the compiler reject an impossible refinement​

Use verum verify to discharge refinement obligations via the SMT backend. Try a refinement the compiler can clearly disprove:

type Positive is Int { self > 0 };

fn return_zero() -> Positive {
    0            // COMPILE ERROR: 0 does not satisfy {self > 0}
}

fn main() {
    let x: Positive = return_zero();
    print(f"x = {x}");
}
$ verum verify src/main.vr
         --> Verifying src/main.vr
error<E500>: refinement constraint failed: {… > 0}
  --> src/main.vr:4:5
  │
2 │ 
3 │ fn return_zero() -> Positive {
4 │     0
  │     ^
5 │ }
6 │ 
  │
error: compilation failed with 1 error

verum build in the application profile falls back to runtime checks for refinements the static check cannot dispatch. The separate verum verify entry point runs the dedicated SMT pipeline — routed through verum_smt.BackendSwitcher, which picks an adapter or a portfolio based on the theory mix of the predicate. Refinements that the solver proves are erased at runtime; refinements it cannot discharge fall through to runtime assertions under application.

For refinements over unbounded inputs (e.g. upper-bounding the length of an f-string formed from an arbitrary Text parameter), SMT capability depends on whether the predicate fits the decidable fragment of the chosen solver. See verification/gradual-verification for the full decision matrix.

Adding a test​

verum new already scaffolded tests/main_test.vr with two starter tests (test_example, test_semantic_types) — those run alongside the ones you add now, so don't be surprised to see four tests instead of two. Create tests/greet_test.vr. A test file needs no mount for the cog it belongs to; greet is in scope because the test is part of the same cog:

@test
fn greet_returns_non_empty() {
    let result = greet("Verum");
    assert(!result.is_empty());
    assert(result.len() < 100);
}

@test
fn greet_includes_name() {
    let result: Text = greet("Alice");
    assert(result.contains("Alice"));
}

Run tests:

$ verum test
     Testing hello v0.1.0 (aot)

running 4 tests (tier=aot, threads=2)
test greet_test::greet_returns_non_empty ... ok (…)
test greet_test::greet_includes_name ... ok (…)
test main_test::test_example ... ok (…)
test main_test::test_semantic_types ... ok (…)

test result: ok. 4 passed; 0 failed; 0 ignored; 4 total; finished in …

verum test builds and runs each test as a native binary — the tier=aot in the header — so the first run pays an AOT compile per test. The durations are elided here because they are dominated by that compile and by your machine.

note
Why let result: Text in the second test

greet returns Greeting, a refinement of Text. Calling .contains on that value goes through AOT method dispatch, which currently loses the base type and aborts — verum test runs at tier=aot by default, so the test would fail there while passing under the interpreter. Binding through the base type avoids it. .len() and .is_empty() on the same value are unaffected, which is why the first test needs no annotation.

@test marks a function as a test. Tests run in parallel by default; see tooling/cli for test filtering and options.

What you just did​

You:

  • Created a project with verum new.
  • Called a function with an explicit IO context.
  • Wrote a refinement-type-checked function.
  • Saw the SMT solver find a counter-example.
  • Wrote and ran tests.

That is the whole shape of day-to-day Verum. Every program:

  1. Declares the contexts it needs in the function signatures.
  2. Attaches invariants to types (refinements) and to functions (requires / ensures).
  3. Lets the compiler verify what the static checker can prove; SMT discharges the rest.
  4. Falls back to runtime assertions only where proofs are not yet written.

Next​