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.
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
}
}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
}
}soma.toml
[verify.before.returned]
requires = ["out"]$ 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.
$ 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:
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"
}
}$ 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:
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"
}
}$ 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.