FORMA Complete Guide

Getting Started

Install FORMA and run your first program in under 5 minutes.

Installation

# Clone and build
git clone https://github.com/sfw/forma.git
cd forma
cargo build --release

# Add to PATH (optional)
export PATH="$PATH:$(pwd)/target/release"

# Verify installation
forma --version

Your First Program

Create hello.forma:

# hello.forma - Your first FORMA program
f main()
    print("Hello, FORMA!")

    # Variables: = for immutable, := for mutable
    name = "World"
    print(f"Hello, {name}!")

forma run hello.forma
# Output:
# Hello, FORMA!
# Hello, World!

A More Complete Example

Here's a program that demonstrates contracts, functions, and error handling:

# calculator.forma - Safe arithmetic with contracts

# Precondition: divisor cannot be zero
@pre(b != 0, "division by zero")
f safe_divide(a: Int, b: Int) -> Int
    a / b

# Function with Option return for partial operations
f find_first_even(numbers: [Int]) -> Int?
    for n in numbers
        if n % 2 == 0
            ret Some(n)
    None

# Main entry point
f main()
    # Safe division with contract protection
    result = safe_divide(10, 2)
    print(f"10 / 2 = {result}")

    # Finding values with Option handling
    nums = [1, 3, 5, 6, 7, 8]
    m find_first_even(nums)
        Some(n) -> print(f"First even: {n}")
        None -> print("No even numbers found")

    # Using ?? for default values
    first = find_first_even([1, 3, 5]) ?? 0
    print(f"First even or default: {first}")

forma run calculator.forma
# Output:
# 10 / 2 = 5
# First even: 6
# First even or default: 0

Project Structure

# Create a new project
forma new my_project
cd my_project

# Project layout
my_project/
├── src/
│   └── main.forma    # Entry point
├── tests/
│   └── test_main.forma
└── forma.toml        # Project configuration

LLM Onboarding Guide

FORMA is a new language without the training data history of Python or Rust. This section provides everything you need to get an LLM or AI agent generating correct FORMA code.

The Challenge

LLMs are trained primarily on established languages. FORMA's syntax—short keywords like f, s, m, indentation-based blocks, and the contract system—may not appear in training data. This guide shows you how to provide the context an LLM needs to generate FORMA reliably.

Step 1: System Prompt Context

Include FORMA syntax basics in your system prompt. Here's a minimal reference:

You are writing code in FORMA, an AI-optimized systems language. Key syntax:

KEYWORDS: f=function, s=struct, e=enum, t=trait, i=impl, m=match
          wh=while, lp=loop, br=break, ct=continue, ret=return
          as f=async function, aw=await, sp=spawn, us=use

TYPES: Int, Float, Bool, Str, Char
       [T]=list, Map[K,V]=map, T?=Option, T!E=Result, (A,B)=tuple

VARIABLES: x = 42 (immutable), y := 0 (mutable)
           y := y + 1 (reassignment also uses :=)

FUNCTIONS:
  f add(a: Int, b: Int) -> Int
      a + b

CONTRACTS (preconditions/postconditions):
  @pre(n >= 0)
  @post(result >= 1)
  f factorial(n: Int) -> Int
      if n <= 1 then 1 else n * factorial(n - 1)

PATTERN MATCHING:
  m value
      Some(x) -> process(x)
      None -> default()

STRUCTS AND METHODS:
  s Point { x: Float, y: Float }
  i Point
      f distance(&self) -> Float
          sqrt(self.x * self.x + self.y * self.y)

ERROR HANDLING:
  ? = propagate error, ?? = default value, ! = unwrap (panic)
  result = risky_operation()?  # Returns early on Err
  value = maybe_none ?? 0      # Default if None

Step 2: Grammar-Constrained Generation

For guaranteed syntactic correctness, use constrained decoding with FORMA's grammar:

# Export grammar for your LLM pipeline
forma grammar --format json > forma-grammar.json

# Use with llama.cpp, Outlines, or other constrained decoding tools
# The grammar ensures only valid FORMA syntax is generated

This eliminates syntax errors entirely—the LLM can only produce valid tokens.

Step 3: Few-Shot Examples

Include working examples in your prompt. Here are templates for common patterns:

# Function with contracts
@pre(items.len() > 0)
@post(forall x in items: result >= x)
f max_element(items: [Int]) -> Int
    max := items[0]
    for x in items
        if x > max
            max := x
    max

# Struct with methods
s User
    id: Int
    name: Str
    email: Str

i User
    f new(id: Int, name: Str, email: Str) -> User
        User { id: id, name: name, email: email }

    f display(&self) -> Str
        f"User({self.id}, {self.name})"

# Error handling with Result
f parse_config(path: Str) -> Config!Str
    content = file_read(path)?
    data = json_parse(content)?
    Ok(Config {
        host: json_get(data, "host") ?? "localhost",
        port: json_get(data, "port") ?? 8080
    })

# Async HTTP handler
as f handle_request(req: Request) -> Response!Str
    user_id = json_get(req.body, "user_id")?
    user = aw fetch_user(user_id)?
    Ok(Response { status: 200, body: json_stringify(user) })

Step 4: Verification Feedback Loop

Use FORMA's toolchain to validate and correct AI-generated code:

# 1. Check syntax and types (JSON for LLM parsing)
forma check generated.forma --error-format json

# If errors, feed the JSON back to the LLM:
# {"errors":[{"line":5,"code":"TYPE","expected":"Int","found":"Str"}]}

# 2. Verify contracts hold
forma verify generated.forma --examples 100

# 3. Explain contracts for human review
forma explain generated.forma --format human

Step 5: Contract Specification Prompting

The most effective approach: specify what the code should do with contracts, let the LLM implement how:

Write a FORMA function that sorts an array of integers.

Requirements (express as contracts):
- Input must not be empty
- Output must be sorted in ascending order
- Output must contain exactly the same elements as input

