# Soma Language — for AI Agents > Soma is a declarative cell language where systems carry their proofs. > One file holds a whole service: contract (`face`), storage with invariants > (`memory`), a model-checked lifecycle (`state`), handlers, HTTP routes and > tests. `soma verify` proves the state machines; memory invariants reject > bad writes before they commit; LLM agents run inside lifecycles the > compiler proves terminate, with hard token caps. Every compiler error > names its own fix, so the write → check → fix loop converges. Everything below is current for the soma binary named in https://soma-lang.dev/version.json and generated from the compiler or verified against it. Unknown URLs on this site return 404, never a page. ## Machine-readable resources - [llms-service.txt](https://soma-lang.dev/llms-service.txt): this file + [guarantees](https://soma-lang.dev/docs/guarantees.md) (proven / enforced / not covered) + [serving](https://soma-lang.dev/docs/serving.md) (routing, exposure, atomicity) + [operations](https://soma-lang.dev/docs/operations.md) (what kills the process, ports, exit codes, HTTP statuses, limits, Linux deploy) + every gotcha — what a service needs, ~50 KB - [llms-full.txt](https://soma-lang.dev/llms-full.txt): this file + full reference + every gotcha + every builtin, one fetch (~90 KB) - [agent.md](https://soma-lang.dev/agent.md): drop-in AGENTS.md / CLAUDE.md block for a project that uses Soma - [skill/SKILL.md](https://soma-lang.dev/skill/SKILL.md): the same knowledge packaged as an agent skill - [builtins.json](https://soma-lang.dev/builtins.json): every builtin with its exact signature (from `soma describe --builtins --json`) — never guess one - [gotchas.json](https://soma-lang.dev/gotchas.json): the mistakes models make, each with the real diagnostic and the fix - [corpus/domains.json](https://soma-lang.dev/corpus/domains.json): the domains (~3 KB) → one domain's index (~12 KB, summaries, each program's verify verdict and soma.toml) - [corpus/index.json](https://soma-lang.dev/corpus/index.json): 300+ verified programs (id, title, features, url) — filter on `features`, then GET the `url` for the raw source. Per domain with summaries: `https://soma-lang.dev/corpus//index.json`. Plain listing: [index.md](https://soma-lang.dev/corpus/index.md) - [docs/reference.md](https://soma-lang.dev/docs/reference.md), [docs/builtins.md](https://soma-lang.dev/docs/builtins.md), [docs/gotchas.md](https://soma-lang.dev/docs/gotchas.md): raw markdown - [repo/index.json](https://soma-lang.dev/repo/index.json): the package registry - [status](https://soma-lang.dev/status): maturity, version, MIT license, known limits, security contact - Source: https://github.com/soma-dev-lang/soma ## Pick Soma when / skip it when Pick it when the task has a lifecycle or a limit that must hold: payments, approvals, interlocks, quotas, escrow, agent workflows with a budget — and you want to hand back evidence (`soma verify` output) instead of "I believe this is correct". Also for a small self-contained HTTP service: one file, no framework, storage and tests included. Skip it when you need a large ecosystem, a mature package set, or raw interpreter speed outside numeric `[native]` handlers. Soma is experimental: verification is per cell; cross-cell composition is linted, not proven. ## The agent loop ``` soma check app.cell # static gates FIRST: contracts, undefined # interpolation vars, unknown/ambiguous calls soma verify app.cell # prove state machines + memory invariants soma test app.cell # run `cell test` assertions (assert/assert_fails) soma run app.cell sig arg1 arg2 soma serve app.cell -p 8080 soma describe app.cell --faces # contract summary of every cell soma describe --builtins --json # exact builtin signatures — never guess soma fix app.cell # auto-repair common check errors soma docs agent # this file, offline, from the binary soma docs guarantees|serving|operations # proofs, HTTP rules, what goes wrong — offline too soma example invariant state_machine # verified programs with those features; soma example # …and the source of one soma init myapp # app.cell + soma.toml + AGENTS.md ``` Work in that order. `check` is cheap and catches most mistakes before anything runs; a `verify` failure is an error, not a warning. ## Cell anatomy ```soma cell App { face { // the contract signal add(a: Int, b: Int) -> Int // return types live HERE promise all_persistent } memory { data: Map [persistent, consistent] invariant data >= 0 // checked BEFORE every write; } // violating write rejected, slot unchanged state flow { // model-checked by `soma verify` initial: draft draft -> approved { guard { amount < 1000 } } // guard: reads the CALLING handler's locals draft -> rejected // approved/rejected: terminal (no outgoing edge) } on add(a: Int, b: Int) { return a + b } // NO return type on handlers on request(method: String, path: String, body: String) { match map("method", method, "path", path) { {method: "GET", path: "/"} -> html("

hi

