Verum

type OrderId is (Int);          // newtype — not just an Int

fn total(orders: &Map<OrderId, Order>) -> Result<Money, PriceError> {
    let mut sum = Money.zero();
    for (_, order) in orders.iter() {
        sum = sum.add(order.price()?);   // ? propagates the error
    }
    Ok(sum)
}

fn receipt(id: OrderId, m: Money) -> Text {
    f"order {id}: {m}"                   // typed interpolation
}

type Shape is
    | Circle(Float)
    | Rectangle(Float, Float)
    | Square(Float);

fn describe(s: Shape) -> Text {
    match s {
        Circle(_)                     => "a circle".clone(),
        Rectangle(w, h) if w == h     => "a square in disguise".clone(),
        Rectangle(_, _)               => "a rectangle".clone(),
        Square(_)                     => "a square".clone(),
    }
}
// Add a variant to Shape and this match stops compiling
// until you say what it means. That is the point.

type Drawable is protocol {
    fn draw(&self) -> Text;
    fn area(&self) -> Float;
};

implement Drawable for Circle {
    fn draw(&self) -> Text { f"Circle(r={self.radius})" }
    fn area(&self) -> Float { 3.14159 * self.radius * self.radius }
}

fn report<S: Drawable>(s: &S) {
    print(f"{s.draw()} covers {s.area()}");
}

async fn producer(tx: Sender<Int>, n: Int) {
    let mut i = 0;
    while i < n {
        tx.send(i).await;      // blocks when the buffer is full:
        i = i + 1;             // backpressure is automatic
    }
}

fn main() {
    let (tx, rx): (Sender<Int>, Receiver<Int>) = bounded(4);
    let p = spawn(producer(tx, 100));
    let c = spawn(consume(rx));
    p.join();
    c.join();
}

mount core.database.sqlite.native.l7_api.{
    Database, DbError, open_readwrite};

fn example() -> Result<(), DbError> {
    let mut db: Database = open_readwrite()?;
    db.execute(&"CREATE TABLE users (id INTEGER PRIMARY KEY, \
                 name TEXT NOT NULL)".into())?;
    db.execute(&"INSERT INTO users (id, name) \
                 VALUES (1, 'alice'), (2, 'bob')".into())?;
    let rows = db.query_all(&"SELECT id, name FROM users \
                              ORDER BY id".into())?;
    for row in rows.iter() { print(f"{row[1].as_text()}"); }
    Ok(())
}
// A SQL engine written in Verum, embedded in the toolchain.

fn sum_ages(users: &List<User>) -> Int {
    let mut total = 0;
    for u in users.iter() {           // &u: &User — checked default
        let age: &checked Int = &checked u.age;
        total += *age;                // 0 ns — compiler proved safe
    }
    total
}

// $ verum analyze --escape
// sum_ages: most references promoted to &checked
//   safe by default, zero-cost where provable

// Embedded build — no malloc, no libc, no stdio.
@no_std
@target("thumbv7em-none-eabihf")
module firmware.uart;

mount sys.mmio;

public fn write_byte(b: u8)
    using [UartRegisters]
{
    while !UartRegisters.tx_empty() {}
    UartRegisters.tx_data.write(b);
}

// Compiles to a microcontroller binary. Same language as
// the verified theorem corpus.

// Runtime — caller provides Database and Logger.
fn handle(req: &Request) -> Response
    using [Database, Logger]
{
    Logger.info(f"{req.method} {req.path}");
    Database.find_user(req.auth)
        .map(|u| Response.ok(&u))
        .unwrap_or_else(|| Response.unauthorised())
}

// Compile time — the compiler provides TypeInfo.
meta fn field_count<T>() -> Int using [TypeInfo] {
    TypeInfo.fields_of<T>().len()
}

@arch_module(
    lifecycle: Lifecycle.Definition,
    exposes:   [Capability.Read(Database("ledger")),
                Capability.Network(Grpc, Outbound)],
    requires:  [Capability.Read(Logger)],
    preserves: [BoundaryInvariant.AllOrNothing,
                BoundaryInvariant.AuthenticatedFirst],
    composes_with: ["payment.fraud", "payment.audit"],
)
module payment.settlement;
// Capability escalation, boundary violation, lifecycle
// regression — each is a compile-time diagnostic with a
// stable code. Claiming Theorem status without a closed
// proof triple is itself an error the compiler catches.

// Same body, different tiers.
type NonNeg is Int { self >= 0 };

@verify(runtime)        // assertion at runtime
fn abs_r(x: Int) -> NonNeg { if x >= 0 { x } else { -x } }

@verify(formal)         // SMT-proved at compile time
fn abs_f(x: Int) -> NonNeg { if x >= 0 { x } else { -x } }

@verify(certified)      // certificate exported, kernel re-checks
fn abs_c(x: Int) -> NonNeg { if x >= 0 { x } else { -x } }

// Promote the tier when the function lands in a load-bearing
// role. Demote when the role changes back. Same source.