The implemented language, its boundaries, and the commands that expose both.

Getting Started

Build the compiler from source, then check and run a small program.

Build

git clone https://github.com/sfw/forma.git
cd forma
cargo build --release
./target/release/forma --version

Hello, ownership

# hello.forma
f greet(ref name: Str) -> Unit
    print(f"Hello, {name}!")

f main()
    name = "Forma"
    greet(ref name)
    print(name)  # the shared loan ended; name is still owned here

forma check hello.forma
forma run hello.forma

The 0.2 Mental Model

Syntax and Bindings

Short keywords are canonical. Readable long aliases are accepted for many control and concurrency forms.

Bindings

limit = 10              # immutable binding
count := 0              # mutable binding
count := count + 1      # update mutable binding

items := load_items()
items := transform(items)  # transform consumes the old value and returns a new one

= and := express mutability, not ownership. Assigning a non-Copy value to another binding still moves it.

Canonical shorthand

Functions and expressions

f clamp(value: Int, low: Int, high: Int) -> Int
    if value < low then low
    else if value > high then high
    else value

f square(value: Int) -> Int = value * value

Operators and literals

The generated EBNF and JSON grammar remain authoritative for precedence, every accepted alias, and lexical detail.

Types

FORMA uses rank-1 inference, nominal generics, nominal traits, and static dispatch. Public function parameters and returns require annotations; local types can be inferred.

Fixed and dynamic collections are different promises

f fixed() -> [Int; 3] = [0; 3]

f dynamic() -> [Int]
    values := vec_new()
    values := vec_push(values, 1)
    values

Ownership and References

Owned, shared, and exclusive parameters

f consume(items: Vec[Item]) -> Unit
    # items is owned here

f inspect(ref items: Vec[Item]) -> Int
    items.len()

f update(ref mut items: Vec[Item]) -> Unit
    # exclusive access for this loan

• Passing a non-Copy value to an owned parameter moves it.
• ref permits reading while preserving the owner.
• ref mut is exclusive and permits mutation.
• clone(value) explicitly duplicates a Clone value.
• mv value may force or document a move; ordinary owned transfer does not require it.

Reference restrictions

References cannot be stored in ordinary aggregates, captured by escaping closures, or sent to another task. They may be returned only when derived from a reference parameter.

s Point { x: Int, y: Int }

# valid: returned reference is derived from p
f get_x(p: &Point) -> &Int = &p.x

# invalid: a reference to a local would escape
# f bad() -> &Int
#     value = 1
#     &value

Compiler-known traits

Copy, Clone, Drop, Send, and Sync receive structural validation. A type with Drop is never Copy. Each initialized owned place is destroyed exactly once.

Functions, Structs, and Enums

s Point { x: Int, y: Int }

e Direction = North | South | East | West

e Maybe[T] = Present(T) | Absent

f origin() -> Point
    Point { x: 0, y: 0 }

i Point
    f translated(&self, dx: Int, dy: Int) -> Point
        Point { x: self.x + dx, y: self.y + dy }

Enums and pattern matching form algebraic data types. Core LLVM currently documents uniform scalar-payload enums; broader Hosted behavior may exceed Core backend support.

Control Flow and Matching

f describe(value: Bool?) -> Str
    m value
        Some(true) -> "yes"
        Some(false) -> "no"
        None -> "unknown"

f sum_to(limit: Int) -> Int
    total := 0
    i := 0
    wh i <= limit
        total := total + i
        i := i + 1
    total

Matches over finite algebraic domains must be exhaustive. Guards do not establish exhaustiveness; unreachable arms are diagnosed. Infinite or open domains require a wildcard unless the compiler knows a finite refined domain.

Error Handling and Closures

Expected failure uses Option or Result. Forma does not use exceptions for ordinary recoverable errors.

f load(path: Str) -> Str!Str
    content = file_read(path)?
    Ok(content)

f port(value: Str?) -> Int
    text = value ?? "8080"
    str_to_int(text) ?? 8080

f transform(values: [Int]) -> [Int]
    map(values, |value: Int| value * 2)

