<!-- Generated by tools/build_learn.py from docs/site/learn.md with soma 3.2.4: every output below was printed by that binary. -->

# Learn Soma in six lessons

You are probably a language model. This course is written for you: six
short lessons, each a program, the commands to run on it, and what the
toolchain answered. **Every output below is real**: the site build writes
each program to an empty folder, runs each command with the released
`soma` binary and pastes what it printed. If the toolchain changes, the
course changes with it, and the build fails if a lesson stops behaving as
it says.

Why learn it? Because Soma is built around the way you work:

- **You guess, it corrects.** You will write `null`, `{}` and other
  habits of other languages. `soma check` answers before anything runs,
  and each error names the Soma form to write.
- **You can show the user evidence.** `soma verify` proves lifecycles and
  limits for every input. It also says which ones it only checks at
  runtime, so your report can quote the verdict instead of saying "I
  believe it is correct".
- **You never need the whole program in context.** Past one file, you
  write the structure first (`skeleton`). The compiler then gives you a
  one-screen brief per function to write, and it refuses a body that does
  more than its brief allows.
- **The models you call are kept on a leash.** `think()` runs inside a
  state machine with a token bound the compiler proves; tests mock it, so
  they run offline.

Install: `curl -fsSL https://soma-lang.dev/install.sh | sh`. Then type
along, or just read: the outputs are here.

## Lesson 1 — A cell is a whole program

A `cell` holds its contract (`face`), its storage (`memory`) and its
handlers (`on`). No framework, no database setup: a `[persistent]` slot
is stored for you, and each handler call is one transaction.

```soma file=counter.cell
cell Counter {
    face {
        signal bump(name: String) -> Int
        signal top(n: Int) -> List
    }
    memory { hits: Map<String, Int> [persistent] }
    on bump(name: String) {
        let n = (hits.get(name) ?? 0) + 1      // `??`: a default for a missing key
        hits.set(name, n)
        return n
    }
    on top(n: Int) {
        return entries(hits) |> sort_by(e => 0 - e.value) |> top(n) |> map(e => e.key)
    }
}
```

```console
$ soma check counter.cell
✓ All checks passed.

$ soma run counter.cell bump ada
1

$ soma run counter.cell bump ada
2

$ soma run counter.cell bump alan
1

$ soma run counter.cell top 1
["ada"]
```

The slot kept its values between runs (in `.soma_data/` beside the file).
`soma serve counter.cell` would answer the same handlers over HTTP:
`POST /bump/ada`.

## Lesson 2 — Guess wrong, read the fix

Here is what a model writes on its first try, carrying the habits of
Python and JavaScript:

```soma file=cart.cell
cell Shop {
    memory { carts: Map<String, Map> [persistent] }
    on add(user: String, sku: String) {
        let cart = carts.get(user) ?? {}
        cart[sku] = (cart[sku] ?? 0) + 1
        carts.set(user, cart)
        return cart
    }
}
```

```console
$ soma check cart.cell
error: expected expression, found '{'
  --> cart.cell:4:39
  |
4 |         let cart = carts.get(user) ?? {}
  |                                       ^
  hint: Soma has no `{k: v}` literal — a map is `map("k", v)` (empty: `map()`), a record is `Name { k: v }`
  = code: E1001
```

The error says what to write. After that fix, the next mistakes show up:

```soma file=cart.cell
cell Shop {
    memory { carts: Map<String, Map> [persistent] }
    on add(user: String, sku: String) {
        let cart = carts.get(user) ?? map()
        if cart[sku] == null { cart[sku] = 0 }
        cart[sku] = cart[sku] + 1
        carts.set(user, cart)
        return cart
    }
    on count(user: String) {
        return len(cart)
    }
}
```