The function should be named `verified_sort` and take `items: [Int]` as input.

This produces:

@nonempty(items)
@sorted(result)
@permutation(items, result)
f verified_sort(items: [Int]) -> [Int]
    # LLM implements sorting algorithm here
    # Contracts ensure correctness regardless of implementation

Complete Onboarding Workflow

Tips for Reliable Generation

• Start with contracts: Specify what the code should do before asking for implementation
• Use explicit types: Include type annotations to reduce ambiguity
• Request small functions: Smaller functions with clear contracts are more reliable
• Feed back errors: Use JSON error output to help the LLM self-correct
• Verify iteratively: Run forma verify after each generation and refine

Syntax Basics

FORMA uses indentation-based syntax with short keywords for token efficiency.

Variables and Assignment

FORMA uses two assignment operators with distinct meanings:

# Immutable variables with = (cannot be changed after creation)
x = 42
name = "Alice"
config = load_config()

# Mutable variables with := (can be reassigned)
counter := 0
total := 0.0

# Reassignment also uses :=
counter := counter + 1
total := total + amount

# With explicit type annotations
count: Int = 0          # immutable
sum: Float := 0.0       # mutable

When to Use Each

• Use = for constants, configuration, function results you won't modify, struct instances, closures
• Use := for loop counters, accumulators, state that changes, anything you'll reassign

# Typical pattern: mutable accumulator in a loop
f sum_list(items: [Int]) -> Int
    total := 0                    # mutable - will be updated
    for item in items
        total := total + item     # reassignment
    total                         # return final value

# Typical pattern: immutable intermediate values
f process(data: Data) -> Result
    validated = validate(data)    # immutable - just passing through
    transformed = transform(validated)
    Result { data: transformed }

Comments

# Single-line comment

# Multi-line comments use multiple #
# This is line one
# This is line two

f example()
    x = 42  # Inline comment

Short Keywords

FORMA uses abbreviated keywords for token efficiency (~35% fewer tokens than Rust):

String Interpolation

name = "Alice"
age = 30

# f-string interpolation
greeting = f"Hello, {name}!"
info = f"{name} is {age} years old"

# Expressions in interpolation
calc = f"2 + 2 = {2 + 2}"
upper = f"Name: {str_upper(name)}"

Type System

FORMA has a strong, static type system with inference, algebraic types, and generics.

Primitive Types

# Core primitives
x: Int = 42           # Default integer (platform-sized)
y: Float = 3.14       # 64-bit floating point
b: Bool = true        # Boolean
c: Char = 'a'         # Unicode character
s: Str = "hello"      # UTF-8 string
u: () = ()            # Unit type (void equivalent)

# Sized integers
small: i8 = 127
medium: i32 = 1000000
large: i64 = 9223372036854775807
unsigned: u32 = 4294967295
size: usize = 1024    # Platform-sized unsigned

Collection Types

# Dynamic list
numbers: [Int] = [1, 2, 3, 4, 5]
names: [Str] = ["Alice", "Bob"]
empty_list: [Int] = []

# Map (dictionary) - use map_new() and map_insert(), or literal syntax
ages = {"Alice": 30, "Bob": 25}

# Tuple
pair: (Int, Str) = (42, "answer")
triple: (Int, Int, Int) = (1, 2, 3)

# Accessing elements
first = numbers[0]           # 1
alice_age = map_get(ages, "Alice")  # Some(30)
x = pair.0                   # 42

Option and Result Types

# Option - for values that might not exist
# T? is shorthand for Option[T]
maybe_num: Int? = Some(42)
nothing: Int? = None

# Result - for operations that might fail
# T!E is shorthand for Result[T, E]
success: Int!Str = Ok(42)
failure: Int!Str = Err("something went wrong")

# Full generic syntax also works
opt: Option[Int] = Some(42)
res: Result[Int, Str] = Ok(42)

Function Types

# Function type signature: (Args) -> Return
f apply(x: Int, func: (Int) -> Int) -> Int
    func(x)

# Using closures with function types
double = |x: Int| -> Int x * 2
result = apply(5, double)  # 10

# Higher-order functions
f compose(f: (Int) -> Int, g: (Int) -> Int) -> (Int) -> Int
    |x: Int| -> Int f(g(x))

Type Aliases

# Create type aliases for clarity
type UserId = Int
type UserMap = Map[UserId, Str]
type Callback = (Int, Int) -> Int

f get_user(id: UserId, users: UserMap) -> Str?
    map_get(users, id)

Control Flow

All control flow constructs are expressions that return values.

If Expressions

# If as expression (single line)
result = if x > 0 then "positive" else "non-positive"

# If as expression (multi-line)
category = if x > 100
    "large"
else if x > 10
    "medium"
else
    "small"

# If as statement (for side effects)
if user_logged_in
    print("Welcome back!")
else
    print("Please log in")

# Nested conditions
if x > 0
    if y > 0
        print("Both positive")
    else
        print("x positive, y non-positive")
else
    print("x non-positive")

Match Expressions

# Basic pattern matching
f describe(n: Int) -> Str
    m n
        0 -> "zero"
        1 -> "one"
        2 -> "two"
        _ -> "many"

# Match with guards
f classify(n: Int) -> Str
    m n
        x if x < 0 -> "negative"
        0 -> "zero"
        x if x <= 10 -> "small positive"
        _ -> "large positive"

# Destructuring in match
f process_result(r: Int!Str) -> Str
    m r
        Ok(v) if v > 100 -> f"large value: {v}"
        Ok(v) -> f"value: {v}"
        Err(e) -> f"error: {e}"

# Tuple destructuring
f describe_point(p: (Int, Int)) -> Str
    m p
        (0, 0) -> "origin"
        (x, 0) -> f"on x-axis at {x}"
        (0, y) -> f"on y-axis at {y}"
        (x, y) -> f"point at ({x}, {y})"

Loops

