The Seven Runes

Every statement in Futuruna begins with a rune — a single character that declares what the statement is.

Rune	Question	What it does
#	What exists?	Types, effects, traits, impls
>	What happens?	Functions, actors, modules
|	What must be true?	Rules, invariants, handlers, scopes
=	What is?	Bindings, monadic bind
~	What flows?	Reactive streams, subjects
@	Where do proofs stop?	IO, imports, dependencies, meta
?	Prove it.	Verification demands

---

# -- What exists

Defines the shape of data: types, algebraic effects, traits, and implementations.

Struct (single-variant product type)

# Point(x: Float, y: Float)
# Weather(city: City, temp: Float, condition: Condition, wind_kph: Float)

Construction uses positional arguments:

= p = Point(1.0, 2.0)
= w = Weather(Copenhagen, 22.0, Sunny, 10.0)

Fields are accessed with dot notation: w.temp, w.condition.

Enum (multi-variant algebraic data type)

# Color = Red | Green | Blue
# Shape = Circle(radius: Float) | Rectangle(width: Float, height: Float)
# Option(a) = None | Some(a)
# List(a) = Nil | Cons(head: a, tail: List(a))

ADT with methods

# Color = Red | Green | Blue {
    > name(c) -> String {
        match c {
            | Red -> "red"
            | Green -> "green"
            | Blue -> "blue"
        }
    }
}

Methods are standalone functions. The first parameter (without type annotation) receives the ADT type.

Product types with rule members

# TaxCase(person: Person, rates: Rates) {
    | taxable_income() -> person.gross_income
    | tax_due() -> taxable_income() * rates.percent / 100

    > label() -> String { "tax:" + show(tax_due()) }
}

= tax = TaxCase(Person(1000), Rates(25))
= due = tax.tax_due()
= label = tax.label()

When a product type body contains | entries, those entries are rule members of the product value. This is the RuleScope model: a pure calculation object whose constructor inputs are visible inside scoped rules. Rule members can call sibling rule members, ordinary global functions/rules, and use under / exception with the same priority semantics as top-level rules. Rule member names do not leak globally. Scoped dispatch matches both name and arity, so a same-named member with a different parameter count does not hide an ordinary global rule. Pure zero-argument rule members are memoized for the duration of one root member evaluation; repeated dependencies therefore retain value semantics without repeatedly evaluating the same rule cascade.

The same product body may contain ordinary > methods. Methods share the product instance and can call rule members with tax_due() or self.tax_due(). Fields are also available in product methods, so person.gross_income works in both | rule members and > methods. A | rule member and > method cannot use the same member name.

RuleScope is different from | scope Name { ... }: | scope owns reactive lifecycle work such as subjects, streams, subscriptions, and teardown. A RuleScope has no mutation or lifecycle ownership.

Effect declaration

# effect Console {
    > say(msg: String) -> ()
    > ask(prompt: String) -> String
}

Defines abstract operations that callers can intercept via | handle.

Trait declaration

# trait Printable {
    > display(self) -> String
}

# trait Greetable {
    > greet(self) -> String {
        "Hello, " + display(self)    -- default implementation
    }
}

Impl block

# impl Printable for Color {
    > display(self) -> String {
        match self {
            | Red -> "Red"
            | Green -> "Green"
            | Blue -> "Blue"
        }
    }
}

---

> -- What happens

Defines transformation: functions, actors, and modules.

Function

> add(a: Int, b: Int) -> Int { a + b }

> greet(name: String) -> String {
    "Hello, " + name + "!"
}

Parameters can omit type annotations (inferred). Return type after ->.

Function with effects

> process(item: String) -> String with Console, Logger {
    say("Processing: " + item)
    log("info", "processed " + item)
    item
}

The with clause declares which effects the function may perform.

Function with inout (mutable value semantics)

> sort_vec(xs: inout List(Int)) -> () {
    @ rust { xs.sort(); }
}

inout parameters are passed as &mut T. The caller's value is mutated in place.

Generic function

> map_list(xs: List(a), f: a -> b) -> List(b) {
    match xs {
        | Nil -> Nil
        | Cons(h, t) -> Cons(f(h), map_list(t, f))
    }
}

Lowercase type variables (a, b) become Rust generics.

Actor

> actor counter(state: Int) {
    | Increment -> state + 1
    | Decrement -> state - 1
    | Reset -> 0
}

Actors have a state parameter and message handlers. Each handler returns the new state. Compiles to a tokio task with an mpsc channel.

Module