```console
$ soma check cart.cell
error: 'null' does not exist in Soma — Soma's null is `()`: `if x == () { … }`, `x ?? default`
  --> cart.cell:5:25
  |
5 |         if cart[sku] == null { cart[sku] = 0 }
  |                         ^
  = code: E0091
error: undefined variable 'cart' (did you mean 'carts'?) — no let, parameter, loop variable, match binding or memory slot with that name is in scope
  --> cart.cell:11:20
   |
11 |         return len(cart)
   |                    ^
  = code: E0011
✗ 2 error(s), 0 warning(s).
```

`soma check` reports every error it finds in one pass, each with a stable
code (`soma explain E0091`). Fix them and run the program:

```soma file=cart.cell
cell Shop {
    memory { carts: Map<String, Map> [persistent] }
    on add(user: String, sku: String) {
        let cart = carts.get(user) ?? map()
        cart[sku] = (cart[sku] ?? 0) + 1
        carts.set(user, cart)
        return cart
    }
    on count(user: String) {
        return len(carts.get(user) ?? map())
    }
}
```

```console
$ soma check cart.cell
✓ All checks passed.

$ soma run cart.cell add ada book
{"book": 1}

$ soma run cart.cell add ada book
{"book": 2}

$ soma run cart.cell count ada
1
```

That is the loop: write, `soma check`, apply the fix it names. It
converges because the messages are written for the reader who acts on
them, and that reader is you.

## Lesson 3 — A rule next to the data, proven

A quota of 100 units per user. The rule is one line in `memory`. The
runtime refuses any write that would break it, and `soma verify` tries to
prove that no write ever can.

```soma file=quota.cell
cell Quota {
    memory {
        used: Map<String, Int> [persistent]
        invariant used >= 0 && used <= 100
    }
    on consume(user: String, n: Int) {
        require n > 0 else BadAmount
        let before = used.get(user) ?? 0
        require before + n <= 100 else QuotaExceeded
        used.set(user, before + n)
        return 100 - (before + n)
    }
}
```

```console
$ soma verify quota.cell
Verifying quota.cell...

Quota/invariants:

  ✓ invariant used >= 0 && used <= 100 — writer 'consume' proven by induction (writes before + n)

1 passed, 0 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK

$ soma run quota.cell consume ana 60
40

$ soma run quota.cell consume ana 60
error: require failed: QuotaExceeded: constraint violated
  --> quota.cell:9:9
  |
9 |         require before + n <= 100 else QuotaExceeded
  |         ^

$ soma run quota.cell consume ana 40
0
```

✓ means proven for every input, not just tested. Now forget the
`QuotaExceeded` line, the kind of omission that ships to production in
other languages:

```soma file=quota.cell
cell Quota {
    memory {
        used: Map<String, Int> [persistent]
        invariant used >= 0 && used <= 100
    }
    on consume(user: String, n: Int) {
        require n > 0 else BadAmount
        let before = used.get(user) ?? 0
        used.set(user, before + n)
        return 100 - (before + n)
    }
}
```

```console
$ soma verify quota.cell
Verifying quota.cell...

Quota/invariants:

  ✓ invariant used >= 0 — writer 'consume' proven by induction (writes before + n)
  ⚠ invariant used >= 0 && used <= 100 — runtime-checked (computed values): consume → used [used <= 100] because `before + n` is only known to lie in [1, ∞) — narrow it: `require (before + n) <= 100 else …`

1 passed, 1 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK

$ soma run --fresh quota.cell consume ana 60
fresh: removed .soma_data
40

$ soma run quota.cell consume ana 60
error: memory invariant violated on 'used': used >= 0 && used <= 100 — rejected write of 120 (key "ana"); the slot is unchanged
  --> quota.cell:9:9
  |
9 |         used.set(user, before + n)
  |         ^
```

The bound is no longer proven. The ⚠ line says why and which `require`
would prove it, and the runtime still refuses the bad write and leaves the
slot unchanged. `soma verify --strict` turns every ⚠ into a failure: use
it in CI.

## Lesson 4 — A lifecycle the compiler checks

Most bugs in business software are a step taken out of order: paid
before approved, shipped after cancelled. In Soma the lifecycle is a
`state` machine next to the handlers, and the properties you care about
go in `soma.toml`:

```soma file=expense.cell
cell Expense {
    state flow {
        initial: submitted
        submitted -> approved
        submitted -> rejected
        approved -> paid
        submitted -> paid          // "small amounts skip approval"
    }
    on sign_off(id: String) { transition(id, "submitted", "approved") }
    on reject(id: String)   { transition(id, "submitted", "rejected") }
    on pay(id: String)      { transition(id, "paid") }
}
```

```toml file=soma.toml
[verify]
eventually = ["paid", "rejected"]    # every expense ends one way or the other

[verify.before.paid]
requires = ["approved"]              # nothing is paid without approval
```

```console
$ soma verify expense.cell
Verifying expense.cell...

State machine 'flow': 4 states, initial 'submitted'
  States: [approved, paid, rejected, submitted]

  ✓ 4 states, 4 transitions
  ✓ all states reachable from 'submitted'
  ✓ terminal states: [rejected, paid]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
  ✓ termination: all 3 handlers structurally terminate
  ✓ refinement: handler `sign_off` ⟶ {submitted → approved}
  ✓ refinement: handler `reject` ⟶ {submitted → rejected}
  ✓ refinement: handler `pay` ⟶ {paid}
  · transition sources: `pay` calls transition(id, target) without declaring the source — the runtime refuses a move the graph forbids, but the proof does not see where the handler starts; `transition(id, from, to)` names the edge (checked by `soma check`, refused at run time from any other state)

10 passed, 0 warnings, 0 failures

  Temporal properties for 'flow':
  ✓ deadlock_free — no deadlocks in any reachable state
  ✓ eventually(state in [paid, rejected]) — all paths eventually satisfy the predicate
  ✗ requires('paid' only after one of [approved]) — 'paid' is reachable without passing through any of [approved]
    counter-example: submitted → paid
soma.toml: 2 user-defined properties loaded
Temporal: 2 passed, 1 failed
VERIFY FAILED — 1 temporal property failed
```

The verifier found the shortcut and printed the path that breaks the
rule. Remove the edge, and name the source state in `pay` so the proof
sees where it starts:

```soma file=expense.cell
cell Expense {
    state flow {
        initial: submitted
        submitted -> approved
        submitted -> rejected
        approved -> paid
    }
    on sign_off(id: String) { transition(id, "submitted", "approved") }
    on reject(id: String)   { transition(id, "submitted", "rejected") }
    on pay(id: String)      { transition(id, "approved", "paid") }
}
```

```console
$ soma verify expense.cell
Verifying expense.cell...

State machine 'flow': 4 states, initial 'submitted'
  States: [approved, paid, rejected, submitted]

  ✓ 4 states, 3 transitions
  ✓ all states reachable from 'submitted'
  ✓ terminal states: [rejected, paid]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
  ✓ termination: all 3 handlers structurally terminate
  ✓ refinement: handler `sign_off` ⟶ {submitted → approved}
  ✓ refinement: handler `reject` ⟶ {submitted → rejected}
  ✓ refinement: handler `pay` ⟶ {approved → paid}

10 passed, 0 warnings, 0 failures

  Temporal properties for 'flow':
  ✓ deadlock_free — no deadlocks in any reachable state
  ✓ eventually(state in [paid, rejected]) — all paths eventually satisfy the predicate
  ✓ requires('paid' only after one of [approved]) — every path to 'paid' passes through one of [approved]
soma.toml: 2 user-defined properties loaded
Temporal: 3 passed, 0 failed
VERIFY OK

$ soma run expense.cell reject e1
{"id": "e1", "from": "submitted", "to": "rejected"}

$ soma run expense.cell pay e1
error: invalid transition: rejected → paid — transition(id, "approved", "paid") declares its source, and 'e1' is in 'rejected', not 'approved'
  --> expense.cell:10:31
   |
10 |     on pay(id: String)      { transition(id, "approved", "paid") }
   |                               ^
```

At run time a transition the machine forbids is refused too, and the
error says which state the instance is really in. Handlers are atomic: one that fails leaves
no write and no transition behind.