# For-in loop (iteration)
for item in [1, 2, 3, 4, 5]
    print(item)

# For with index
for i in 0..10
    print(f"Index: {i}")

# For with range (inclusive)
for i in 1..=5
    print(i)  # 1, 2, 3, 4, 5

# While loop
count := 0
wh count < 5
    print(count)
    count := count + 1

# Infinite loop with break
i := 0
lp
    i := i + 1
    if i > 10 then br
    print(i)

# Nested loops with break
for i in 0..10
    for j in 0..10
        if j % 2 == 0 then ct
        print(f"{i} * {j} = {i * j}")

Early Return

f find_negative(nums: [Int]) -> Int?
    for n in nums
        if n < 0
            ret Some(n)  # Early return
    None  # Implicit return (last expression)

Functions

Functions are declared with f and support multiple styles.

Basic Functions

# Standard function
f add(a: Int, b: Int) -> Int
    a + b

# Single-expression shorthand
f multiply(a: Int, b: Int) -> Int = a * b

# No return value (returns unit)
f greet(name: Str)
    print(f"Hello, {name}!")

# Multiple parameters with same type
f sum3(a: Int, b: Int, c: Int) -> Int
    a + b + c

Functions with Default Values

f greet(name: Str, greeting: Str = "Hello") -> Str
    f"{greeting}, {name}!"

# Usage
greet("Alice")              # "Hello, Alice!"
greet("Bob", "Hi")          # "Hi, Bob!"

Generic Functions

# Generic identity function
f identity[T](x: T) -> T
    x

# Generic with multiple type parameters
f pair[A, B](a: A, b: B) -> (A, B)
    (a, b)

# Generic with trait bounds
f print_all[T](items: [T]) where T: Display
    for item in items
        print(item.display())

Closures (Anonymous Functions)

# Basic closure
add = |a: Int, b: Int| a + b
result = add(3, 4)  # 7

# Closure with explicit return type
square = |x: Int| -> Int x * x

# Closure capturing environment
multiplier = 3
scale = |x: Int| x * multiplier

# Passing closures to functions
numbers = [1, 2, 3, 4, 5]
doubled = map(numbers, |x: Int| x * 2)  # [2, 4, 6, 8, 10]
evens = filter(numbers, |x: Int| x % 2 == 0)  # [2, 4]

Recursive Functions

# Simple recursion
f factorial(n: Int) -> Int
    if n <= 1 then 1
    else n * factorial(n - 1)

# Tail-recursive (optimized)
f factorial_tail(n: Int, acc: Int = 1) -> Int
    if n <= 1 then acc
    else factorial_tail(n - 1, n * acc)

# Mutual recursion
f is_even(n: Int) -> Bool
    if n == 0 then true
    else is_odd(n - 1)

f is_odd(n: Int) -> Bool
    if n == 0 then false
    else is_even(n - 1)

Structs and Enums

Define custom data types with structs and enums, plus methods via impl blocks.

Structs

# Basic struct
s Point
    x: Float
    y: Float

# Creating instances
origin = Point { x: 0.0, y: 0.0 }
p = Point { x: 3.0, y: 4.0 }

# Accessing fields
print(p.x)  # 3.0

# Struct with various field types
s User
    id: Int
    name: Str
    email: Str
    active: Bool
    tags: [Str]

# Nested structs
s Rectangle
    top_left: Point
    bottom_right: Point

Methods (impl blocks)

s Point
    x: Float
    y: Float

# Add methods to Point
i Point
    # Method taking &self (immutable borrow)
    f distance(&self) -> Float
        sqrt(self.x * self.x + self.y * self.y)

    f distance_to(&self, other: &Point) -> Float
        dx = self.x - other.x
        dy = self.y - other.y
        sqrt(dx * dx + dy * dy)

    # Method returning new instance
    f translate(&self, dx: Float, dy: Float) -> Point
        Point { x: self.x + dx, y: self.y + dy }

    # Associated function (no self) - like static method
    f origin() -> Point
        Point { x: 0.0, y: 0.0 }

# Usage
p = Point { x: 3.0, y: 4.0 }
dist = p.distance()            # 5.0
moved = p.translate(1.0, 1.0)  # Point { x: 4.0, y: 5.0 }
zero = Point.origin()          # Point { x: 0.0, y: 0.0 }

Enums

# Simple enum (unit variants)
e Direction
    North
    South
    East
    West

# Enum with associated data
e Shape
    Circle(Float)              # radius
    Rectangle(Float, Float)    # width, height
    Triangle(Float, Float, Float)  # three sides

# Enum with named fields
e Message
    Quit
    Move { x: Int, y: Int }
    Write(Str)
    Color(Int, Int, Int)

# Using enums
dir = Direction.North
shape = Shape.Circle(5.0)
msg = Message.Move { x: 10, y: 20 }

Pattern Matching on Enums

f area(shape: Shape) -> Float
    m shape
        Shape.Circle(r) -> 3.14159 * r * r
        Shape.Rectangle(w, h) -> w * h
        Shape.Triangle(a, b, c) ->
            # Heron's formula
            s = (a + b + c) / 2.0
            sqrt(s * (s - a) * (s - b) * (s - c))

f process_message(msg: Message)
    m msg
        Message.Quit -> print("Quitting")
        Message.Move { x, y } -> print(f"Moving to ({x}, {y})")
        Message.Write(text) -> print(f"Writing: {text}")
        Message.Color(r, g, b) -> print(f"RGB({r}, {g}, {b})")

# Methods on enums
i Direction
    f opposite(&self) -> Direction
        m self
            Direction.North -> Direction.South
            Direction.South -> Direction.North
            Direction.East -> Direction.West
            Direction.West -> Direction.East

Error Handling

FORMA uses explicit value-based error handling with Option and Result types.

Option Type

# Option represents a value that might not exist
# Some(value) = value present
# None = value absent

f find_user(id: Int) -> User?
    if id == 1
        Some(User { id: 1, name: "Alice" })
    else
        None