• ? propagates a Result error.
• ?? supplies an Option default.
• ! unwraps and panics on failure; prefer explicit handling at public boundaries.
• Closure parameters are typed. Escaping closures cannot capture references.
• The initial unrecoverable panic strategy is abort, not unwinding.

Generics and Traits

f identity[T](value: T) -> T = value

t Named
    f name(&self) -> Str

f label[T: Named](ref value: T) -> Str
    value.name()

Dispatch is static. At most one implementation may apply to a concrete trait/type pair, and the implementation must belong to the package defining the trait or type. Overlapping blanket implementations and specialization are disallowed in 0.2.

Resolution order is deterministic: inherent methods, explicitly imported traits, then prelude traits. Remaining ambiguity is an error, never a source-order choice.

Effects and Capabilities

Effects are inferred through the call graph and describe authority a function may use. They do not grant authority. Runtime flags grant capabilities to one execution.

forma run reader.forma --allow-read
forma run writer.forma --allow-write
forma run client.forma --allow-network
forma run tool.forma --allow-exec
forma run configured.forma --allow-env
forma run ffi.forma --allow-unsafe
forma run trusted.forma --allow-all

Structured Concurrency

as f compute(value: Int) -> Int
    value * value

as f main()
    task = sp compute(12)
    result = aw task
    print(result)

• Task captures move into the child and must satisfy compiler-known Send.
• References cannot cross task boundaries.
• Task handles are affine: await, cancel, return, or explicitly detach them.
• Cancellation, deadlines, task limits, and a subset of capabilities propagate.
• Channels and mutexes are Hosted library/runtime handles; sending moves the value.

Contracts

Contracts are parsed language nodes, not comments. Function contracts describe transitions; struct invariants describe every valid externally observable value.

@inv(balance >= 0, "balance cannot be negative")
s Account
    balance: Int

@pre(n >= 0, "n must be non-negative")
@post(result >= 1)
f factorial(n: Int) -> Int
    if n <= 1 then 1 else n * factorial(n - 1)

@nonempty(items)
@sorted(result)
@permutation(items, result)
f verified_sort(items: [Int]) -> [Int]
    sort_ints(items)

@inv fields are in scope by name. Forma checks invariants after construction, at function entry and return, and when a ref mut borrow returns. Exclusive mutation may be temporarily inconsistent, but must restore validity before return. old(...) and result remain function-contract concepts.

Runtime enforcement is not formal proof. Formal verification treats invariant-bearing parameters as entry assumptions, symbolically tracks projected mutation, and generates obligations at struct construction, direct pure-call, and return boundaries. For named structs and tuples whose leaves are supported Bool or signed 64-bit Int values, Z3 can report invariant establishment and preservation as PROVED or produce a reproducible COUNTEREXAMPLE. Untrusted JSON, TOML, network, and database data should be validated by a fallible decoder before constructing an invariant-bearing value.

0.2 profile boundary: the Hosted interpreter enforces function contracts and struct invariants. The LLVM path type-checks their declarations but does not yet inject native runtime checks.

Verification Levels

# Reproducible generated contract tests
forma verify rules.forma --level test --examples 200 --seed 42 --report

# Complete supported finite domain
forma verify rules.forma --level exhaustive --max-domain 4096 --report

# Formal attempt; Experimental subset
forma verify rules.forma --level formal --report

# Automation output
forma verify src/ --level test --report --format json

Verification runs with capabilities restricted by default. --allow-side-effects opts generated examples into full capabilities; effectful or unsafe code without a formal model remains non-proof work.

Formal mode invokes z3 by default. FORMA_SMT_SOLVER can select another solver command that accepts the same stdin flags. A missing, failed, or timed-out solver produces UNKNOWN.

The current formal subset follows acyclic control flow path by path and supports checked signed 64-bit arithmetic, Bool, tuples, named structs, field and tuple projection, structural equality, projected field updates, direct pure-call inlining, and struct-invariant establishment and return preservation. Unsatisfiable preconditions or invariant assumptions are rejected as vacuous. Loops, recursive or indirect calls, effects, arrays and vectors, indexing, enums, and reference/dereference reasoning remain explicit UNKNOWN boundaries.