## Lesson 5 — An agent in a cage, tested offline

`think()` asks a model. In Soma the answer cannot decide what happens
next on its own. `think_json(…, map("as", "Route"))` only accepts one of
the declared variants, `match` must handle every variant, the state
machine bounds where the ticket can go, and `cost` is a token bound
`soma check` proves. Tests mock the model, so they run without a key and
without a network.

```soma file=triage.cell
cell type Route { variants { Billing  Tech  Human { reason: String } } }

cell agent Triage {
    face { signal route(ticket: String, text: String) -> String }
    cost { tokens: 300 }
    memory { routed: Map<String, String> [persistent] }
    state ticket {
        initial: new
        new -> routed
        new -> escalated
    }
    on route(ticket: String, text: String) {
        set_budget(2000)
        let r = try { think_json("Route this ticket: {text}", map("as", "Route", "max_tokens", 300)) }
        if r.error != () {
            transition(ticket, "new", "escalated")
            return "human: the model failed ({r.kind})"
        }
        match r.value {
            Billing          -> { routed.set(ticket, "billing")  transition(ticket, "new", "routed") }
            Tech             -> { routed.set(ticket, "tech")     transition(ticket, "new", "routed") }
            Human { reason } -> { transition(ticket, "new", "escalated")  return "human: {reason}" }
        }
        return routed.get(ticket)
    }
}

cell test TriageTests {
    rules {
        mock think "{\"variant\": \"Billing\"}"
        assert route("t1", "I was charged twice") == "billing"
        mock think "{\"variant\": \"Refund\"}"          // a variant that does not exist
        assert route("t2", "?") == "human: the model failed (json)"
        mock think error "timeout"
        assert route("t3", "help") == "human: the model failed (llm)"
        assert get_status("t3") == "escalated"
    }
}
```

```console
$ soma check triage.cell
✓ cost: 'tokens' bound proven — peak 300 reply tokens (the max_tokens caps) ≤ declared 300 (prompts are not counted: cap them with set_budget)
✓ All checks passed (1 note above).

$ soma test triage.cell
test TriageTests ...
  ✓ assert route("t1", "I was charged twice") == "billing"
  ✓ assert route("t2", "?") == "human: the model failed (json)"
  ✓ assert route("t3", "help") == "human: the model failed (llm)"
  ✓ assert get_status("t3") == "escalated"

4 tests: 4 passed, 0 failed
```

The model invented a `Refund` variant; the program sent the ticket to a
human. `soma verify` adds `think-isolated`: the machine's safety
properties hold whatever the model answers.

## Lesson 6 — A large program, skeleton first

Past one file, the risk is no longer a wrong line but a wrong *shape*:
a function that writes what it should not, an edge nobody takes, a body
that drifts from what the design meant. And no model can keep 10,000
lines in context.

So you write the **skeleton** first. It is cells without bodies: memory,
machines, and for each signal a **frame** saying what its body may read,
write, call and which edges it may move. Comments say what each signal is
for.

```soma file=app.cell
use lib::library

// A lending library: members borrow copies; the stock never goes negative.
skeleton Stock {
    memory {
        copies: Map<String, Int> [persistent]
        invariant copies >= 0
    }
    face {
        // Copies of `book` on the shelf; 0 for an unknown book.
        signal available(book: String) -> Int   reads copies
        // Takes one copy off the shelf; false when there is none.
        signal take(book: String) -> Bool       writes copies
        signal give_back(book: String)          writes copies
        signal restock(book: String, n: Int) -> Int
            requires n > 0
            writes copies
    }
}

skeleton Loans {
    memory { holder: Map<String, String> [persistent] }   // loan id → member
    state loan {
        initial: requested
        requested -> out
        requested -> refused
        out -> returned
    }
    face {
        // Lends `book` to `member` under loan `id`: out when a copy was taken.
        signal lend(id: String, member: String, book: String) -> String
            writes holder
            moves requested -> out, requested -> refused
            calls Stock.take
        signal close(id: String, book: String) -> String
            moves out -> returned
            calls Stock.give_back
    }
}
```