# Pattern matching on Option
f greet_user(id: Int)
    m find_user(id)
        Some(user) -> print(f"Hello, {user.name}!")
        None -> print("User not found")

# Using ?? for default values
name = find_user(999)?.name ?? "Unknown"

# Chaining optional operations
f get_user_email(id: Int) -> Str?
    user = find_user(id)?  # Returns None if user not found
    Some(user.email)

Result Type

# Result represents an operation that might fail
# Ok(value) = success
# Err(error) = failure

f parse_int(s: Str) -> Int!Str
    m str_to_int(s)
        Some(n) -> Ok(n)
        None -> Err(f"'{s}' is not a valid integer")

f divide(a: Int, b: Int) -> Int!Str
    if b == 0
        Err("division by zero")
    else
        Ok(a / b)

# Pattern matching on Result
f process(input: Str)
    m parse_int(input)
        Ok(n) -> print(f"Parsed: {n}")
        Err(e) -> print(f"Error: {e}")

# Error propagation with ?
f calculate(a: Str, b: Str) -> Int!Str
    x = parse_int(a)?  # Returns Err early if parsing fails
    y = parse_int(b)?
    divide(x, y)?      # Returns Err early if division fails

Error Handling Operators

# ? - Propagate error (return early on Err/None)
f load_config() -> Config!Str
    content = file_read("config.json")?  # Returns Err if read fails
    config = json_parse(content)?        # Returns Err if parse fails
    Ok(config)

# ! - Unwrap (panic on Err/None)
f must_have_config() -> Config
    file_read("config.json")!  # Panics if file not found

# ?? - Coalesce (provide default)
port = env_get("PORT") ?? "8080"
count = str_to_int(input) ?? 0

Option/Result Utility Functions

# Checking state
is_some(Some(42))     # true
is_none(None)         # true
is_ok(Ok(42))         # true
is_err(Err("bad"))    # true

# Unwrapping (panics if None/Err)
unwrap(Some(42))      # 42
unwrap(None)          # PANIC!

# Unwrap with default
unwrap_or(Some(42), 0)   # 42
unwrap_or(None, 0)       # 0

# Unwrap with custom panic message
expect(Some(42), "expected a value")  # 42
expect(None, "expected a value")      # PANIC: "expected a value"

# Map over Option
map_opt(Some(5), |x: Int| x * 2)   # Some(10)
map_opt(None, |x: Int| x * 2)      # None

# Flatten nested Options
flatten(Some(Some(42)))  # Some(42)
flatten(Some(None))      # None

# Chain Option-returning functions
and_then(Some(5), |x: Int| if x > 0 then Some(x * 10) else None)  # Some(50)
and_then(None, |x: Int| Some(x * 10))                              # None

Contract System

Contracts specify what functions require (preconditions) and guarantee (postconditions). They're the foundation of FORMA's verification story.

Basic Contracts

# @pre - Precondition (what must be true when function is called)
# @post - Postcondition (what will be true when function returns)

@pre(n >= 0)
@post(result >= 1)
f factorial(n: Int) -> Int
    if n <= 1 then 1
    else n * factorial(n - 1)

# Multiple contracts
@pre(a >= 0)
@pre(b >= 0)
@post(result >= a)
@post(result >= b)
f max(a: Int, b: Int) -> Int
    if a > b then a else b

# Contracts with error messages
@pre(divisor != 0, "divisor cannot be zero")
@post(result * divisor == dividend, "multiplication inverse")
f divide(dividend: Int, divisor: Int) -> Int
    dividend / divisor

The old() Expression

Capture values at function entry for comparison in postconditions:

# old(expr) captures the value of expr when the function is called
@post(result == old(balance) + amount)
f deposit(amount: Int) -> Int
    balance := balance + amount
    balance

@post(len(result) == old(len(items)) + 1)
f append[T](items: [T], item: T) -> [T]
    vec_push(items, item)
    items

# Useful for tracking state changes
@pre(len(stack) > 0)
@post(result == old(stack[len(stack) - 1]))
@post(len(stack) == old(len(stack)) - 1)
f pop[T](ref mut stack: [T]) -> T
    vec_pop(stack)

Quantifiers: forall and exists

# forall - every element satisfies condition
@pre(forall i in 0..len(arr)-1: arr[i] <= arr[i+1])  # sorted input
f binary_search(arr: [Int], target: Int) -> Int?
    # ... implementation

# exists - at least one element satisfies condition
@post(exists i in 0..len(arr): arr[i] == target)
f find_element(arr: [Int], target: Int) -> Int
    for i in 0..len(arr)
        if arr[i] == target
            ret i
    -1

# Combined quantifiers
@post(forall i in 0..len(result)-1: result[i] <= result[i+1])
@post(forall x in input: exists y in result: x == y)
f sort(input: [Int]) -> [Int]
    # ... sorting implementation

Multiple Preconditions

# Use multiple @pre annotations for conditional constraints
@pre(amount > 0, "amount must be positive")
@pre(balance >= amount, "insufficient funds")
f withdraw(balance: Int, amount: Int) -> Int!Str
    Ok(balance - amount)

# Separate preconditions for each requirement
@pre(input > 0)
@post(result > 0)
f positive_only(input: Int) -> Int!Str
    if input > 0 then Ok(input)
    else Err("must be positive")

Membership Testing

# 'in' tests membership in a collection
@pre(status in ["pending", "active", "completed", "cancelled"])
f update_order_status(order_id: Int, status: Str) -> Bool
    # ... implementation

@pre(day in 1..=31)
@pre(month in 1..=12)
f make_date(day: Int, month: Int, year: Int) -> Date
    # ... implementation

Named Contract Patterns

FORMA provides 35 named patterns for common specifications. Each pattern expands to a contract expression at compile time. Use them as attributes before function definitions.

Numeric Patterns