") {method: "POST", path: "/add/" + id} -> handle(id) // ONE variable per pattern, at the end _ -> response(404, map("error", "not found")) } } } ``` ## Core syntax (current) ```soma let x = 42 x += 1 // no semicolons; newlines separate let v = -1 // negative literals work let s = "hello {name}" // interpolation; UNDEFINED vars are // check-time errors; no nested "..." inside {} let xs = [1, 2, 3] xs[0] = 99 // bracket index read AND write let m = map("k", 1) m["k"] = 2 // maps too; m.k and m["k"] both read let g = Game { bet: 10 } g.bet = 20 // records: literal + dot mutation g.board[0] = 7 xs[i][j] = v // nested lvalues let y = m["nope"] ?? 0 // null-coalescing; () is null for i in range(0, 10) { } range(9, -1, -1) // stepped/descending ranges sum(xs) avg(xs) min(xs) max(xs) product(xs) // reductions over lists contains(xs, x) slice(xs, 1, -1) keys(m) values(m) entries(m) // membership, slices, map views sort_by(rows, "field") sort_by(rows, r => [0 - r.total, r.name]) // stable; list key = several keys xs = push(xs, x) concat(a, b) // push/concat RETURN a new list; `+` on numeric // lists adds element-wise — it does not concatenate xs.sort() xs.reverse() m2.det() // UFCS: any builtin as method match x { 1 -> "a" n if n > 5 -> "big" _ -> "other" } // arms use -> let f = p => p * 2 f(3) // lambdas use =>; first-class data |> filter(x => x.ok) |> sort_by("score", "desc") |> top(10) let r = try { risky() } if r.error != () { ... } // error handling ``` ## Vectorized (numpy/MATLAB style) ```soma let M = [1, 0, 0, 1].reshape(2, 2) // matrices = List>, first-class A * B // matmul A + B / A - B elementwise A + 10 A / 2 // scalar broadcast (both orders) v * v v + v // numeric vectors: + * / - elementwise A > 2 v >= 1.0 // comparison masks (0/1) A.T A.shape det(A) matrix("1 2; 3 4") concat(a, b) // EXPLICIT list concatenation (+ on non-numeric lists concats) ``` ## Sum types (exhaustive — compiler refuses a missing arm) ```soma cell type Pay { variants { Charged { tx: String } Declined { reason: String } Cash } } match r { Charged { tx } -> "paid {tx}" Declined { reason } -> "no: {reason}" Cash -> "cash" } // typed state machines: state order: OrderState { initial: Placed ... } // transition(id, Variant) is compile-checked against the type // to_json(Charged { tx: "t1" }) == '{"_type":"Pay","_variant":"Charged","tx":"t1"}' // (a tuple variant carries "_values"); from_json brings the variant back; HTTP // answers a returned variant the same way. Slots store variants as variants. ``` ## Coming from Python / TypeScript ```soma map("k", v) map() // no {k: v} literal; record: Name { k: v } [1, 2, 3] [] // list literals x == () x ?? 0 // null is (); no null / None / undefined if c { a } else { b } // is an expression; no ternary; && || ! (no and/or/not) x => x + 1 // lambdas take ONE parameter for x in xs { } for k in keys(m) { m[k] } for e in entries(m) { e.key e.value } slice(xs, 1, 3) slice(xs, -2) // no xs[a:b] xs = push(xs, x) // push / concat / sort / with RETURN new values on f(n: Int) [native] { … } // annotations go AFTER the parameter list; no @decorator fail("bad_kind", "bad kind: {k}") // throw new Error(msg); catch: let r = try { … } r.detail == msg parse_int(s) ?? parse_float(s) // Number(s); to_float("5") prints 5.0; round(x) is an Int, round(x, 2) a Float m["k"] = v m.get("k") // a LOCAL map has no .set — .set/.delete/.push are slot methods f(opts: Map) … opts.x ?? 10 // keyword arguments / defaults: pass a map, read with ?? Name { k: v } is_a(r, "Name") // struct / dataclass / interface: a record literal (no class) format("%5.2f|%-8s|%03d", x, s, n) // printf / f-string widths (%d %s %f %.Nf, - and 0 flags) 7 / 2 == 3.5 idiv(-7, 2) == -3 // `/` is exact; idiv truncates toward zero, % follows the dividend's sign floor_div(-7, 2) == -4 mod(-7, 2) == 1 // Python's // and % ``` A `class` with private fields is a `cell` with `memory` slots: one instance, no `new`, no `this` — `this.hits.get(u)` is `hits.get(u)`; `constructor(a, b)` is a `configure(a, b)` handler writing a `config` slot; subclasses are the variants of a `cell type`, overridden methods one exhaustive `match` each. A script is `on main() { print(…) }` run with `soma run --fresh app.cell main`: `soma run` prints the handler's returned value (return nothing from main), and slots persist in `.soma_data/` between runs unless `--fresh`; `soma test` starts empty. `counts[k] += 1` on a missing key is `() + 1` — write `(counts.get(k) ?? 0) + 1`; `for r in rows { r.v = 2 }` changes a copy (check warns). Number literals: `1_000_000`, `0xFF`, `0b101`; strings: `\n \t \r \" \\ \u{1F600}`. `soma check` names the Soma form for each of these when you get it wrong. ## Tests `every` / `after` blocks do not run under `soma test`: call the sweeper directly (`assert _sweep(5) == ["o4"]`) with `mock now` for the clock. ```soma cell test MyTests { // a name and a `rules` block are required rules { let orders = fixture() // shared by the rules below; a bare call // is not a rule: bind it (let _ = f()) assert total(orders) == 42 // == is structural on lists/maps assert_fails pay("x") // passes when the expression RAISES assert_fails pay("x") matching "invalid transition" // …for the right reason mock think "billing" // next think() reply; or a list to queue mock think error "timeout" // next think() fails mock approve false // next approve() answer (one per call) mock price_check 120 // next call of ANY handler (a tool, an mock Notifier.send error "down" // http wrapper) answers / raises instead; // error "not_found: x" raises kind not_found mock now 1700000000 // freeze now()/now_ms()/today() until the next mock now property "sum" forall n: Int in 0..100 ensures f(n) >= 0 // 0..100 = 0…99, every value (≤ 20k) } } ``` `soma test` isolates storage (fresh per run), runs `[native]` handlers natively, and — with no LLM key configured — mocks `think()` (echo: reply = prompt). A mock scripts the NEXT call of the rule it precedes; one left unused after a rule that raised is discarded (with a note). Each `cell test` starts with fresh slots, machines and mocks. `soma test --json` gives one record per rule. `approve()` never answers on its own: unscripted it raises `approval_required` (also under serve; SOMA_APPROVE=always|never is the explicit unattended policy; `soma run` at a terminal asks). `assert` needs a Bool. A test cell calls the handlers of every cell unqualified, or as `Cell.handler(…)`; slot methods (`m.get(k)`, `xs.len`) work there too. A failure prints the asserted source, `file:line`, left/right, and the fields a value really has when `x.field` came back `()`. ## Things you would otherwise guess - A fresh id is implicitly in the initial state: `transition(id, "held")` on an id nobody created is legal; `has_state(id)` is true only once the id has TRANSITIONED — a record stored in a slot but never transitioned is "fresh" to it (test the slot for duplicates: `require m.get(id) == () else Dup`). - `transition()`'s first argument is an INSTANCE id (an order, a ticket), not the machine's name; one cell has one machine, any number of instances. - A slot is a Map or a List (`n: Int` is a check error). Read a whole slot by its bare name (`history`, `counts`); write with `counts.set(k, v)` / `counts[k] = v` / `history.push(x)`; `history = …` is an error. An invariant on a Map slot applies to every value written. - `r.kind` of a refused write is `"invariant"`; of a bad `transition()`, `"invalid_transition"`; of `require … else Tag`, `"Tag"`. - Declared parameter types are enforced at runtime: `add(points: Int)` given `2.5` raises kind `type` (400) before the body runs — no `is_int` check needed. - Values are copies: `let row = s[k] row.count += 1` changes `row` only — write it back (`s[k] = row`); a map read from a slot is a copy too (`cards.set(id, c)` after editing `c`). Records keep their field order. - In `cell test`, `request(...)` is an ordinary call: an error it does not catch RAISES (assert it with `assert_fails request(...) matching "not_found"`); the kind → HTTP status mapping is applied by `soma serve` only. Return `response(status, …)` yourself when a test must see the status. - `"""…"""` is raw for escapes (`\t` stays two characters) but `{x}` IS interpolated; write `{{` for a literal brace. - `[1, 2] + [10, 20]` is element-wise (`[11, 22]`; Floats when a value is one); `concat(a, b)` joins lists. - Persistent data lives in `.soma_data/` beside the program (serve and run); `soma test` starts empty. A slot gives back exactly what it accepted (an Int beyond 64 bits stays an Int); a value that does not fit the slot's declared value type (`Map` given a String) is refused with kind `type`. - On a List slot: `rows.push(x)`, `rows[i] = x`, `rows.delete(i)` (by index), `rows.get(i)`, `rows.len` — all invariant-checked. A Map slot's `.keys` / `.values` / `.entries` come SORTED by key (every backend); a record's own fields keep their insertion order. - A bare call to a name two cells define (`pack(id)` with `Orders.pack` and `Warehouse.pack`) is a check error: qualify it (`Warehouse.pack(id)`). - `emit ev(data)` inside one process is a synchronous, atomic fan-out to every cell with `on ev(data)`: a listener that raises fails the emitter, and the emitter's rollback takes the listeners' writes with it. Only across processes (the `[peers]` bus) is an emitted event an effect that is not rolled back. `soma check` warns when nobody handles the event. - `invariant len(rows) <= 500` is proven when the handler's ONE write that can add an entry (a `push`, or a `set` of a key not known to exist) comes after `require len(rows) < 500` and is not in a loop; a `set` after `require rows.get(k) != ()` (or in the `else` of `if rows.get(k) == ()`) cannot grow the slot. - A `require` counts for the writes of its own block and the blocks nested in it — `if ok { require n < 3 … m.set(k, n + 1) }` is proven; a require inside a loop body narrows that iteration's `let` locals only. - HTTP out: `http_get/post/put/patch/delete(url, body?, map("timeout", ms, "headers", map(...)))` never raise; non-2xx is `{error, kind, status, body}` (kind `http_status` | `timeout` | `refused` | `network`); default timeout 30 s; `mock http_post …` in tests. - `verify --strict` bounds a write only from numbers it can bound: a number read out of a record in a `Map` slot has no interval — keep the guarded number in its own `Map` slot with an invariant (the ⚠ line says `reads a slot with no interval invariant`). - `ensure cond` at the end of a handler raises kind `ensure` (422) when the postcondition is false — the whole handler is rolled back. - Dates: `parse_date("2026-03-01")` → map(year, month, day, weekday, epoch_day), `add_days`, `add_months`, `days_between`, `months_between`, `days_in_month`, `format_date(ts)`; ISO strings compare with `<`. - Money: Ints in cents (any size, exact); `div_round(n, d)` is HALF_UP division (`div_round(cents * bps, 120000)` = BigDecimal interest at scale 2); `format("%10.2f", …)` only for display, `money = "{idiv(c, 100)}.{…}"` for exact text. - Data: `read_csv(path)` → List (auto-typed cells); `agg`, `sort_by`, `top`, `median`, `pstdev`; `stdev` / `variance` are SAMPLE (n − 1) like Python's statistics, `pstdev` / `pvariance` population. `|> map`, `|> filter` and `xs[i]` are linear (20k rows in 0.1 s). - `think_json()` raises kind `json` when the model does not answer a JSON object (catch it with `try`); a ```json fence around the object is fine. A mocked `think` costs ~4 characters per token, so `set_budget` exhaustion (kind `budget`) is testable offline. Under `soma serve`, `trace()` keeps the last 1000 steps process-wide. ## Scheduled work ```soma every 30s { expire_due() } // under soma serve: runs at start-up, then every 30 s (5s, 1min, 500ms) after 10s { warm_cache() } // once, 10 s after start-up ``` A tick is a handler invocation: atomic, serialized with requests (and with other processes on the same `.soma_data`), rolled back and logged if it raises; the next tick still runs. The interval counts from the end of the previous tick. verify checks the `transition()` targets of these blocks too. ## Handlers are atomic A top-level handler invocation is all-or-nothing: if it raises, every memory write and every `transition()` it made is rolled back. A failing `try { }` block is rolled back to where it started, and the handler continues. Under `soma serve` handlers run one at a time, so read-modify-write is safe (300 parallel payments of 10 against a balance of 1000 pay exactly 100). With persistent slots the handler IS one SQLite transaction: a process killed mid-handler (`kill -9`) leaves nothing of it on disk. `every` / `after` ticks are handler invocations too (same rollback). You do not write compensation code. Not rolled back: effects outside the process (http calls, think(), emitted events). ## Errors ```soma fail("not_found", "reservation {id}") // raise: a kind + a detail require amount > 0 else InvalidAmount // raise with kind InvalidAmount (a bare tag) require open < 3 else LoanLimit "{member} holds {open} loans" // kind + interpolated detail let r = try { reserve(id) } // r = {value, error, kind, detail} if r.kind == "not_found" { return response(404, map("error", r.detail)) } if r.error != () { fail(r) } // re-raise unchanged ``` Kinds raised by the runtime: `invalid_transition`, `guard_failed`, `invariant`, `ensure`, `division_by_zero`, `index`, `llm`, `budget`, `type`, `json` (a body that is not JSON), `stack_overflow`, `approval_required` (`approve()` with nobody to answer). Branch on `r.kind`, never on substrings of `r.error`; in tests `assert_fails f() matching "not_found"` matches the kind or the message. ## HTTP `response(status, body)` is a map `{_status, _body}` (assert `r._status == 404`); `html(..)`, `redirect(..)` likewise. A handler may also return a plain map or string (200). `soma run app.cell request GET /path ""` calls the router without a server; `soma serve app.cell -p 8080` serves it. Static files: `static/`. `soma serve` ALSO exposes every public handler of the request-owning cell at `///` (that is how forms post to `/add`). A path that `request` matches explicitly goes to `request`; prefix handlers that must not be reachable over HTTP with `_` (`on _debit(…)`). `soma check` warns when a handler and a route share a name unless the route delegates to that handler. `body: String` is the raw text (`from_json(body)`); `body: Map` is the parsed JSON (a non-JSON body is a 400 before the handler runs) — the same under serve, test and run. A raised error answers with its kind: not_found → 404, guard_failed → 403, invalid_transition → 409, invariant → 422, your own `fail("tag")` / `require … else Tag` → 400, as `{"error": message, "kind": tag}`. A plain return answers 200: a map/list as JSON, `()` as `null`, a String or number as `{"result": …}`. Path segments and query values are coerced to the parameter's declared type (`/decide/x/true` → Bool). Every response carries `Access-Control-Allow-Origin: *`. `request` may be declared in `face` or not; its return type is not checked (a route answers whatever it returns). `serve` binds 127.0.0.1 (`--host 0.0.0.0` to expose), refuses a taken port and a program that fails check, and survives a handler's runaway recursion (500 `stack_overflow`; the process stays up). ## Verification properties `soma verify` proves, for every cell with a state machine: reachability, deadlock-freedom, liveness (every state can reach a terminal), refinement (each handler's `transition()` targets are declared states — the SOURCE of a transition is the instance's runtime state, so a removed edge is caught at runtime as `invalid_transition`, not by verify; declare `[verify.before.X] requires` for the edges you care about), and termination of every handler whose recursion has a decreasing argument — a handler it cannot prove (`while true`, `rec(n + 1)`) is a ⚠ warning, not a proof, and the runtime depth guard is what stops it. `property … forall n in a..b` in tests walks EVERY value up to 20,000, samples with a fixed seed beyond that (not a proof). State more in a `soma.toml` beside the program (`[package]` is optional; an unknown key is an error): ```toml [verify] cells = ["Expense"] # optional: which cells these apply to deadlock_free = true # (always on; the key is accepted) eventually = ["paid", "rejected"] # every path reaches one of these (AF) never = ["corrupt"] # unreachable states (AG not) always = ["a", "b", "c"] # the machine is only ever in one of these [verify.after.rejected] never = ["paid"] # `paid` is unreachable once `rejected` was reached eventually = ["archived"] # after `rejected`, every path reaches `archived` [verify.before.paid] requires = ["manager_approved"] # precedence: no path reaches `paid` without ONE of these requires_all = ["held", "picked"] # …without EACH of these ``` In the machine, `* -> failed` means from EVERY state — it also adds `paid -> failed`, so `paid` is no longer final (verify says so). Keep states final with `* -> failed except [paid, denied]`. A property naming a state no machine declares is an error, and verify ends with one verdict line (`VERIFY OK` / `VERIFY FAILED — …`). `soma verify` and `soma test` refuse a program that fails `soma check`. Invariants on computed values are proven by induction when interval reasoning suffices (`(counts.get(k) ?? 0) + 1` keeps `counts >= 0`; `let open = … require open < 3 … set(k, open + 1)` keeps `<= 3` — an unconditional `require` on a once-bound local counts); the rest is reported per conjunct as runtime-checked. `soma verify --strict` fails on every ⚠ too (a proof that degraded to runtime-checked, an unprovable termination) — the CI gate. A failed property prints a counter-example path and is an error. What verify does NOT prove: data-dependent rules inside handlers, and invariants on computed values (those are runtime-checked — reported as such, never as "proven"). Guards (`a -> b { guard { cond } }`) are enforced at runtime and read the locals of the handler that calls `transition()`; the model keeps guarded edges. A `cost { tokens: N }` that cannot be proven (a think() without a literal max_tokens) is a check ERROR, not a note. ## Agents (LLMs inside the cage) ```soma cell agent Researcher { face { signal research(topic: String) -> Map tool search(q: String) -> String [capability: "https://api.x.com/*"] "Search" } state job { initial: idle idle -> working working -> done * -> failed } on research(topic: String) { set_budget(5000) // hard token cap transition("t", "working") let facts = think("Research {topic}", map("max_tokens", 2000)) transition("t", "done") return map("facts", facts, "spent", tokens_used()) } } // soma verify PROVES the lifecycle; add `cost { tokens: 2000 }` (also // latency:, usd:) to the cell and soma check PROVES the bound when every // think() has a literal max_tokens and runs a known number of times. // approve(msg) is a gate a PERSON answers: tests script it (mock approve), // serve raises approval_required unless SOMA_APPROVE says otherwise. // think(prompt, map(..)) or think(prompt, system, map(..)): options go LAST. // Offline: `mock think …` in tests, SOMA_LLM_MOCK=echo | fixed:TEXT, or // [agent] mock = "echo" in soma.toml. Record/replay: --record, soma replay. ``` ## Top gotchas (full list: /docs/gotchas.md or /gotchas.json — all verified) 1. `f(args)` calls YOUR handler `f` when one takes that many arguments, the builtin `f` otherwise (`on list() { return list(1, 2) }` reaches the builtin). `soma check` warns when an argument count sends a call to a builtin you probably did not mean. Another cell's handler: `Ledger.post(x)` (or bare `post(x)` when the name is unique); `get_status(id)` answers the initial state for an unknown id — `has_state(id)` tells them apart. 2. `match` arms use `->` (`=>` is lambdas). Handlers don't declare return types (face signals do). 3. No nested string literals inside `{...}` interpolation — bind a let first. 4. `==` is structural on lists, maps and variants (`[] == []`, key order irrelevant). `null`/`None` do not exist: null is `()`, test with `x == ()` or default with `x ?? 0`. 5. `transition()` returns {id, from, to}; read state with get_status(id). Wrap fallible transitions in try { }. 6. Slot methods (.set/.get) are for `memory` slots; local maps use m[k]. 7. `assert_fails expr` needs an expression that RAISES (not a falsy bool). 8. serve routes only the cell that owns `request` — put routable signals there, delegating to domain cells. 9. Adjacent string literals don't concatenate (`return "a" "b"` is a check error); `on` and `given` are reserved words. 10. Floats: compare with a tolerance, never ==. 11. `7 / 2` is `3.5` — everywhere, `[native]` included. `idiv(7, 2)` is the integer quotient (truncates toward zero, BigInt-exact). 12. One memory invariant names one slot; `size` invariants also guard `delete`. A cost bound is *proven* only when every `think()` runs a known number of times (literal `range`, `[loop_bound(N)]`); a declared bound that cannot be proven is a check ERROR. ## Packages ```toml [dependencies] matrix = "^0.2" # semver; registry at soma-lang.dev/repo local = { path = "../pkg" } # or git = "...", subdir = "packages/x" ``` `soma install` → .soma_env/packages/, commit-pinned in soma.lock. `use matrix` imports it. A package's API = its face; its proofs (cell test) re-run on YOUR toolchain: `soma test .soma_env/packages/matrix/matrix.cell`. ## Performance Interpreter is the reference semantics (linear-time `map`/`filter`/indexing; a 20k-row CSV aggregation runs in ~0.3 s interpreted). Annotate hot handlers `[native]` for Rust-codegen: measured at rustc -O parity (16.8 ns/op) on numeric loops; a native compile failure aborts the run (there is no silent fall-back to the interpreter). `soma check` verifies the native vocabulary (every handler, every error at once). Same semantics as the interpreter: `7 / 2` is 3.5, a division by zero is an ordinary `try`-catchable error, an Int overflow promotes to BigInt, and an Int slot refuses a non-exact `/` instead of truncating. What a `[native]` handler may use — nothing else: - parameters and locals: Int, Float, Bool, String (a List cannot cross the boundary in either direction: parse the input into buffers inside the handler, return a String) - arithmetic, comparisons, `if`/`while`/`for i in range(a, b)`, `return`, sqrt log exp pow abs min max floor ceil round sin cos random, idiv gcd pow_mod sqrt_int, band bor bxor bnot shl shr bit_len bit_test bit_set bit_clr bit_next, to_int to_float to_string, str_len str_at str_eq, sibling `[native]` handlers - arrays: `buffer(n) -> Buf` (n Ints, zeroed), `buf_get(b, i) -> Int`, `buf_set(b, i, v)`; `buffer_f(n)` / `buf_get_f` / `buf_set_f` for Floats - maps: `hashmap() -> HMap` (Int → Int), `hm_get(m, k)`, `hm_set(m, k, v)`, `hm_inc(m, k)`, `hm_len(m)`, `hm_has(m, k)` - strings: `strbuf() -> SBuf`, `sb_push(b, s)`, `sb_push_int(b, n)`, `sb_push_char(b, c)`, `sb_len(b)`, `sb_finish(b) -> String`; `regex_count / regex_replace / regex_match`; `read_file read_stdin write_str` (write_str flushes; an Int overflow re-runs the handler in BigInt mode, so text written BEFORE the overflow is repeated — keep write_str away from overflow-prone arithmetic, or return the text) - a Buf/HMap/SBuf lives in ONE variable of ONE handler: it cannot be re-bound (`let t = u u = v` — copy elements instead), returned, or passed to a sibling (pack results into a String with strbuf). A Buf holds 64-bit Ints: a value that overflows i64 while stored into it is a `range` error (scalars promote to BigInt; mask the value or keep it scalar). `for` takes `range(a, b)` only (a step → `while`). A literal `/ 0` does not compile. `soma check` reports all of these. - one FFI call costs ~2 µs: make the LOOP native, not just the per-element kernel (10^7 sibling calls inside a native loop: 20 ms; 2·10^6 calls from an interpreted loop: 3.5 s). Not available natively: maps/lists/records, think(), memory slots, `try`, `match`, string interpolation — call an interpreted handler for those. The buffer / hashmap / strbuf primitives exist ONLY in `[native]` handlers (`soma check` refuses them elsewhere); everything else in the list, `sin`, `regex_*`, `read_stdin` included, works in interpreted handlers too. ## Learn from working code - https://soma-lang.dev/corpus/index.json — 300+ programs, all passing check+test (algorithms, web, agents, state machines, finance, games, data, safety interlocks, medical, aerospace…). Before writing a cell, fetch one with the features you need and adapt it. - treasury/ airlock/ poker/ elevator/ hft/ delivery/ — complete apps where the safety property is a verified theorem - packages/matrix/ — the reference package (numpy-style linalg, 43 proofs) --- # What Soma guarantees — and what it does not Three columns, no adjectives. If a claim about Soma is not in the first two columns, it is not a guarantee. ## 1. PROVEN statically — by `soma verify`, before the program runs On the **state machine** of each cell (a finite graph, model-checked): | Property | Meaning | How to ask | |---|---|---| | Reachability | every declared state can be reached from `initial` | always | | Deadlock-freedom | no reachable non-final state without an exit | always | | Liveness | every state can reach some final state | always (n/a for cyclic machines — said so) | | `eventually = [...]` | every path reaches one of these states | `soma.toml [verify]` | | `never = [...]` | these states are unreachable | `soma.toml [verify]` | | `always = [...]` | the machine is only ever in one of these states | `soma.toml [verify]` | | after … `never` | once X was reached, Y is unreachable | `[verify.after.X] never = ["Y"]` | | after … `eventually` | after X every path reaches one of … | `[verify.after.X] eventually = [...]` | | precedence | no path reaches T without one of / each of … | `[verify.before.T] requires / requires_all` | On the **handlers**: | Property | Meaning | |---|---| | Refinement | every `transition(id, "x")` with a literal target is a declared edge, and every declared edge is taken by some handler (or reported) | | Termination | handlers terminate: bounded loops, recursion with a decreasing argument and a base case, no call cycles | | Think-isolation | with only literal transition targets, the properties above hold whatever an LLM returns | | Cost bound | `cost { tokens: N }` holds when every `think()` has a literal `max_tokens` and runs a known number of times (across sibling handlers) — a declared bound that cannot be proven is a `soma check` error (worded "bound is advisory"), never a silent pass | | Invariants on known values | a write of a literal, a `clamp(..)`, or a value interval reasoning can bound — including by induction on the slot's own invariant: `(counts.get(k) ?? 0) + 1` keeps `counts >= 0` | A failed property prints a counter-example path. A property that names a state no machine declares is an error. `soma verify` refuses a program that fails `soma check`. **"Eventually" is a statement about the graph.** It says no path avoids the target forever; it does not say anyone will call your handlers. A payment can sit in `authorized` until someone acts. ## 2. ENFORCED at runtime — always on, cannot be bypassed from Soma code | Mechanism | Guarantee | |---|---| | Memory invariants | checked **before** every `set`, bracket write, `push` and `delete` (for `size`). A violating write raises (`kind "invariant"`) and the slot is unchanged. `soma verify` lists each write it could not prove as *runtime-checked*. | | Transitions | `transition()` to an undeclared edge raises `invalid_transition` with the valid targets. Guards raise `guard_failed`. | | **Atomic handlers** | a handler that raises leaves nothing behind: its memory writes and transitions are rolled back. A failing `try { }` block is rolled back to where it started. Consequence: an error means "nothing happened" — to *record* a refusal (a reservation moved to `rejected`), return it as a value instead of raising. | | **Serialized handlers** | under `soma serve`, top-level handler invocations run one at a time: read-modify-write needs no lock. | | `require` / `ensure` / `fail` | raise; errors carry a `kind` a caller can branch on. | | Token budget | `set_budget(N)` stops `think()` when the budget is spent. | | Exhaustive `match` | a missing sum-type arm is a `soma check` error, not a runtime surprise. | ## 3. NOT COVERED — know this before you rely on Soma - **Data-dependent rules inside handlers** ("amount ≤ order total", "no refund after 30 days"). They are your `if`s and guards. Guards are enforced at runtime, not proven; the model checker keeps guarded edges. - **Cross-cell composition.** Verification is per cell. "stock was taken iff the reservation is held" across two cells is tested, not proven (atomic handlers do cover the rollback of both cells' writes within one invocation). - **Conservation / aggregate properties** ("the sum of balances never changes"). An invariant sees one written value at a time. - **Effects outside the process** are not rolled back: HTTP calls, `think()`, files, events sent over the `[peers]` bus to another process. (An `emit` handled by a cell of the same process IS inside the handler's transaction: synchronous, and rolled back with it.) - **Untyped records.** A record is a map: a typo'd field name reads as `()`. Ordering against `()` raises, equality does not. - **Authentication, authorization, TLS, rate limiting**: `soma serve` has none. Put it behind a reverse proxy. - **Throughput.** Handlers are serialized and the interpreter walks the AST; `[native]` is for numeric kernels only. - **Maturity.** Experimental, one author, one package in the registry. The verifier itself is tested (adversarially, with mutation and differential runs) but not mechanically verified. --- # `soma serve` — exactly what gets exposed, and how ``` soma serve app.cell -p 8080 # HTTP on :8080 soma run app.cell request GET /stats "" # call the router with no server ``` ## Routing: three rules, in this order 1. `GET /static/` serves `/static/` — confined to that directory (`..` cannot escape it). 2. A path that the cell's `request(method, path, body)` handler **matches explicitly** — a literal (`"/stats"`) or a prefix pattern (`"/hold/" + id`) in one of its `match` arms — goes to `request`. 3. Otherwise, if the first path segment is the name of a **public handler** of the request-owning cell, that handler is called with the remaining segments and query values as arguments: `POST /add/5` → `add(5)`. This is how an HTML form posts to `/add`. Anything else goes to `request` (or 404 without one). **Every public handler of the request-owning cell is therefore an HTTP endpoint** — except `request` itself, which is only ever the router. A handler is private when its name starts with `_` (`on _debit(account, amount)`), or when it lives in another cell. Put domain logic in its own cell and keep the HTTP cell thin. `soma check` warns when a handler and one of `request`'s routes share a name. Only the cell that defines `request` is routed. Other cells are reachable from it by calling their handlers by name. ## Requests and responses `request` receives `(method, path, body)` — and a fourth `query: Map` argument when it declares one. The declared type of `body` decides its shape, identically under `soma serve`, `soma test` and `soma run`: - `body: String` — the raw request text; `from_json(body)` parses a JSON body (it raises kind `json` on invalid JSON: wrap it in `try`). - `body: Map` — the JSON object (or form fields) already parsed; a request whose body is not JSON is answered `400 {"kind": "json"}` before the handler runs; an empty body is `map()`. A handler may return: | Return value | HTTP | |---|---| | a Map or a List | `200`, JSON | | a String or a number | `200`, `{"result": …}` (JSON) | | `()` | `200`, `null` | | `response(status, body)` | that status; the value is `{_status, _body}` — assert `r._status == 404` in tests | | `html(body)` / `html(status, body)` | HTML | | `redirect(url)` | `302` | An error the handler does not catch is answered by its kind, as `{"error": "kind: detail", "kind": kind}`: `not_found` → 404; `guard_failed`, `forbidden`, `approval_required` → 403; `invalid_transition`, `conflict` → 409; `invariant`, `ensure` → 422; `json`, `type`, `division_by_zero` and your own `require … else Tag` / `fail("tag")` → 400; `stack_overflow`, `llm`, `budget`, undefined names → 500 (the full table is in operations.md). Map a kind yourself only when you want a different status or body: ```soma let r = try { _hold(id) } if r.kind == "invalid_transition" { return response(410, map("error", r.detail)) } if r.error != () { fail(r) } // re-raise: the default mapping answers (under serve; a test sees the raised error) ``` Path segments reach `request` percent-decoded (`/stock/a%20b` → `"/stock/a b"`). Path patterns hold ONE variable, at the end (`"/loans/" + rest`); split `rest` for more segments, or take the rest from the body or query. Public handlers (no `_` prefix, `request` aside) are also reachable directly at `///…`: arguments are coerced to the declared parameter types (`/decide/x/true` → Bool), a trailing `Map`/`List` parameter takes the JSON body (a non-JSON body → `400 {"kind": "json"}`). At start-up `serve` calls a zero-argument `start()` (or `init()`) handler when the cell has one. ## Concurrency and atomicity Each request runs on its own thread, and **top-level handler invocations are serialized**: one handler at a time, process-wide. A handler that raises is rolled back (writes and transitions). You do not need locks or compensation code; you do pay for it in throughput, and a `think()` call holds the line for as long as the model takes. ## Storage `[persistent]` slots live in `/.soma_data/soma.db` (SQLite). `soma run` uses the same database, so state carries over between runs; `soma test` uses fresh in-memory storage every time. ## What `soma serve` does not do No TLS, no authentication, no header access from handlers, no rate limiting. It binds 127.0.0.1 (`--host 0.0.0.0` to expose it). `PORT + 2` (the signal bus) is opened only when a cell uses `emit`, declares `scale`, or `--join` is given — the start-up log says `bus: listening` or `bus: not started`; `PORT + 1` only when a cell declares `on ws`. Every response, static files, the dashboard and the pre-handler 400s included, carries `Access-Control-Allow-Origin: *` (browsers on any origin may call it; put a proxy in front to restrict). `--no-schedule` starts the HTTP side without the `every` / `after` threads (tests, debugging). Run it behind a reverse proxy and firewall the bus port. --- # Operating a Soma service — what happens when it goes wrong Tested facts about the process, not intentions. Version: `soma --version` (the website's `/version.json` says which release is published; a served program has no such route). ## What kills the process, what does not | Event | Effect | |---|---| | A handler raises (require, invariant, transition, `fail`, division by zero, a String reaching an `Int` parameter) | That request is answered with a 4xx/5xx JSON body (table below); every write and transition of the request is rolled back; the process stays up | | Runaway recursion in a handler | Answered `500 {"kind": "stack_overflow"}` at depth 512; request threads have a 64 MB stack so the guard fires before the OS does; the process stays up | | A `[native]` handler panics (a `buf_get` past the end, an `idiv` by zero) | Caught at the boundary: an ordinary `try`-catchable error with the same kind the interpreter would raise (`index` → 400, `division_by_zero` → 400); the process stays up. Int overflow does not panic: it promotes to BigInt exactly as interpreted code does | | `think()` fails or times out | Kind `llm`, rolled back like any error; the request is answered, not hung: one provider round-trip is capped at 60 s (`timeout_ms` in the options map, or `SOMA_LLM_TIMEOUT_MS`), retried up to 3 times on 429/5xx | | A scheduled `every` / `after` block raises | Logged, rolled back (writes and transitions — it is a handler invocation), next tick runs | | Port already answering, `soma check` errors, an unreadable file | `soma serve` refuses to start and exits 1 — it never serves a program that does not check (`--no-check` overrides) | | Out of memory, SIGKILL, `kill -9`, SIGTERM | The process dies at once (no draining: an in-flight client gets an empty reply); committed handlers are in `.soma_data/soma.db` (SQLite); the handler in flight is lost as a whole — its writes sat in one uncommitted SQLite transaction | | Disk full while writing | Expected (not exercised): the SQLite write fails, the request is rolled back and answered 500 | | A slow upstream (`http_post` to a service that hangs) | The handler holds the process-wide lock for the whole call: every other request waits. Every http builtin has a timeout (default 30 s; pass `map("timeout", ms)`) — keep it short; the upstream is not cancelled | | A slow handler (a quadratic loop, a huge `to_json`, a loop of 100 000 `slot.set`) | Handlers run one at a time: every other request and every scheduler tick WAITS for it — there is no per-request time limit. `soma verify` proves termination, not speed. A persistent slot write costs about 1 ms (each is an SQLite statement): a 100 000-key rebuild in one handler holds the process for ~2 minutes. Keep handlers short; batch bulk loads outside the request path; put a proxy timeout in front | | The program changed and `.soma_data/` is older | A renamed slot is a new empty slot (the old rows stay in the file); a slot whose value TYPE changed gives back the old values with their old type; an invariant added later is not checked against stored values (verify proves it for future writes only); a state-machine instance stored in a state the new machine no longer declares takes no transition, `*` edges included. `soma serve` and `soma run` audit the database at start-up and print one `warning: stored data: …` line per problem: instances in undeclared states, values an invariant refuses, values of another type than declared, slot data no slot declares any more (renamed/removed). Migrate (below) or delete `.soma_data/` | ## Addresses and ports - `soma serve app.cell -p 8080` binds **127.0.0.1:8080**. Nothing is reachable from the network until you pass `--host 0.0.0.0` (or put a reverse proxy in front — recommended: TLS, auth and headers are the proxy's job; Soma reads none). - The event bus for `emit` between processes binds port **+2** (8082), the WebSocket endpoint port **+1** (8081) only when a cell declares `on ws(...)`. Both follow `--host`. - `serve` probes the port first: a process already answering there is an error (exit 1), not a silent bind beside it. - The dashboard is `/__soma/` on the same port; static files are served from `./static/` only. ## Exit codes | Command | 0 | 1 | |---|---|---| | `soma check` | no errors (warnings allowed) | at least one error | | `soma verify` | `VERIFY OK` (vacuous when the program has no state machine — it says so) | `VERIFY FAILED …` (also when `soma check` fails) | | `soma test` | every assertion passed | any failure, or `soma check` fails, or no test cell | | `soma run` | the handler returned | the handler raised, or the program does not check, or the handler name is unknown | | `soma serve` | (runs until stopped) | cannot start: port taken, check errors, bind failure | | `soma deploy` | provider CLI succeeded | the CLI is missing or failed (the Dockerfile is still generated) | | `soma docs`, `soma example` | printed | unknown topic / no match | `--json` on `check`, `verify`, `test`, `describe`, `example` prints machine-readable stdout (also for a fatal error such as an unreadable file); diagnostics go to stderr. `soma verify --strict` turns every ⚠ into a failure. ## HTTP answers for a raised error Body: `{"error": "", "kind": ""}`. | kind | status | raised by | |---|---|---| | `not_found` | 404 | `fail("not_found", …)` | | `guard_failed`, `forbidden`, `approval_required` | 403 | a transition guard; `fail("forbidden")`; `approve()` with nobody to answer | | `invalid_transition`, `conflict` | 409 | `transition()` off the machine; `fail("conflict")` | | `invariant`, `ensure` | 422 | a memory invariant refusing a write; `ensure` | | `json`, `division_by_zero`, `type`, `index` | 400 | a non-JSON body for `body: Map`; arithmetic; a wrong-typed argument or a value that does not fit the slot's declared type; a list index out of range (also from a `[native]` buffer) | | your own `require … else Tag` / `fail("tag", …)` | 400 | the program refused the request | | `stack_overflow`, `llm`, `budget`, `undefined_variable`, `undefined_function`, `no_handler` | 500 | the program itself is wrong or the world failed | A handler that returns normally answers 200 with its value as JSON (`()` is `null`, a String is `{"result": "…"}`), or the status inside a `response(status, body)` map. ## Limits - Int is arbitrary precision (i64 fast path, BigInt beyond); Float is f64; `7 / 2` is `3.5`. - Recursion depth: 512 frames, then `stack_overflow`. - Request bodies and paths: no configured cap; 20 MB bodies and 20 KB paths were served without crashing. Put the cap on the proxy. - Handlers run one at a time (a process-wide lock): correct under contention, no parallelism inside one process. Throughput is not a goal. - `forall` properties in tests walk every value up to 20 000, then sample with a fixed seed. - One process, one SQLite file (`.soma_data/soma.db`, created beside the program); no replication unless a `scale` section and a bus join are configured (experimental). ## Migrating stored data There is no migration command: a migration is a handler, run once with `soma run` against the same `.soma_data/` (it shares the database with a running `soma serve`, and like every handler it is one transaction). - **Added slot / field**: old rows read `()`. Backfill in a one-shot handler (`for id in skus.keys { if prio.get(id) == () { prio.set(id, 2) } }`), or default at read time (`prio.get(id) ?? 2`). - **Renamed state**: run a copy of the program that still declares the old state and an edge out of it (`picked -> packed`), with a `_migrate` handler calling `transition(id, "packed")` for each stuck id; then serve the new program. `soma run migrate.cell _migrate`. - **Renamed slot**: keep the old slot declared next to the new one for one release, copy in `_migrate`, then drop it. The audit names the orphaned rows until then. - **Re-typed slot**: read, convert, `set` — or rename the slot. - **Tightened invariant**: stored values that violate it are served but can not be written back; fix them in `_migrate` or keep the old bound. Make `_migrate` idempotent (check before writing) and back up `.soma_data/soma.db` first. ## Environment variables | Variable | Effect | |---|---| | `SOMA_LLM_KEY` (or `ANTHROPIC_API_KEY`, `OPENAI_API_KEY`) | the provider key for `think()`; without one `soma test` mocks and `soma serve` raises kind `llm` | | `SOMA_LLM_MOCK=echo` \| `fixed:` | `think()` never reaches a provider (overrides `[agent] mock` in soma.toml); `soma serve` prints `llm: MOCK …` at start-up when the program calls think | | `SOMA_LLM_TIMEOUT_MS` | one provider round-trip cap (default 60 000) | | `SOMA_APPROVE=always` \| `never` | answers `approve()` when no terminal is attached (`soma serve` fails closed otherwise: 403 `approval_required`) | | `PORT` | not read — pass `-p` | ## Between processes `emit` reaches every cell of the same process synchronously. Across processes it needs the bus: a `[peers]` table in soma.toml (`other = "host:PORT+2"`) on the sending side. `--join host:bus-port` registers a node for `scale` sharding; it does not by itself forward `emit`. A peer that is down when the process starts is logged as `peer: … failed` and not retried — start the receiving process first. This is the experimental corner of Soma; single-process is the supported shape. ## Persistence `[persistent]` slots and state-machine instances live in `.soma_data/soma.db` next to the `.cell` file (wherever the command is run from), shared by `soma serve` and `soma run`; `soma run --fresh` deletes it first. `soma test` starts from empty storage every run. Back up the file; there is no migration tool — a renamed slot is a new, empty slot. Values round-trip exactly: an Int beyond 64 bits comes back as that Int, a variant as a variant, `()` as `()`. A write that does not fit the slot's declared value type (`Map` given a String or `1.0`; `Map` given a plain map) is refused with kind `type` before it commits; an Int written to a `Float` slot is stored as a Float. One process holds one connection to the database and each handler runs inside `BEGIN IMMEDIATE … COMMIT`, which also serializes handlers across processes. ## Deploying on Linux There is no published Linux binary yet; build from source (Rust stable + GMP): ```sh apt-get install -y build-essential libgmp-dev m4 git git clone --depth 1 --branch v https://github.com/soma-dev-lang/soma cd soma/compiler && cargo build --release # ./target/release/soma serve /srv/app/app.cell -p 8080 --host 0.0.0.0 ``` `soma deploy --target fly|cloudflare|aws` generates a multi-stage Dockerfile that does exactly this (build stage `rust:1-bookworm`, runtime `debian:bookworm-slim` + `libgmp10`) and invokes the provider CLI; a missing CLI exits 1 after generating the files. A systemd unit is a one-liner: `ExecStart=/usr/local/bin/soma serve /srv/app/app.cell -p 8080`, `WorkingDirectory=/srv/app` (the database lives there), `Restart=always`. ## Logs One line per request on stderr: `POST /pay/x → 409 2ms invalid transition …`. Start-up prints the cell, its handlers, the database path, the bind address and the dashboard URL. No log files are written by Soma; use the supervisor's. --- # Verified wrong→right pairs # Soma for agents: verified wrong → right The mistakes an LLM makes writing Soma, each with the **actual compiler error** and the fix. Every pair below is verified against the current `soma` binary. This is the self-correction corpus: when `soma check` / `soma run` emits one of these errors, apply the paired fix. A rule of thumb: **`soma check` catches most of these before you run.** Write the file, run `soma check app.cell`, fix what it reports, repeat. --- ## 1. Nested string literals inside `{...}` interpolation ```soma // WRONG — a string literal inside an interpolation segment return "len: {len(\"hi\")}" // error: string interpolation cannot evaluate a nested string literal // in '{len("hi")}' — bind the value with a let first ``` ```soma // RIGHT — bind it, then interpolate the variable let n = len("hi") return "len: {n}" ``` ## 2. `match` arms use `->`, not `=>` ```soma return match x { 1 => "a" * => "b" } // error: match arms use '->', not '=>' ``` ```soma return match x { 1 -> "a" * -> "b" } ``` `=>` is **lambda** syntax (`p => p + 1`). `->` is match arms and signal return types. Don't cross them. ## 3. Handlers don't declare return types ```soma on add(a: Int, b: Int) -> Int { return a + b } // error: handlers do not declare return types — put '-> Int' on the // signal declaration inside face { } ``` ```soma face { signal add(a: Int, b: Int) -> Int } on add(a: Int, b: Int) { return a + b } ``` ## 4. Adjacent string literals do NOT concatenate ```soma return "hello " "world" // error: in G.hello: a string literal follows `return` and is never // evaluated — adjacent string literals do not concatenate ``` ```soma return "hello world" // one literal let name = "world" return "hello {name}" // or interpolate ``` (`soma check` also warns on any other unreachable statement after `return` / `break` / `continue`.) ## 5. `==` IS structural on lists, maps and variants ```soma [1, 2] == [1, 2] // true map("US", 1, "EU", 2) == map("EU", 2, "US", 1) // true — key order is irrelevant [] == [] // true ``` `<`, `>` on lists or maps is an error (compare a field or `len()`), and values of different kinds are an error to compare (`1 == "1"`), not `false`. ## 6. Float equality needs a tolerance ```soma return 0.1 + 0.2 == 0.3 // false — floating point ``` ```soma return abs((0.1 + 0.2) - 0.3) < 0.0001 ``` ## 7. `transition()` returns a map, not the target string ```soma on advance(id: String) { return transition(id, "next") // returns {id, from, to}, not "next" } ``` ```soma on advance(id: String) { transition(id, "next") return get_status(id) // the new state as a string } ``` Guard fallible transitions with `try`: ```soma let r = try { transition(id, "next") } if r.error != () { return map("error", r.error) } ``` ## 8. `is_a` does not recognize sum-type VARIANTS — match them ```soma let b = Box { w: 3 } // Box is a `variants` constructor return is_a(b, "Box") // false — variants aren't tagged records ``` ```soma // extract the kind with an exhaustive match handler on kind(s: Map) { return match s { Box { w } -> "Box" // ... every variant } } ``` (`is_a` / `is_type` DO work on record literals: `is_a(Game { x: 1 }, "Game")` is `true`.) ## 9. There is no `cell type X { fields { ... } }` Records are plain map-shaped values. Construct them with a literal: ```soma let g = Game { bet: 10, pot: 0 } // a field-accessible value (a Map) g.bet = 20 // mutate fields in place let b = g.bet return is_a(g, "Game") // true — record literals carry _type ``` Use `cell type X { variants { ... } }` only for *sum types* (tagged unions). ## 10. `soma serve` routes only the cell that owns `request` ```soma // other cells' signals are NOT auto-routed as HTTP endpoints ``` ```soma // put every routable signal on the request-owning cell, delegating // to domain cells: cell Api { face { signal request(...) -> String signal place(...) -> Map } on place(...) { return place_order(...) } // delegate to Orders on request(method, path, body) { ... } } ``` --- ## These USED to be limitations and now WORK — use them freely Older Soma code worked around these; the current language supports them directly. Prefer the direct form. ```soma // bracket indexing (read + write) on lists, maps, strings let x = xs[2] xs[2] = 99 let v = m["key"] m["key"] = 1 let c = s[0] // negative literals let n = -1 // not `0 - 1` // descending / stepped ranges for r in range(10, 0, -1) { } // not build-then-reverse // numeric reductions over a list sum(xs) product(xs) avg(xs) min(xs) max(xs) // UFCS — any builtin is a method xs.sum() xs.sort() xs.reverse() m.det() m.transpose() // nested record/list mutation g.board[0] = 99 g.meta.turn = 5 xs[i][j] = v // matrices are first-class, with vectorized (numpy-style) operators let M = [1,0,0,1].reshape(2,2) let P = A * B let t = M.T det(M) A + 10 A / 2 1 - A // scalar broadcast on matrices v * 2 v - 1 v * v v + v // vector broadcast + elementwise (+ * / -) A > 2 v >= 2.0 // comparison masks (0/1) // list CONCATENATION is concat(a, b); non-numeric lists keep + = concat // `with` is functional copy-update for maps AND lists let m2 = with(m, "k", 9) let l2 = with(xs, 0, 9) ``` --- ## The agent loop, in commands ``` soma check app.cell # contracts, interpolation, dispatch — fix these first soma verify app.cell # PROVE state machines + memory invariants soma test app.cell # run `cell test` assertions (assert / assert_fails) soma run app.cell sig a # execute a handler soma serve app.cell -p 8080 soma describe app.cell --faces # token-cheap contract summary of every cell soma describe --builtins --json # the exact builtin signatures (never guess) ``` When unsure of a builtin's signature, run `soma describe --builtins` — do not guess. When unsure of a cell's API, run `soma describe --faces`. --- ## More verified footguns (found generating 168 programs) ## 11. Your handler shadows a builtin of the same name — when the argument count matches `f(args)` calls the program's handler `f` if one takes that many arguments, the builtin `f` otherwise. User code shadows the library, as everywhere else. ```soma on merge(a: Int, b: Int) { return a + b + 1000 } on use_it() { return merge(1, 2) } // 1003 — your handler on list() { return list(1, 2) } // [1, 2] — 2 ≠ 0 arguments: the builtin ``` `soma check` warns on the two confusing cases: ```soma on merge(a: Int, b: Int, c: Int) { … } on use_it() { return merge(m1, m2) } // warning: call to 'merge' with 2 argument(s) … resolves to the BUILTIN merge(): // the handler G.merge takes [3] on list() { let items = list() … } // warning: inside G.list, `list(…)` with 0 argument(s) calls the handler ITSELF // (recursion), not the builtin list(). For an empty list write [] ``` Method calls (`xs.count(p)`) always go to builtins. ## 12. `assert_fails` needs an expression that RAISES, not a falsy bool ```soma assert_fails 1 == 2 // FAILS the test: 1==2 is just `false`, no error ``` ```soma assert_fails xs[99] // passes: out-of-bounds RAISES assert_fails transition(id, "illegal") // passes: invalid transition raises assert !(1 == 2) // for a falsy predicate, use plain assert + ! ``` ## 13. Slot methods work on declared `memory` slots, not local maps ```soma let seen = map() seen.set("k", 1) // error: `.set()` is a memory-slot method and 'seen' is a local — a local map is written with brackets: `seen[k] = v` ``` ```soma let seen = map() seen["k"] = 1 // local maps use bracket indexing let v = seen["k"] ?? 0 ``` `.get`/`.set`/`.has`/`.delete`/`.keys` are for `memory { slot: ... }` slots. ## 14. `on` is a reserved keyword It can't be a parameter name or a map field read as `.on`. Use `enabled`, `active`, etc. ## 15. No semicolons; statements are newline-separated ```soma { a = 1; b = 2 } // error: unexpected character ';' — Soma has no semicolons, one statement per line ``` ```soma { a = 1 b = 2 } ``` ## 16. `given` is reserved (like `on`) It's a face-declaration keyword — can't be a state name, param, or identifier. `error: expected identifier, found Given`. Use `granted`, `input`, etc. ## 17. What a test cell's `rules { }` accepts `assert`, `assert_fails` (optionally `… matching "text"`), `let name = expr` (a fixture for the rules below), `mock think "reply"` / `mock think ["a", "b"]` / `mock think error "timeout"`, and `property`. No bare statements: put logic in a handler and call it. ## 18. One invariant, one slot An invariant is checked per write, with only the written slot in scope. ```soma memory { a: Map b: Map invariant a + b <= 100 } // error: memory invariant references several slots (a, b) — ... Write // one invariant per slot ``` `size` invariants are enforced on `delete` too: `invariant size >= 1` rejects removing the last entry. ## 19. `7 / 2 = 3.5` everywhere — say `idiv` when you mean the integer quotient `/` on two Ints is 3.5 (an Int only when exact) in the interpreter AND in `[native]` handlers. Native code is statically typed, so where the quotient must be an Int it is checked instead of truncated: ```soma on mid(lo: Int, hi: Int) [native] { let m = lo m = (lo + hi) / 2 // m is an Int slot return m } // mid(1, 2) → error: Int / Int is not exact here, and this spot can only // hold an Int (7 / 2 is 3.5) — write idiv(a, b) ... ``` ```soma on mid(lo: Int, hi: Int) [native] { return idiv(lo + hi, 2) } // 1, everywhere ``` `soma check` warns on Int / Int in native handlers; `soma fix f.cell --native-idiv` rewrites them (for code written when native `/` truncated). A `[native]` division by zero is an ordinary, `try`-catchable runtime error. ## 20. A cost bound is only *proven* when every `think()` count is known `think()` reached through a loop over a list, a lambda (`map(xs, x => think(..))`) or a recursive helper makes the bound unprovable — and an unprovable declared bound is a `soma check` **error** (the message reads `cost: 'tokens' bound is advisory — …`, exit 1), not a note: a bound nobody can prove is a lie in the program's own words. Give the loop a literal `range(0, N)` or `[loop_bound(N)]` to get `bound proven` back, or remove the `cost` block. Calls to sibling handlers are composed: `for i in range(0, 3) { helper() }` costs 3 × helper. ## 21. Habits from Python / TypeScript that `soma check` now redirects ```soma if x == null { } // error: 'null' does not exist — Soma's null is `()`; also `x ?? default` xs.includes(v) // error: no method 'includes' — in Soma: contains(xs, v) rows.push(o) // warning: result discarded — push returns a NEW list: rows = push(rows, o) [a[0]] + rest // warning: `+` ADDS numeric lists element-wise — concat(a, b) / push(xs, x) let t = lefft + 1 // error: undefined variable 'lefft' (did you mean 'left'?) ``` Everyday collection builtins: `contains(list|map|string, x)`, `slice(xs, start, end?)` (negative indexes count from the end), `keys(m)` / `values(m)` / `entries(m)`, `sort_by(rows, "field")` or `sort_by(rows, r => [0 - r.total, r.name], "desc"?)` (stable; a list key sorts on several keys), `round(x, digits)`. ## 22. Transition guards see the calling handler's locals ```soma state expense { initial: approved approved -> paid { guard { amount < 10000 } } } on pay(id: String) { let amount = amounts.get(id) ?? 0 // the guard reads THIS `amount` transition(id, "paid") // raises "guard failed…" when false } ``` A guard sees: the locals of the handler calling `transition()`, the cell's memory slots, `_id`, `_from`, `_to`. `soma check` rejects a guard that reads a name its calling handler never binds. Guards are enforced at runtime; the model checker keeps the edge (an over-approximation, so safety results hold). ## 23. `soma.toml` is validated A `soma.toml` that does not parse — or has an unknown key under `[verify]` — is an error for every command (it used to be ignored silently, so `[verify]` properties were never checked). `[package]` is optional. ## 24. Handlers are atomic; errors have kinds A handler that raises leaves nothing behind: its writes and transitions are rolled back (a failing `try { }` block too, to where it began). Do not write compensation code. Raise with `fail("kind", "detail")` or `require cond else Tag`; catch with `let r = try { … }` and branch on `r.kind` (`"not_found"`, `"invalid_transition"`, `"guard_failed"`, `"invariant"`, …); `fail(r)` re-raises. ## 25. `* -> failed` leaves EVERY state, final ones included ```soma state s { initial: a a -> paid * -> failed } // paid -> failed exists: paid is not final state s { initial: a a -> paid * -> failed except [paid] } // paid stays final ``` `soma verify` warns about the first form and prints the second. ## 26. A route in `request` and a handler of the same name `soma serve` exposes every public handler at `//`. With `on hold(id, qty)` and a route `"/hold/" + id`, the explicit route wins — but other `/hold/…` shapes still reach the handler. Prefix internal handlers with `_`. `soma check` warns.