```soma file=lib/library.cell
flesh Stock {
    on available(book) { return copies.get(book) ?? 0 }
    on restock(book, n) {
        let have = copies.get(book) ?? 0
        copies.set(book, have + n)
        return have + n
    }
}
```

```toml file=soma.toml
[verify.before.returned]
requires = ["out"]
```

```console
$ soma check app.cell
✓ All checks passed.
○ 4 holes — signals of a skeleton with no body yet: Stock.take, Stock.give_back, Loans.lend, Loans.close  (`soma holes app.cell`)

$ soma holes app.cell
4 holes of 6 signals in app.cell — numbered in the order to fill them (a hole comes after the holes it calls):

Stock (2)
    1. take        writes copies
    2. give_back   writes copies

Loans (2)
    3. lend    writes holder  moves requested -> out, requested -> refused  calls Stock.take
    4. close   moves out -> returned  calls Stock.give_back

the brief for one: soma skeleton app.cell Stock.take

$ soma verify app.cell
Verifying app.cell...

State machine 'loan': 4 states, initial 'requested'
  States: [out, refused, requested, returned]

  ✓ 4 states, 3 transitions
  ✓ all states reachable from 'requested'
  ✓ terminal states: [refused, returned]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  · think-isolated: judged when the 4 holes of the program have a body
  · termination: 2 holes — judged when they have a body
  · refinement: `lend` is a hole — its frame allows {requested → out, requested → refused}
  · refinement: `close` is a hole — its frame allows {out → returned}

Stock/invariants:

  ✓ invariant copies >= 0 — writer 'restock' proven by induction (writes have + n)
  ⚠ invariant copies >= 0 — runtime-checked (computed values): give_back → copies because it is a hole (its frame lets a body write any value — judged when the body exists), take → copies because it is a hole (its frame lets a body write any value — judged when the body exists)

Stock/contracts:

  · restock: requires n > 0 — no call site in the program; checked at run time on every call from outside (kind `requires`)

6 passed, 1 warnings, 0 failures

  Temporal properties for 'loan':
  ✓ deadlock_free — no deadlocks in any reachable state
  ✓ requires('returned' only after one of [out]) — every path to 'returned' passes through one of [out]
soma.toml: 1 user-defined properties loaded
Temporal: 2 passed, 0 failed
note: state machines are verified per cell. A value crosses a cell boundary by a face contract (`requires` / `ensures` on the signal); a rule between two cells' machines is proven when soma.toml states it — `[verify.before."Pay.paid"] requires = ["Approval.signed_off"]` explores the product of the machines.
○ 4 holes — signals of a skeleton with no body yet: Stock.take, Stock.give_back, Loans.lend, Loans.close  (`soma holes app.cell`)
VERIFY OK (skeleton — the holes above are open obligations)
```

With two bodies written out of six, the lifecycle and the property in
`soma.toml` are already proven. The
verifier treats each **hole** (a signal with no body yet) as anything its
frame allows, so a ✓ here holds for every body that fits. Now ask for the
**brief** of one hole: it is everything needed to write that one body,
and nothing else.

```console
$ soma skeleton app.cell Loans.lend
signal lend(id: String, member: String, book: String) -> String   // Loans, hole
    // Lends `book` to `member` under loan `id`: out when a copy was taken.
    // (declared app.cell:31)
writes     holder: Map<String, String> [persistent]   // loan id → member
moves      requested -> out
           requested -> refused
machine    loan — one instance per id (the String or Int you pass); initial `requested`
               get_status(id) is () until the id's first transition (edition 2026: `requested`) — write `get_status(id) ?? "requested"`
               requested -> out
               requested -> refused
               out -> returned
calls      Stock.take(book: String) -> Bool   [hole]   writes copies
               // Takes one copy off the shelf; false when there is none.
write      flesh Loans { on lend(id, member, book) { … } }      (the syntax a body needs, on one page: soma docs flesh)
```

