A systems language
that tells the truth.

Rung 0 · Type-level

The bad state cannot be written. The wrong program does not compile, so nothing is left to check at runtime.

decl Transaction @must_consume { conn: *Connection }

fn handle(t: Transaction) {
    if ok { commit(t) }
    // ERROR: on the else path, t is never consumed
}

Discharged by the type checker · no runtime cost

Rung 1 · Comptime fold

A literal decides it. The compiler computes the answer while compiling and emits nothing.

alias Index[n: usize] = usize @where(usize < n)

fn third(xs: [8]int) -> int {
    let i: Index[8] = 3     // 3 < 8, decided at comptime
    return xs[i]
}

Discharged at comptime · no runtime cost

Rung 2 · Summoned proof

Dynamic arithmetic. You summon the SMT extension, and it proves the predicate holds on every path.

alias Balance = i64 @where(i64 >= 0)

fn withdraw(b: Balance, amount: Balance) -> Balance {
    if amount > b { return b }
    return b - amount       // proved: b - amount >= 0 here
}

Discharged by an extension · no runtime cost

Rung 3 · Runtime check

Nobody could prove it statically, so it does not vanish: it becomes a check that traps on violation.

@requires(i < m.rows && j < m.cols)
fn (m: Matrix[T]) at(i: usize, j: usize) -> T

// a caller that cannot prove the bounds
// gets a trap instead of a wrong answer

Discharged at runtime · one check, in the open

Rung 4 · Advisory

The memory analyzer warns or hints. It never blocks the build and inserts no cost.

// mk analyze, or -Wmm on any build
fn checksum(data: []byte) -> u32 {
    tmp := mm.alloc(data.len())
    // hint: this pointer never escapes,
    //       it could be @consume
}

Advisory · a warning, no inserted cost

Rung 5 · Human

The last rung is you. You assert it in writing, at the operation, and the reason stays greppable.

@requires(i < buf.len)
fn read(buf: Buffer, i: usize) -> byte {
    return unsafe raw_read(buf.ptr + i)
        assume "Buffer invariant + @requires bounds"
}

Discharged by you · signed, never silent