Skip to content

Functions & Verbs

Every Prove function declares its purpose with a verb. The verb IS the declaration — the compiler verifies the implementation matches the declared intent.

Quick Reference

Verb Family Purpose
transforms Pure Failable data computation/conversion
validates Pure Boolean check (returns Boolean)
derives Pure Non-mutating data access or derivation
creates Pure Construct new value
matches Pure Pure algebraic dispatch
inputs IO Read from external world
outputs IO Write to external world
dispatches IO IO algebraic dispatch (pattern match with IO in arms)
streams IO Blocking IO loop
detached Async Fire-and-forget coroutine
attached Async Awaited coroutine
listens Async Event dispatcher
renders Async UI render loop with mutable state

Key Concepts

Intent Verbs

Functions declare their purpose through verbs. The compiler enforces that implementations match declared intent:

derives double(n Integer) Integer
  ensures result == n * 2
from
    n * 2

validates is_positive(n Integer)
from
    n > 0

See Intent Verbs for detailed reference.

Async Verbs

Structured concurrency via cooperative coroutines:

detached log(msg String)
from
    console(msg)

attached fetch(url String) String
from
    request(url)&

See Async Verbs for detailed reference.

Verb Dispatch

The same name can have multiple verbs — the compiler resolves which to call from context:

validates email(String)
creates email(String) Email
inputs email(Integer) Email!

See Call Resolution for how this works.

Lambdas & Iteration

No loops — use map, filter, reduce:

names as List<String> = map(users, |u| u.name)
active as List<User> = filter(users, |u| u.active)
total as Decimal = reduce(prices, 0, |acc, p| acc + p)

See Lambdas & Iteration for detailed reference.

Examples

Pure Function

matches area(s Shape) Decimal
from
    match s
        Circle(r) => pi * r * r
        Rect(w, h) => w * h

IO Function

inputs users() List<User>!
from
    query(db, "SELECT * FROM users")!

Async Function

detached log(event Event)
from
    console(event.message)

attached fetch(url String) String
from
    request(url)&