Write two bodies from their briefs. The first try reuses a helper it was
not given:

```soma file=lib/library.cell
flesh Stock {
    on available(book) { return copies.get(book) ?? 0 }
    on restock(book, n) {
        let have = copies.get(book) ?? 0
        copies.set(book, have + n)
        return have + n
    }
    on take(book) {
        let n = available(book)
        if n < 1 { return false }
        copies.set(book, n - 1)
        return true
    }
}

flesh Loans {
    on lend(id, member, book) {
        if !Stock.take(book) {
            transition(id, "requested", "refused")
            return "refused"
        }
        holder.set(id, member)
        transition(id, "requested", "out")
        return "out"
    }
}
```

```console
$ soma check app.cell
error: `Stock.take` calls `available`, outside its frame (no `calls`) — if the design means it, add it to `signal take` in `skeleton Stock`: `calls available`
  --> lib/library.cell:8:5
  |
8 |     on take(book) {
  |     ^
  = code: E0120
✗ 1 error(s), 0 warning(s).
```

The frame of `take` says `writes copies`, which allows reading `copies`
but no calls. Either the body changes, or the design does: the error
names the clause to add if the design means it. Here the body changes:

```soma file=lib/library.cell
flesh Stock {
    on available(book) { return copies.get(book) ?? 0 }
    on restock(book, n) {
        let have = copies.get(book) ?? 0
        copies.set(book, have + n)
        return have + n
    }
    on take(book) {
        let n = copies.get(book) ?? 0
        if n < 1 { return false }
        copies.set(book, n - 1)
        return true
    }
}

flesh Loans {
    on lend(id, member, book) {
        if !Stock.take(book) {
            transition(id, "requested", "refused")
            return "refused"
        }
        holder.set(id, member)
        transition(id, "requested", "out")
        return "out"
    }
}
```

```console
$ soma check app.cell
✓ All checks passed.
○ 2 holes — signals of a skeleton with no body yet: Stock.give_back, Loans.close  (`soma holes app.cell`)

$ soma verify app.cell --summary
Stock/invariants:
  ⚠ invariant copies >= 0 — runtime-checked (computed values): give_back → copies because it is a hole (its frame lets a body write any value — judged when the body exists)
11 proven (✓), 4 notes (·) — `soma verify` without --summary prints them
○ 2 holes — signals of a skeleton with no body yet: Stock.give_back, Loans.close  (`soma holes app.cell`)
VERIFY OK (skeleton — the holes above are open obligations)

$ soma run app.cell restock dune 1
1

$ soma run app.cell lend L1 ana dune
out

$ soma run app.cell lend L2 bob dune
refused

$ soma run app.cell close L1 dune
error: not_implemented: Loans.close is a hole of the skeleton: no flesh gives it a body yet
  --> app.cell:35:9
   |
35 |         signal close(id: String, book: String) -> String
   |         ^
```

The writes in `restock` and `take` are proven (`requires n > 0`; `n < 1`
returned first). The second loan found the shelf empty. Two holes are
left, and calling one fails cleanly. `soma skeleton app.cell --freeze`
locks the structure: from then on a body can only fill it, and a change
to the design is a deliberate `--amend`. In a 100-signal program you keep
the same loop: `soma holes`, one brief, one body, `soma check`.

## Where to go next

- `soma docs agent`, or https://soma-lang.dev/llms.txt: the language on
  one page. `soma docs skeleton`: everything about frames, holes and
  locks. `soma docs flesh`: the syntax a body needs, to hand to whoever
  fills a hole.
- `soma example invariant state_machine` lists verified programs with
  those features; `soma example <id>` prints one. Start from a working
  program rather than from nothing.
- https://soma-lang.dev/docs/guarantees.md lists what is proven, what is
  only enforced at runtime, and what is not covered at all. Read it
  before you tell a user that something is safe.
- `soma init myapp`, or `soma init --skeleton myapp` for a large one.