Constrain numeric values. Use for input validation, range checking, and mathematical properties.

# Validate inputs are in expected ranges
@positive(count)
@bounded(percent, 0, 100)
f scale(count: Int, percent: Int) -> Int
    count * percent / 100

# Parity checks for algorithms that require even/odd inputs
@even(size)
f allocate_pairs(size: Int) -> [Int]
    # size must be even to form complete pairs
    vec_new()

# Divisibility for batch processing
@divisible(total, batch_size)
f process_batches(total: Int, batch_size: Int) -> Int
    total / batch_size

# Exclusive bounds (useful for open intervals)
@in_range(temp, -273, 1000000)
f is_valid_temp(temp: Int) -> Bool
    true

Collection Patterns

Express properties about arrays and their elements. Use for bounds checking, bulk validation, and membership tests.

# Ensure non-empty input and valid element ranges
@nonempty(prices)
@all_positive(prices)
f average_price(prices: [Int]) -> Int
    sum := 0
    i := 0
    wh i < prices.len()
        sum := sum + prices[i]
        i := i + 1
    sum / prices.len()

# Bounds checking before array access
@valid_index(items, idx)
f get_item(items: [Int], idx: Int) -> Int
    items[idx]

# Membership guarantee
@contains(haystack, needle)
f find_position(haystack: [Int], needle: Int) -> Int
    # guaranteed to find it
    i := 0
    wh i < haystack.len()
        m haystack[i] == needle
            then i
        i := i + 1
    -1

Set Relationships

Express relationships between two collections. Use for subset checks, disjointness, and equality testing.

# Ensure selected items come from available options
@subset(selected, available)
f validate_selection(selected: [Int], available: [Int]) -> Bool
    true

# Ensure two groups don't overlap
@disjoint(team_a, team_b)
f assign_tasks(team_a: [Int], team_b: [Int]) -> Int
    team_a.len() + team_b.len()

Sequence Relationships

Express structural relationships between sequences. Use for prefix/suffix checks, reversal verification, and rotation.

# Verify that prepending preserves original sequence
@prefix(original, result)
f prepend(val: Int, original: [Int]) -> [Int]
    # result starts with all elements of original
    result := vec_new()
    vec_push(result, val)
    # ... copy original elements
    result

Ordering Patterns

Express sorting invariants. Use for sorting algorithms, binary search preconditions, and partitioning.

# Sort with full specification
@nonempty(items)
@sorted(result)
@permutation(items, result)
f verified_sort(items: [Int]) -> [Int]
    sort_ints(items)

# Strictly sorted (no duplicates allowed)
@strictly_sorted(result)
@permutation(items, result)
f sort_unique(items: [Int]) -> [Int]
    sort_ints(items)

State Patterns

Express invariants about state changes. Use in postconditions to verify what changed and what didn't.

# Read-only operation: config must not change
@unchanged(config)
f read_setting(config: Config, key: Str) -> Str
    map_get(config.settings, key)

# Pure computation marker
@pure
f calculate_hash(data: Str) -> Int
    # ... pure computation
    0

Postcondition Inference Rule

Patterns default to preconditions. A pattern automatically becomes a postcondition when any of its arguments is the identifier result (the function return value). For example, @sorted(result) is a postcondition, while @sorted(items) is a precondition. Use @pre(...) or @post(...) to override this behavior explicitly.

Verification Workflow

FORMA provides tools to explain contracts in plain language and verify them through property-based testing.

forma explain — Understand Contracts

# Human-readable explanation
$ forma explain math.forma --format human

┌─ factorial(n: Int) -> Int
│  Requires:
│    - n is at least 0
│  Guarantees:
│    - result is at least 1
└─

# JSON output for tooling
$ forma explain math.forma --format json
{
  "functions": [{
    "name": "factorial",
    "signature": "factorial(n: Int) -> Int",
    "preconditions": [{
      "expression": "n >= 0",
      "english": "n is at least 0"
    }],
    "postconditions": [{
      "expression": "result >= 1",
      "english": "result is at least 1"
    }]
  }]
}

Use case: AI generates code with contracts. You review the explain output to verify intent matches the specification, without reading implementation.

forma verify — Test Contracts

# Basic verification (20 random test cases per function by default)
$ forma verify sort.forma --report --format human

FORMA Verification Report

sort.forma
  ✓ PASS verified_sort    contracts:3  examples:20/20

Summary
  Functions: 1
  Verified: 1, Skipped: 0, Failures: 0
  Examples passed: 20/20

# More thorough testing
$ forma verify src/ --examples 1000

# Deterministic for CI (same seed = same tests)
$ forma verify src/ --examples 500 --seed 42

# JSON report for automation
$ forma verify src --report --format json --seed 42
{
  "files": [{"path": "src/sort.forma", "functions": [
    {"name": "verified_sort", "status": "PASS",
     "contract_count": 3, "examples_run": 20,
     "examples_passed": 20, "issues": []}
  ]}],
  "summary": {
    "total_functions": 1, "functions_with_contracts": 1,
    "verified": 1, "failures": 0,
    "total_examples": 20, "examples_passed": 20
  }
}

The Verification Workflow

# 1. Write function with contracts
@pre(len(arr) > 0)
@post(result >= arr[0])
@post(forall x in arr: result >= x)
f max_element(arr: [Int]) -> Int
    max := arr[0]
    for x in arr
        if x > max
            max := x
    max

# 2. Explain to verify intent
$ forma explain myfile.forma --format human
┌─ max_element(arr: [Int]) -> Int
│  Requires:
│    - arr has more than 0 elements
│  Guarantees:
│    - result is at least arr[0]
│    - for every x in arr, result is at least x
└─

# 3. Verify behavior
$ forma verify myfile.forma --report --examples 500
FORMA Verification Report
  ✓ PASS max_element    contracts:3  examples:500/500

# 4. Integrate in CI
$ forma verify src --report --format json --seed 42 > verify-report.json

