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 effects that do not need an explicit context — see reference/builtins for the full list.
  2. User-defined effects are explicit. The moment you need 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
     Linking hello
    Finished dev [unoptimized + debuginfo] target(s) in 1.2s
      Binary ./target/debug/hello (~53 KB)
        note CBGR ~15ns/check (use &checked for hot paths)
Interpreting src/main.vr
        note compiled in 0.00s
Hello from hello!
Sum: 15
        note executed in 0.00s

verum run compiles to VBC bytecode and executes it in the interpreter by default. Use --aot to compile-and-execute the native binary instead. For a release build:

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

The release build enables LLVM optimisations (O3, LTO), removes debug-only assertions, and strips the binary. Expect it to be about 40× smaller and 5-10× faster than the debug version on real code.

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
}

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: {<predicate>}
  --> src/main.vr:4:5
  │
2 │ 
3 │ fn return_zero() -> Positive {
4 │     0
  │     ^
5 │ }

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​

Create tests/greet_test.vr:

mount hello.*;

@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 = greet("Alice");
    assert(result.contains("Alice"));
}

Run tests:

$ verum test
   compiling hello v0.1.0 (./hello)
    finished in 0.2s
     running 2 tests
test greet_returns_non_empty ... ok
test greet_includes_name ... ok

test result: ok. 2 passed; 0 failed

@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 its effects 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​