> module Math {
    > square(x: Int) -> Int { x * x }
    > cube(x: Int) -> Int { x * x * x }
}

Modules can be nested. Contents are accessed via Math.square(5).

---

| -- What must be true

Declares rules, invariants, effect handlers, and scopes. The most versatile rune.

Logic rules (Prolog-style)

| taxable(person) -> resident(person), has_income(person)

Default rules with overrides (Catala-style)

| advisory(w) -> "all clear"
| advisory(w) -> "heat warning" under w.temp > 35.0
| exception heatwave advisory(w) -> "danger" under w.temp > 45.0

Rules are evaluated by priority tier: exceptions, guarded defaults, ordinary clauses, then an unguarded default. Within one tier, source order is authoritative and the first applicable rule wins. Put the more specific of two overlapping guards first. under adds a guard condition. exception <label> places the rule in the exception tier for the same head. The label (here heatwave) names the exception for readability and debugging; it does not affect priority.

Named invariants (verification targets)

| name: subject_expr -> predicate_expr

Defines a named predicate that ? can check. The subject expression is the value being tested; the predicate expression must return Bool.

= balance = 1000
= max_supply = 1000000
| balance_bounded: balance -> balance >= 0 && balance <= max_supply

The name before : is the invariant name. The expression between : and -> is the subject (captured by ? name: val). The expression after -> is the predicate.

Effect handlers

= result = | handle Console {
    | say(msg) -> { @ print("[console] " + msg); resume(()) }
    | ask(prompt) -> { @ print("[console] " + prompt); resume("default") }
} in greet("World")

Intercepts effect operations from the in body. resume(value) continues execution with the given return value.

Scope blocks (lifecycle management)

| scope WeatherStation {
    ~ readings = subject()
    readings <- 42
    @ print(show(readings))
}

Scopes group statements with lifecycle management. Subjects, streams, and live subscriptions within a scope are cleaned up when the scope ends. Named scopes are also the explicit owner required for live subscriptions started inside ordinary functions. See docs/stream-lifetimes.md.

Match arms

Inside a match expression, | introduces each arm (see basics.md for match syntax).

---

= -- What is

Binds a name to a value. Ground truth at a point in time.

Simple binding

= x = 42
= name = "hello"
= result = add(20, 22)

With type annotation

= x: Int = 42
= name: String = "hello"

Top-level initialization order

Unique top-level bindings may refer to bindings declared later, directly or through functions, rules, and RuleScope members. Futuruna initializes the required dependencies first in both interpreted and compiled execution. Declarative @ comptime and @ export annotations remain attached when a binding moves with its dependencies.

| answer() -> base + 1

= result = answer()
= base = 41

Rebound names keep source-order semantics. A cycle between unique top-level bindings is rejected with the complete initialization path.

Monadic bind (early return)

= value <- parse_int("42")

If the expression returns Ok(v) or Some(v), binds v and continues. If Err(e) or None, returns immediately (early return). Equivalent to Rust's ? operator.

> add_parsed(a_str: String, b_str: String) -> Result(Int, String) {
    = a <- parse_int(a_str)
    = b <- parse_int(b_str)
    Ok(a + b)
}

---

~ -- What flows

Declares reactive streams and subscribes to them. Values that change over time.

The ~ rune has two forms:

1. Binding (~ name = expr) — creates a stream
2. Subscription (~ expr | arms) — consumes a stream with event handling

Stream binding

~ nums = from_list([1, 2, 3, 4, 5])
~ doubled = map(nums, |x| x * 2)
~ big = nums |> filter(|x| x > 3)

Subscription (~ + |)

-- Subscribe to a stream with value handling
~ nums | x -> { @ print(show(x)) }

-- With error handling
~ nums
    | x -> { @ print(show(x)) }
    | Err(e) -> { @ print("error: " + show(e)) }

-- Full lifecycle (value + error + completion)
~ nums
    | x -> { @ print(show(x)) }
    | Err(e) -> { @ print("error: " + show(e)) }
    | Complete -> { @ print("stream ended") }

-- Pipeline ending in subscription
~ sensor |> filter(valid) |> map(to_celsius)
    | t -> { display(t) }
    | Err(e) -> { log(e) }

The | arms handle three stream events: values, errors, and completion. This replaces for loops on streams. Use for for lists/ranges; use ~ + | for streams.

See streams.md for the full stream API and subscription reference. For lifetime ownership rules around function-local subscriptions, see docs/stream-lifetimes.md.

Subject creation (push-based streams)