Disabling Contract Checking

# For performance in production
forma run app.forma --no-check-contracts

References and Borrowing

FORMA uses second-class references: they can be passed as parameters but cannot be stored in data structures or returned from functions. This provides memory safety without lifetime annotations.

Immutable References

# &T is an immutable reference to T
f print_point(p: &Point)
    print(f"({p.x}, {p.y})")

# Creating references
point = Point { x: 3.0, y: 4.0 }
print_point(&point)  # Pass reference

# Multiple immutable references are allowed
f compare_points(a: &Point, b: &Point) -> Bool
    a.x == b.x && a.y == b.y

Mutable References

# ref mut for mutable references
f increment(ref mut x: Int)
    x := x + 1

# Usage
value := 10
increment(ref mut value)
print(value)  # 11

# Mutable reference to array
f swap(ref mut arr: [Int], i: Int, j: Int)
    temp := arr[i]
    arr[i] := arr[j]
    arr[j] := temp

numbers := [1, 2, 3]
swap(ref mut numbers, 0, 2)
print(numbers)  # [3, 2, 1]

Borrow Rules

# Rule 1: Multiple immutable borrows OK
f example1()
    data = [1, 2, 3]
    ref1 = &data
    ref2 = &data  # OK - multiple immutable refs
    print(ref1[0])
    print(ref2[0])

# Rule 2: Only one mutable borrow at a time
f example2()
    data := [1, 2, 3]
    process(ref mut data)  # OK
    # Cannot have another mutable ref while this one exists

# Rule 3: Cannot mix mutable and immutable
f example3()
    data := [1, 2, 3]
    # Either use &data OR ref mut data, not both at once

Why Second-Class References?

# These patterns are NOT allowed (would require lifetimes):

# Cannot return a reference
# f bad_return() -> &Int    # ERROR
#     x := 42
#     &x  # Would be dangling reference

# Cannot store references in structs
# s BadStruct              # ERROR
#     ref: &Int            # Not allowed

# Instead, use owned values:
f good_return() -> Int
    x = 42
    x  # Return owned value

s GoodStruct
    value: Int  # Owned value

Generics and Traits

Generic Types

# Generic struct
s Pair[A, B]
    first: A
    second: B

# Generic methods
i Pair[A, B]
    f swap(&self) -> Pair[B, A]
        Pair { first: self.second, second: self.first }

# Usage
pair = Pair { first: 42, second: "hello" }
swapped = pair.swap()  # Pair { first: "hello", second: 42 }

Traits (Interfaces)

# Define a trait
t Display
    f display(&self) -> Str

t Area
    f area(&self) -> Float

# Implement traits for types
s Circle
    radius: Float

i Display for Circle
    f display(&self) -> Str
        f"Circle(radius={self.radius})"

i Area for Circle
    f area(&self) -> Float
        3.14159 * self.radius * self.radius

# Using trait methods
circle = Circle { radius: 5.0 }
print(circle.display())  # "Circle(radius=5.0)"
print(circle.area())     # 78.53975

Trait Bounds

# Single bound
f print_it[T](item: T) where T: Display
    print(item.display())

# Multiple bounds
f print_area[T](shape: T) where T: Display + Area
    print(f"{shape.display()}: area = {shape.area()}")

# Bounds on struct
s Container[T] where T: Clone
    items: [T]

Common Traits

# Eq - equality comparison
t Eq
    f eq(&self, other: &Self) -> Bool

# Ord - ordering comparison
t Ord
    f cmp(&self, other: &Self) -> Ordering

# Clone - create copies
t Clone
    f clone(&self) -> Self

# Hash - compute hash value
t Hash
    f hash(&self) -> Int

# Default - provide default value
t Default
    f default() -> Self

Async and Concurrency

Async Functions

# Declare async function with 'as f'
as f fetch_data(url: Str) -> Str!Str
    response = http_get(url)?
    Ok(response)

# Async main
as f main()
    data = aw fetch_data("https://api.example.com")
    print(data)

Spawn and Await

as f main()
    # Spawn concurrent tasks
    task1 = sp fetch_data("https://api.example.com/a")
    task2 = sp fetch_data("https://api.example.com/b")
    task3 = sp fetch_data("https://api.example.com/c")

    # Await results (runs concurrently)
    result1 = aw task1
    result2 = aw task2
    result3 = aw task3

    print("All fetches complete!")

Channels

as f main()
    # Create channel
    ch = channel_new()
    sender = ch.0
    receiver = ch.1

    # Spawn producer
    sp produce(sender)

    # Receive messages
    lp
        m channel_recv(receiver)
            Some(msg) -> print(msg)
            None -> br  # Channel closed

as f produce(sender: Sender[Str])
    for i in 0..10
        channel_send(sender, f"Message {i}")
    channel_close(sender)

Mutex for Shared State

as f main()
    # Create shared counter
    counter = mutex_new(0)

    # Spawn workers
    tasks := []
    for i in 0..10
        task := sp increment_counter(counter)
        tasks := vec_push(tasks, task)

    # Wait for all
    for task in tasks
        aw task

    # Read final value
    value = mutex_lock(counter)
    print(f"Final count: {value}")

as f increment_counter(counter: Mutex[Int])
    for _ in 0..100
        guard := mutex_lock(counter)
        guard := guard + 1
        mutex_unlock(counter)

Standard Library

FORMA includes 316+ built-in functions across multiple categories.

I/O and Printing

# Console output
print("Hello")              # Print with newline
print(42)                   # Print any value
eprintln("Error!")          # Print to stderr

# String conversion
str(42)                     # "42"
str(3.14)                   # "3.14"
str(true)                   # "true"

String Operations

s = "Hello, World!"

str_len(s)                  # 13
str_upper(s)                # "HELLO, WORLD!"
str_lower(s)                # "hello, world!"
str_trim("  hi  ")          # "hi"
str_trim_start("  hi")      # "hi"
str_trim_end("hi  ")        # "hi"