Explain before you verify

forma explain rules.forma --format human
forma explain rules.forma --format json --examples=3 --seed 42

Modules and Packages

One file defines one module in the initial model. Imports are importer-relative or package-rooted, explicit exports are deterministic, and pub controls visibility.

us math.tools
us collections.{Vec, Map}
us std.fs -> filesystem

pub md api
    pub f answer() -> Int = 42

Project files

demo/
├── forma.toml
├── forma.lock
└── src/
    └── main.forma

[package]
name = "demo"
version = "0.1.0"

[deps]
math = { path = "../math" }

0.2 resolves deterministic local path dependencies. Registry and Git sources are future package-manager work and are rejected rather than guessed. Hierarchical namespace-preserving scopes will grow from today’s deterministic explicit-export boundary.

CLI and Tooling

Core workflow

forma check app.forma
forma check app.forma --partial
forma check app.forma --error-format json

forma run app.forma
forma build app.forma -o app -O 2

forma fmt app.forma
forma fmt app.forma --write
forma fmt app.forma --check

forma build requires a compiler built with cargo build --release --features llvm and a compatible LLVM 18 installation. The LLVM backend is Experimental beyond its documented Core subset.

Semantic queries and editor support

forma typeof app.forma --position 12:8
forma complete app.forma --position 12:8
forma lsp

Diagnostics, hover/completion data, symbols, navigation, references, signatures, and formatting reuse the shared compiler session. Richer member ranking, rename/refactor flows, and deeper cross-file UX remain evolution work.

Grammar and contract tooling

forma grammar --format ebnf > forma.ebnf
forma grammar --format json > forma-grammar.json
forma explain app.forma --format markdown
forma verify app.forma --report --format json

Project and development commands

forma new my-app
forma init
forma repl
forma lex app.forma
forma parse app.forma

Builtins, Standard Library, and Unsafe Code

The generated builtin registry is the exact API index. It records each signature, parameter ownership mode, inferred effects, required capability, interpreter support, native support, and verification support.

# Machine-readable compiler surface
docs/builtins.json

# Forma modules built on that surface
std/core.forma   std/io.forma     std/string.forma
std/vec.forma    std/map.forma    std/iter.forma
std/json.forma   std/datetime.forma

Do not infer a builtin from its name or from another language. Agents should query completion or read the generated registry, then confirm usage with forma check.

Feature Profiles

Support is transitive through direct calls and reported per function. A Core-looking wrapper around a Hosted builtin remains unsupported by Core LLVM or formal verification.

Compiler-Checked Examples

The viewer below is restricted to showcase files that pass the current 0.2 ownership-aware forma check gate. The linked repository files remain the source of truth.

Known 0.2 Boundaries

• Stability: 0.x semantics and diagnostics do not yet carry a 1.0 compatibility promise.
• LLVM: the Core subset has native coverage and differential tests; the whole backend remains Experimental until every Core example has parity.
• Formal verification: SMT proof is Experimental and intentionally limited to a pure supported subset.
• Packages: deterministic local paths ship; registry and Git sources do not.
• Isolation: process isolation is optional defense in depth, not a replacement for effects and runtime capability checks.
• Destructors: Core uses compiler-generated drop glue; observable user-defined destructor bodies remain Experimental.
• Bytecode: no VM is planned until measurements justify startup, portability, or sandboxing costs.

At a Glance

These four cards are a memory aid. The complete generated language and builtin surface follows below.

owned:   value: T
shared:  ref value: T
mutable: ref mut value: T
clone:   clone(value)
move:    mv value

--level test
--level exhaustive
--level formal
--examples N
--max-domain N
--seed N
--max-steps N
--timeout MS

--allow-read
--allow-write
--allow-network
--allow-exec
--allow-env
--allow-unsafe
--allow-all

Core
Hosted
Native
Experimental

Complete Searchable Reference

This index is generated from Forma 0.2’s grammar, builtin registry, parser, and standard library. It includes every canonical keyword and alias, literal form, grammar production and operator, type and language form (including @inv), named contract pattern, standard-library export, CLI/evidence term, and compiler-registered builtin.