~ clicks = subject()              -- empty subject
~ temp = subject(20.0)            -- with initial value
~ history = subject(0, 10)        -- replay subject (buffer last 10)

Push values into subjects

clicks <- "click1"
clicks <- "click2"
temp <- 25.0

Subject properties

clicks.count       -- number of values pushed
temp.latest        -- most recent value

---

@ -- Where proofs stop

The boundary between the verified world and effects. Every @ says: formal reasoning cannot reach here.

Print (IO)

@ print("hello")
@ print("value: " + show(x))

Import (multi-file)

@ import ./utils                    -- flat import: merge all definitions
@ import Utils from ./utils         -- qualified: access via Utils.function()
@ import #a1b2c3 from ./utils       -- content-addressed import

Use (Rust items)

@ use std::collections::HashMap
@ use std::io::*

Use @ import for Futuruna modules.

Depend (Cargo dependencies)

@ depend "serde" "1"
@ depend "tokio" "1"

Export (visibility)

@ export
> public_function() -> Int { 42 }

Marks the next definition as public. Without @ export, definitions are private.

Calculate (typed external input)

@ calculate("Danish personal income tax")
| calculate_tax(input: TaxInput) -> TaxResult(annual_tax = annual_tax(input))

Marks one typed rule or function as a discoverable calculation boundary for runa schema, runa template, and runa call. This annotation does not perform an effect or change rule semantics. Its optional single string labels the whole calculation; nested input labels and questions remain field metadata. See calculations.md.

Comptime (compile-time evaluation)

@ comptime = table = generate_lookup(1000)

The expression is evaluated at compile time and inlined as a constant.

Rust escape hatch

@ rust {
    fn fast_sort(x: &mut [f64]) {
        x.sort_unstable_by(|a, b| a.partial_cmp(b).unwrap());
    }
}

Inline raw Rust code. Handles nested braces, strings, and comments correctly.

---

? -- Prove it

Interrogates what other runes declared. Checks invariants defined with |.

How it works

1. Define an invariant with |:

   | balance_ok: balance -> balance >= 0 && balance <= max_supply
   

2. Check it with ?:

   ? balance_ok
   

The six forms

Without else, failure halts the program. With else, failure is handled and execution continues.

-- Form 1: Bare check (halt on failure)
? balance_ok

-- Form 2: Pass block (halt on failure)
? balance_ok -> {
    @ print("Balance verified")
}

-- Form 3: Capture + pass (halt on failure)
? balance_ok: val -> {
    @ print("Balance is " + show(val))
}

-- Form 4: Else block (no halt)
? balance_ok else {
    @ print("Balance violated!")
}

-- Form 5: Pass + else (no halt)
? balance_ok -> {
    @ print("OK")
} else {
    @ print("FAIL")
}

-- Form 6: Full form — capture + pass + else (no halt)
? balance_ok: val -> {
    @ print("Verified: " + show(val))
} else {
    @ print("Violation: " + show(val))
}

The : val capture binds the subject value (the data being checked), not the boolean result.

Verify all invariants

? all                                          -- check all, halt on any failure
? all -> { @ print("All OK") }                -- with pass block
? all -> { @ print("OK") } else { @ print("Some failed") }   -- with both

Three assurance levels

The same ? line works at three levels of assurance:

• runa run — evaluates the predicate with current values at runtime
• runa build — emits debug_assert!() in the compiled binary
• runa verify — translates to SMT-LIB2 and invokes Z3 to prove for all inputs

Verifying rule dispatch

runa verify can translate pure, total, non-recursive | rule groups directly, including rules inside a product RuleScope. Conditions and exceptions use the same precedence as execution; there is no need to restate the rule cascade as a separate > function.

# TaxCase(income: Int) {
    | rate_percent() -> 25
    | rate_percent() -> 30 under income > 500000
    | exception low_income rate_percent() -> 20 under income < 100000
    | tax_due() -> income * rate_percent() / 100
}

= high_income_case = TaxCase(income = 600000)
| high_income_tax: high_income_case.tax_due() -> high_income_case.tax_due() == 180000

Plain imports are resolved recursively for verification. An exception declared by an importing file therefore extends the imported rule group and keeps its normal exception priority. Within one priority tier, imported declarations come before declarations in the importing file and the first applicable rule wins, just as it does during execution.

The solver path fails closed with a diagnostic for partial non-Boolean rules, recursive dispatch, higher-order parameters, effects, and other expressions outside its current first-order subset. runa verify remains a Preview surface.