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 Data computation/conversion
validates Pure Boolean check (returns Boolean)
reads Pure Non-mutating data access
creates Pure Construct new value
matches Pure Algebraic dispatch
inputs IO Read from external world
outputs IO Write to external world
streams IO Blocking IO loop
detached Async Fire-and-forget coroutine
attached Async Awaited coroutine
listens Async Event dispatcher

Key Concepts

Intent Verbs

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

transforms 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)
transforms 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

transforms 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)&