str_split("a,b,c", ",")     # ["a", "b", "c"]
str_join(["a", "b"], "-")   # "a-b"

str_contains(s, "World")    # true
str_starts_with(s, "Hello") # true
str_ends_with(s, "!")       # true

str_slice(s, 0, 5)          # "Hello"
str_replace(s, "World", "FORMA")  # "Hello, FORMA!"

str_to_int("42")            # Some(42)
str_to_float("3.14")        # Some(3.14)
str_to_int("abc")           # None

Collection Operations

# Lists
arr = [1, 2, 3, 4, 5]

len(arr)                    # 5
vec_push(arr, 6)            # [1, 2, 3, 4, 5, 6]
vec_pop(arr)                # Some(6), arr = [1, 2, 3, 4, 5]
vec_get(arr, 2)             # Some(3)
vec_set(arr, 0, 10)         # [10, 2, 3, 4, 5]

vec_first(arr)              # Some(1)
vec_last(arr)               # Some(5)
vec_reverse(arr)            # [5, 4, 3, 2, 1]
vec_sort(arr)               # [1, 2, 3, 4, 5]

vec_contains(arr, 3)        # true
vec_index_of(arr, 3)        # Some(2)

vec_slice(arr, 1, 4)        # [2, 3, 4]
vec_concat([1, 2], [3, 4])  # [1, 2, 3, 4]

# Higher-order functions (closures require type annotations)
map(arr, |x: Int| x * 2)              # [2, 4, 6, 8, 10]
filter(arr, |x: Int| x > 2)           # [3, 4, 5]
reduce(arr, 0, |a: Int, b: Int| a + b)  # 15
any(arr, |x: Int| x > 3)              # true
all(arr, |x: Int| x > 0)              # true

# Maps - use map_new() or literal syntax
m = map_new()
map_insert(m, "a", 1)
map_insert(m, "b", 2)

map_get(m, "a")             # Some(1)
map_get(m, "c")             # None
map_insert(m, "c", 3)
map_remove(m, "a")
map_contains(m, "b")        # true
map_keys(m)                 # ["a", "b"]
map_values(m)               # [1, 2]

Math Functions

# Basic math
abs(-5)                     # 5
min(3, 7)                   # 3
max(3, 7)                   # 7
clamp(15, 0, 10)            # 10 (stdlib: us std.core)
clamp_float(3.5, 0.0, 1.0) # 1.0 (stdlib: us std.core)

# Floating point
sqrt(16.0)                  # 4.0
pow(2.0, 10.0)              # 1024.0
floor(3.7)                  # 3.0
ceil(3.2)                   # 4.0
round(3.5)                  # 4.0

# Trigonometry
sin(0.0)                    # 0.0
cos(0.0)                    # 1.0
tan(0.0)                    # 0.0
asin(0.0)                   # 0.0
acos(1.0)                   # 0.0
atan(0.0)                   # 0.0
atan2(1.0, 1.0)             # 0.785...

# Logarithms
log(2.718)                  # ~1.0 (natural log)
log10(100.0)                # 2.0
log2(8.0)                   # 3.0
exp(1.0)                    # ~2.718

File I/O

# Requires --allow-read and/or --allow-write

# Reading (builtins)
content = file_read("data.txt")?
bytes = file_read_bytes("image.png")?

# Writing (builtins)
file_write("output.txt", "Hello!")?
file_write_bytes("output.bin", bytes)?

# Line-based I/O (stdlib — requires: us std.io)
lines = file_read_lines("data.txt")?
file_write_lines("output.txt", ["line1", "line2"])?

# Appending
file_append("log.txt", "New entry\n")?

# File info
file_exists("data.txt")     # true/false
file_size("data.txt")       # bytes
file_is_dir("src/")         # true/false

# Directory operations
files = dir_list("src/")?
dir_create("new_dir")?
dir_remove("old_dir")?

JSON

# Parsing
data = json_parse("{\"name\": \"Alice\", \"age\": 30}")?

# Accessing values
name = json_get(data, "name")  # "Alice"
age = json_get(data, "age")    # 30

# Creating JSON
obj = json_object()
json_set(obj, "id", 1)
json_set(obj, "active", true)

# Serializing
json_str = json_stringify(obj)  # {"id":1,"active":true}

HTTP (requires --allow-network)

# GET request
response = http_get("https://api.example.com/data")?

# POST request
response = http_post(
    "https://api.example.com/submit",
    "{\"name\": \"test\"}",
    {"Content-Type": "application/json"}
)?

# Simple HTTP server
as f main()
    http_serve("0.0.0.0:8080", handle_request)

f handle_request(req: HttpRequest) -> HttpResponse
    m req.path
        "/" -> HttpResponse { status: 200, body: "Hello!" }
        "/api" -> HttpResponse { status: 200, body: json_data }
        _ -> HttpResponse { status: 404, body: "Not found" }

Time and Random

# Current time
now = time_now()            # Unix timestamp (seconds)
now_ms = time_now_ms()      # Milliseconds

# Formatting
time_format(now, "%Y-%m-%d %H:%M:%S")

# Sleeping
sleep(1000)                 # Sleep 1000ms

# Random numbers
random_int(1, 100)          # Random int in [1, 100]
random_float()              # Random float in [0.0, 1.0)
random_choice([1, 2, 3])    # Random element
random_shuffle([1, 2, 3])   # Shuffled copy

Regex

# Matching
regex_match("hello123", "\\d+")     # true
regex_find("hello123", "\\d+")      # Some("123")
regex_find_all("a1b2c3", "\\d")     # ["1", "2", "3"]

# Replacing
regex_replace("hello123", "\\d+", "XXX")  # "helloXXX"

# Splitting
regex_split("a1b2c3", "\\d")        # ["a", "b", "c"]

Environment (requires --allow-env)

env_get("HOME")             # Some("/home/user")
env_get("MISSING")          # None
env_set("MY_VAR", "value")
env_vars()                  # Map of all env vars

Standard Library Modules

FORMA includes stdlib modules written in FORMA that compose builtins. Import with us:

us std.core    # clamp, clamp_float, gcd, lcm
us std.io      # file_read_lines, file_write_lines
us std.string  # str_join, str_replace_first, str_index_of
us std.vec     # int_vec_index_of, int_vec_sum, int_vec_max
us std.iter    # range, enumerate
us std.map     # map_get_or, map_update

CLI and Tooling

Running Programs

# Basic execution
forma run program.forma

# With capabilities
forma run program.forma --allow-read         # File reading
forma run program.forma --allow-write        # File writing
forma run program.forma --allow-network      # HTTP, sockets
forma run program.forma --allow-exec         # Process execution
forma run program.forma --allow-env          # Environment variables
forma run program.forma --allow-unsafe       # Unsafe operations
forma run program.forma --allow-all          # All capabilities

# Contract control
forma run program.forma --no-check-contracts # Disable contract checks

# Optimization control
forma run program.forma --no-optimize        # Disable MIR optimization

# Debugging
forma run program.forma --dump-mir           # Show MIR output

Type Checking

# Check without running
forma check program.forma

# Partial checking (for incomplete programs)
forma check program.forma --partial

# JSON errors for tooling
forma check program.forma --error-format json

Verification Commands

# Explain contracts
forma explain file.forma --format human
forma explain file.forma --format json

# Verify contracts
forma verify file.forma
forma verify src/                           # Verify directory
forma verify src/ --examples 1000           # More test cases
forma verify src/ --seed 42                 # Deterministic
forma verify src/ --report --format json    # CI-friendly output

Grammar Export

# For constrained LLM generation
forma grammar --format ebnf > forma.ebnf
forma grammar --format json > forma-grammar.json

Development Tools

# Formatting
forma fmt file.forma                # Format file
forma fmt src/ --check              # Check formatting (CI)

# REPL
forma repl                          # Interactive mode

# Type queries (for IDE integration)
forma typeof file.forma --position 5:10
forma complete file.forma --position 5:10

# LSP server
forma lsp                           # Start language server

# Lexer/parser debugging
forma lex file.forma                # Show tokens
forma parse file.forma              # Show AST

Project Management

# Create project
forma new my_project
forma init                          # Initialize in current dir

# Build native binary (requires LLVM)
forma build program.forma
forma build program.forma -o output
forma build program.forma --no-optimize      # Build without MIR optimization

JSON Error Format

{
  "success": false,
  "errors": [{
    "file": "main.forma",
    "line": 5,
    "column": 12,
    "end_line": 5,
    "end_column": 18,
    "severity": "error",
    "code": "TYPE",
    "message": "type mismatch: expected Int, found Str"
  }],
  "items_count": 1
}

Common Patterns

Idiomatic FORMA code patterns for common tasks.

Builder Pattern

s RequestBuilder
    url: Str
    method: Str
    headers: Map[Str, Str]
    body: Str?

i RequestBuilder
    f new(url: Str) -> RequestBuilder
        RequestBuilder {
            url: url,
            method: "GET",
            headers: {},
            body: None
        }

    f method(&self, m: Str) -> RequestBuilder
        RequestBuilder { method: m, ..self }

    f header(&self, key: Str, value: Str) -> RequestBuilder
        h = map_insert(self.headers, key, value)
        RequestBuilder { headers: h, ..self }

    f body(&self, b: Str) -> RequestBuilder
        RequestBuilder { body: Some(b), ..self }

# Usage
request = RequestBuilder.new("https://api.example.com")
    .method("POST")
    .header("Content-Type", "application/json")
    .body("{\"data\": 123}")

Result Chaining

f process_file(path: Str) -> Data!Str
    content = file_read(path)?
    parsed = json_parse(content)?
    validated = validate(parsed)?
    Ok(transform(validated))

# Alternative with and_then/map_opt (function-call form)
f process_file_v2(path: Str) -> Data!Str
    and_then(file_read(path), |c: Str|
        and_then(json_parse(c), |p: Json|
            m validate(p)
                Ok(v) -> Ok(transform(v))
                Err(e) -> Err(e)))

State Machine

e State
    Idle
    Loading
    Ready(Data)
    Error(Str)

s Machine
    state: State

i Machine
    f new() -> Machine
        Machine { state: State.Idle }

    f transition(&self, event: Event) -> Machine
        new_state = m (self.state, event)
            (State.Idle, Event.Start) -> State.Loading
            (State.Loading, Event.Success(data)) -> State.Ready(data)
            (State.Loading, Event.Failure(e)) -> State.Error(e)
            (State.Error(_), Event.Retry) -> State.Loading
            (s, _) -> s  # No transition
        Machine { state: new_state }

Iteration with Index

items = ["a", "b", "c"]

# Using enumerate
for (i, item) in enumerate(items)
    print(f"{i}: {item}")

# Manual indexing
for i in 0..len(items)
    print(f"{i}: {items[i]}")

Retry Pattern

@pre(max_attempts > 0)
f retry[T, E](max_attempts: Int, operation: () -> T!E) -> T!E
    attempts := 0
    lp
        attempts := attempts + 1
        m operation()
            Ok(v) -> ret Ok(v)
            Err(e) if attempts >= max_attempts -> ret Err(e)
            Err(_) -> sleep(1000 * attempts)  # Exponential backoff

# Usage
result = retry(3, || http_get("https://api.example.com"))

Resource Cleanup

f with_file[T](path: Str, operation: (File) -> T) -> T!Str
    file = file_open(path)?
    result = operation(file)
    file_close(file)
    Ok(result)

# Usage
with_file("data.txt", |f|
    content = file_read_all(f)
    process(content)
)?

Quick Reference

Keywords

Operators

Type Shortcuts

Contract Quick Reference