§3. Type system

Markdown Open in ChatGPT Open in Claude

Generated from docs/LANGUAGE.md §3. This is the normative specification; for a guided tour see the Language and Neurosymbolic sections.

3.1 Base types, collections, and core expressions

Scalars int (arbitrary precision default; i8..i64, f16/f32/f64 sized forms), bool, str, bytes; algebraic data: struct, enum (sum types with payloads; declaration and destructuring in §3.9), tuples (tuple[T, U], literal (a, b), destructured by irrefutable patterns, §5.13); generics with inference; Option[T] and Result[T, E] in the prelude — there is no null. Option values are written Some(x) and None; Result values are written Ok(x) and Err(e) (§5.20). None is the empty variant of a sum type, never a null reference — it is consumed by match, by the combinators, or by ?/unwrap (§5.20), not by identity tests. Static typing throughout with local inference; the Codon divergence list applies (no monkey-patching, no dynamic member addition).

Numerics. The default int/Int/ZZ domain is a signed arbitrary-precision integer with an i64 fast representation and automatic promotion. Exact work is governed by a 16,384-bit resource ceiling; exceeding it is ResourceLimit, not machine overflow or a silent wrap. Source literals admit at most 4,300 decimal digits, while the tagged wire path admits the derived 4,933 digits needed to round-trip every runtime value. Integer +/-/*/powers/shifts/bitwise operations remain exact. Integer / computes the exact rational quotient before one checked rounding to finite f64; // is floor division (toward negative infinity) and % uses the divisor’s sign, so for every nonzero integer b, a == (a // b) * b + (a % b) as in Python. Division/modulo by zero, non-real powers, and non-finite results raise typed errors rather than returning NaN/inf. Mixed finite integer/float comparisons use exact binary-rational comparison instead of rounding the integer through f64; conversions and fixed-width narrowing remain explicit constructors.

Width casts round through the real format, so a sized type is observable, not cosmetic:

Floats: f32(x), f16(x), bf16(x), f8(x) round x through IEEE binary32 / binary16 / bfloat16 / FP8-E4M3 respectively — f16(0.1) != 0.1, f8(1000.0) == 448.0 (saturates), bf16 keeps f32’s range but 7 mantissa bits. This is the quantization behavior ML code needs, native.
Integers: i8(x), i16(x), i32(x), i64(x), u8(x), u16(x), u32(x), and u64(x) are explicit narrowing conversions with two’s-complement wrap (like a systems as iN): i8(200) == -56, u8(300) == 44. int/Int/ZZ construct the arbitrary-precision domain; fixed-width annotations are not yet retained as distinct runtime value types.

String methods (a str.method() surface): upper/lower/strip/lstrip/rstrip, split/join/replace, startswith/endswith/contains, find/rfind (char index or -1)/count, slice/substring, capitalize/title, isdigit/isalpha/isalnum/ isspace, repeat, len.

Static type checking. sema check verifies types before the program runs — call arity (too many / too few arguments), struct construction (unknown field names), a literal argument whose base type conflicts with a declared parameter (add(1, "two") where add wants two ints), a return whose base type conflicts with the declared return, and trait-object conformance (§3.9): an evident concrete type placed in a trait slot it does not conform to — a Blob in a list[Shape] argument or Shape-typed binding, or a non-Ord value passed where [T: Ord] is required. The checker is conservative by design: it only flags a mismatch when it can resolve a concrete type on both sides, so generative outputs (simulate), ported functions, extern helpers, untyped locals, and generics are left alone (typed any), and int/float interoperate. It is a whole-project pass (a function typed in one module is checked at its call sites in another), grown incrementally toward full local inference — the linter a type system would give you, today, with zero false positives on the example corpus.

Runtime call boundary. An ordinary def binds positional arguments, keyword arguments, defaults, *args, and **kwargs before executing its body. Supported concrete annotations are checked at entry and return (including lossless int to f64 widening), while erased generic and function annotations remain governed by their documented static semantics. A missing name, unknown method or namespace member, non-callable value, arity mismatch, invalid annotation, effect-row violation, or contract failure terminates with a typed error; none is converted to a stub, None, or a no-op. Selecting the bytecode VM preserves the tree-walker’s value, error kind/message, source span, and call-frame trace for these boundaries.

Conditional expression. then if cond else else_ is an expression (only the taken branch is evaluated). It sits below every binary operator and above lambda/=> in precedence, and its else branch is right-associative so it chains: a if p else b if q else c. It is the concise form default trait methods lean on (§3.9); the statement if is §5.13.

Collections. list[T], dict[K, V], and set[T] are built in, homogeneous, and value-semantic (§3.8). Literals and comprehensions are Pythonic: [x for x in xs if p(x)], {k: v for ...}, {x for ...}; a comprehension is the sequential base case of the parallel [...] form (§5.17) with identical scoping and typing rules. Slices on list/str/bytes use Python syntax and return copies. Dict keys and set elements require types that are hashable with total ==. Heterogeneous collections remain excluded (Codon divergence list); dynamic JSON-shaped data enters through the prelude JsonValue sum and leaves it at a typed boundary (parse[T] against a struct schema with field contracts — §3.4, §5.22), never via stringly subscripting. For canonical flattening (§3.2), dict and set flatten in sorted key/element order so embeddings and replay are order-independent.

Iteration. The Iterable trait (§3.9) is the single iteration protocol: iter() returns an Iterator[T] whose next() returns Option[T]. for x in xs:, comprehensions, parallel and stream consumption both take Iterable operands; Stream[T] (§5.25) implements it with bounded-queue backpressure, so for incident in stream: is the consumption form. Generator functions (stream def bodies with yield, §5.25) are the lazy-producer surface; D39 resolves the Q10 deferral by making frames affine and pulls journal-ordered.

Function types. Functions and lambdas are first-class values. The function type is written (T, U) -> R !{row}; the effect row is part of the type, so a parameter of function type declares the effects its callee may perform — a higher-order function cannot smuggle effects its own row does not admit. coerce by, provide factories, and reducer arguments are ordinary function-typed values.

Statements. Retained Python statement forms: if/elif/else, while, for ... in, break, continue, return, pass, match. There is no assert — the token is reserved and rejected with a machine-applicable fix-it to ensure/check, whose statement-position forms are the assertion vocabulary, semantic assertions included (§5.4) — and no try/raise (failures are typed values, §5.20). Blocks introduce no new scope (Python binding rules); bindings made inside if/expect arms are visible after the block. The one exception is with <expr> as x: (§5.21): the as-binding is scoped to its block — the handle is affine and released at scope exit, so it cannot be referenced afterwards.

Prelude type commitments. The following types are language-adjacent and committed in the prelude, not user code: Path, Duration (durations in budget/restart/heal clauses are quoted duration literals — "2s", "50ms" — parsed at compile time), Instant (returned by clock.now()), JsonValue, Tensor[T], Atomic[T], Mutex[T], Task[T] (§5.12), Stream[T]/Window[T] (§5.25), DebugSnapshot (§5.26), and the structured logging/console surface (log.*, print, alert — typed prelude events with normative routing, masking, and level semantics, §5.27). Their full APIs live in the stdlib reference, not this spec.

3.2 Semantic values and canonical flattening

Every value of a type implementing the Semantic protocol carries a lazily computed, cached embedding alongside its exact representation (BRIEF §3.1; lineage: SymbolicAI’s Symbol.embedding, 01 §9). Semantic is a trait (§3.9; this document previously called it a “protocol” — that word now exclusively means session types, §5.12). str implements it natively; Sema structs and enums derive it via canonical flattening unless the author explicitly opts out (enums flatten as descriptor

variant name + flattened payload, so categorical values are comparable and monitorable): a deterministic, compiler-generated rendering flatten(v) -> str of descriptors, field names, and field values, stable across runs and recorded in the ABI so embeddings are comparable across builds. FFI/opaque values need adapters before they become Semantic.

Embedding computation is tiered: default tier is an always-resident static-embedding model (~30 MB, hot-loop viable at ~40 µs/sentence CPU); escalation to a transformer embedder is explicit or scheduler-driven (06). The tier is part of the judge identity (§3.3).
Because ~= sites are compiler-visible IR operations, the optimizer may hoist embeddings out of loops, batch cold misses, and pre-embed string literals into the binary (06) — an optimization no library can perform (01 §14.6).
Embeddings never change observable semantics except through the graded operators of §5.1.

struct Article:
    sem "A news article ingested from a feed"
    title: str sem "Article headline as published by the source"
    body: str sem "Full article body text"
    source: str sem "Publisher or feed identity"

# a.embedding is lazy, cached, content-hash interned; flatten(a) is the canonical text.

Inline field descriptors are first-class syntax, not comments. They become part of canonical flattening, generated schemas, contract diagnostics, constrained decoding, and self-repair context. Long descriptors may still be declared out of line with sem Type.field = "...".

3.3 Graded similarity: the `Sim` type

a ~= b does not return bool. It returns a Sim value:

struct Sim:
    score: f32              # in [0, 1], metric-normalized
    judge: JudgeId          # full judge identity, see below
    calibration: Option[CalibrationId]   # named calibration set, if any

JudgeId is the complete identity tuple (model hash, prompt/template hash, decode + seed policy, metric + embedding tier) — THEORY.md Axiom J; a decision site’s static type additionally carries (calibration-set id, threshold τ, α). Any component change is a semver-major change to program semantics. Sim is the only graded-truth carrier; where a graded value travels with its subject, the pair is written (T, Sim) — there is no separate Scored[T] type, and foreign projections (INTEROP.md’s sema.Graded) are lowerings of Sim plus the site’s (τ, α).

Sim is the single graded-truth substrate: ~= scores, contract check results, and semantics() scores all inhabit it, so thresholding, evidence reporting, and the guarantee map treat them uniformly (BAML’s @check-as-metadata generalized, 04 §2.2).

Coercion to control flow is explicit or calibrated, never silent:

if a ~= b: is legal only when the comparison’s judge carries a calibration (threshold chosen by conformal risk control / Learn-then-Test with declared α — arXiv:2208.02814, arXiv:2110.01052); the guarded region types as statistical(α).
if (a ~= b).score > 0.9: is always legal but the region types as best_effort unless the literal threshold is itself certified against a calibration set.
Uncalibrated judges compile with a warning and type as best_effort; they cannot guard proved or checked regions (05 §6.2).
The if rule generalizes to every boolean coercion context — while conditions, boolean operands, and a bool-returning position such as return semantics(...): a calibrated verdict coerces with the enclosing region (and, through the signature’s guarantee status, the caller’s view of the result) typed statistical(α); an uncalibrated coercion in any of these positions is a compile error, not a silent downgrade.
Boolean conjunction/disjunction of calibrated guards composes by union bound: a region guarded by two calibrated coercions types statistical(α₁ + α₂). Chains that would push the summed α past the site’s declared budget are compile errors.

Default-judge honesty (THEORY.md honesty clause). The prelude’s default judge ships uncalibrated: ~= under it types best_effort until a named, domain-applicable calibration set is bound (package- or module-level binding). Corpus examples that annotate statistical(α) on default-judge sites assume such a binding is in force.

Non-properties, stated in the spec: ~= is reflexive and symmetric by construction, but not transitive — it is similarity, not equivalence (05 §5 guarantee map). Chained rewriting that assumes transitivity is a compile-time error.

Rejected alternative: full provenance-semiring propagation of graded truth through all control flow (Scallop, arXiv:2304.04812) — the most principled published semantics, but it globalizes cost and complexity onto every branch; Sema thresholds at the branch with typed obligations instead, and keeps semirings as the candidate formalism for a future graded region feature (Open question Q2).

3.4 Semantic descriptors and boundary contracts

Every public data boundary is also a contract boundary. sem is the descriptor form for human meaning at every useful granularity: field, struct, function, operator, bridge export, and long out-of-line declarations. Descriptors are not comments. They feed canonical flattening, constrained emission, contract diagnostics, stack traces, policy decisions, monitor channels, and self-repair context.

A field declaration may carry a semantic descriptor, a deterministic refinement, and an optional normalizer:

struct IntakeProfile:
    age: int sem "Human age in whole years; accepts numerals or spelled-out English" where 0 <= value <= 130 coerce by parse_age

sem is the field’s natural-language meaning. where is checked over value after parsing or coercion. coerce by names a normalizer that may turn boundary data such as "I am seventeen" into the declared representation before validation. Field contracts are also the R2 stage of the decode-and-repair ladder (§5.22). A failed field contract produces a typed ContractViolation carrying field path, descriptor, raw value, normalized value if any, blame party, and stack trace. In supervised code the runtime can retry or repair the normalizer, but the invalid value is still typed as failed and cannot flow onward.

Struct-level sem describes the object as a whole. It participates in canonical flattening before field descriptors, and struct-level check semantics(...) clauses validate holistic coherence after all fields pass their deterministic contracts:

struct LocaleProfile:
    sem "Locale-routing profile; never a protected-class decision"
    display_name: str sem "User supplied display name"
    languages: list[str] sem "Languages the user can read"
    region_hint: str sem "Non-authoritative region hint for content localization"
    check semantics("region_hint is supported by languages and other profile fields",
                    self, alpha=0.02)

Function and operator sem descriptors describe intent at call boundaries. When a boundary fails, the diagnostic contains the failed field path, enclosing struct descriptor, callable descriptor, policy envelope, semantic predicate, evidence, and stack trace. This is the native join-point where aspect-style validation happens, but as typed language semantics rather than decorator convention.

Sensitive inferences, such as protected demographic classification from names or language signals, are not ordinary validators. They require an explicit policy grant and may not feed access, pricing, employment, medical, legal, or other adverse decisions unless the policy and domain law allow it. Sema can express such checks, but the default prelude treats them as policy-sensitive semantics(...) sites, not harmless class-level traits.

3.5 Trust labels (information flow)

Every value carries a trust label from the lattice untrusted < validated < trusted (FIDES-style product of integrity with type, arXiv:2505.23643; 08). Sources are language constructs, so labeling is nearly annotation-free: simulate outputs, network/file reads, and FFI returns are born untrusted; string literals and pure computation over trusted inputs are trusted. Sinks (code.exec, proc.spawn, SQL identifiers/fragments, tool dispatch, ported splice-in) require trusted.

The lattice is ordered by trust: untrusted is bottom. Propagation takes the meet — any value computed from mixed inputs carries the least trusted label among them, so taint is sticky and no combination of operations can launder a label upward. Endorsement is the only upward move, and it has exactly two doors: passing contracts / sound verifiers (→ validated), or the audited human-approval effect human.approve (→ trusted). A statistical verifier (calibrated judge, semantics() pass) can never endorse above validated — no error bound converts a statistical verdict into trusted. Explicit endorsement sites use the endorse operation, which is itself policy-gated and journaled; capability values (Cap[R]), narrowing, and one-shot grants are specified operationally in GOVERNANCE.md §6 and defer to this section for the lattice and doors. Some sinks accept validated; code.exec never does without an explicit policy grant. This is the type-level mechanism behind BRIEF §3.5’s “a prompt-injected simulate can emit text but nothing it produces can ever run.”

3.6 Effects and capabilities

Sema types effects in rows on function signatures, Koka-style (Leijen, POPL 2017; 05 §3.3). This list is the one canonical effect vocabulary for the whole doc set (GOVERNANCE.md §3 mirrors it and defers here):

model.invoke  model.embed   model.load
fs.read       fs.write      net.connect     net.listen
proc.spawn    code.gen      code.exec       code.patch
db.read       db.write      db.schema
clock         random        ffi.call        memory.query   memory.retain
env.read      config.reload config.watch    observe.record observe.export
event.emit    event.subscribe
policy.change package.install  ui.render    human.approve

Effect instances are parameterized with parentheses — net.connect("api.internal:443"), fs.read("data/**") — and policies match on instances (§5.8). Colon-namespaced spellings (net:model-egress) and bare namespace aliases (model for model.invoke) are illegal; the legacy bare-model alias is a compile error. human.approve is the audited human-approval effect that endorsement to trusted requires (§3.5); policy.change is the distinguished policy-mutation effect (§5.8); event.emit/event.subscribe belong to the event system (§5.19; event.subscribe is reserved for dynamic subscription, Q12).

A function typed def f(x: int) -> int !{} provably performs no model calls, no I/O — the deterministic core is a type-enforced sublanguage, not a convention.
policy (§5.8) grants and confines capabilities; capture checking (Capturing Types, TOPLAS 2023) makes confinement transitive over closures: a closure created under a no-code.exec policy stays code.exec-free even when invoked elsewhere.
The runtime is an effect-handler stack: record/replay, mocking, batching, and policy enforcement are all handlers over these operations (05 §3.3; Pyro Poutines precedent, arXiv:1810.09538).

An omitted row is inferred, never a wildcard. Writing no !{...} does not grant ambient authority — it asks the compiler to infer the minimal row from the body (Koka-style), which is fail-closed: a function that touches nothing infers !{}. Authority is always conspicuous, never the silent default (object-capability discipline; unsafe-style opt-in). Two rules make this enforceable rather than aspirational:

assure silver+ requires an explicit row on every declared function (sema check errors otherwise). Inference stays an assure bronze ergonomic; the published surface — the verification cache key (§3.4) and the caller contract — must state the row so a later code.exec shows up as a signature diff, not a silent change. Exempt because their row is derived elsewhere: simulate/by model-backed defs (§5.22), ported def ... from ports (INTEROP), and provide (no row slot, §5.15).
!{*} is the explicit all-effects top (⊤) — a loud, greppable escape hatch for spikes and REPL work, not the meaning of silence. sema check warns on it at bronze and errors at silver+, and the runtime refuses to admit a !{*} row under any policy that forbids or bounds capability (it runs only under an unrestricting policy stack). Do not confuse it with the useful star: an effect row variable !e for effect-polymorphic higher-order code (map(f: (A) -> B !e) -> list[B] !e — “map has whatever effects f has”), which is parametric and precise. The row-variable form is reserved for a later revision; !{*} is concrete ⊤, the least informative row.

Calling an operation is checked; declaring a capability is open. An effect row may name any capability (!{fs.raed} parses — rows are extensible). But calling an operation resolves like any builtin: a call to an unrecognized op (fs.raed("x"), json.pares(...)) raises NameError at the call site rather than silently journaling an effect and returning None. Each effect namespace (fs, net, code, proc, observe, memory, event, env, config, package, ui) has a recognized callable surface that is a superset of its canonical vocabulary above, and the fixed-op library namespaces (json, csv, http, sql, monitors) likewise reject unknown ops. Intentionally dynamic namespaces (log by level, tools/mcp/skills/stream by name) stay open by design. Typos are caught, not swallowed.

Statement position is likewise guarded: the permissive parser accepts an unknown word …: as an inert directive (the tier-0 declarative-config escape), so a typo (esnure false) or a misplaced suite clause (allow: inside a def) would parse and do nothing. sema check warns on any directive in a def/simulate body that no runtime handler recognizes, so these silent no-ops surface at check time without closing the open design.

Custom capabilities — the row vocabulary is open. The catalog above is the built-in vocabulary, not a closed set: a row may declare namespaces the runtime has never heard of — !{mysql.query} parses, is containment-checked, and is journaled like any built-in path. A custom effect is a marker: there is no namespace object behind it (mysql.query(...) in a body is a NameError at the call site), so the way to mint one is the wrapper-module pattern — a connector module whose public defs carry the custom effect plus the real underlying effects they exercise. Callers then transitively need BOTH labels: sema check rejects an uncontained caller (call to payments_read requires undeclared effect(s) payments.read), the runtime denies a call whose active row lacks the label, and a policy can deny either the domain label or the underlying capability by path, with scoped instances load-verified like any other rule (§5.8).

# payments.sema — the connector module is the only place the label is minted.
def payments_read(account: str) -> list[dict] !{payments.read, db.read}:
    return db.query("SELECT amount, account FROM payments WHERE account = ?", [account])

# main.sema
from payments import payments_read

policy NoPaymentReads:
    forbid cap:
        payments.read
    justification "auditors may not touch payment rows in this scope"

def audit_exposure(account: str) -> int !{payments.read, db.read}:
    return len(payments_read(account))

def main() -> None !{payments.read, db.read, db.write, observe.record, ui.render}:
    db.exec("CREATE TABLE IF NOT EXISTS payments (account TEXT, amount REAL)")
    db.insert("payments", {"account": "acct-1", "amount": 12.5})
    log.info("payments visible", rows=audit_exposure("acct-1"))
    with policy(NoPaymentReads):
        expect n = audit_exposure("acct-1"):
            log.info("policy failed to bite", rows=n)
        except Denied as d:
            # "policy NoPaymentReads denies effect payments.read in
            #  audit_exposure(): forbidden capability"
            log.info("denied as designed", why=d.message)

Two honest boundaries. First, effect vocabulary is authority labeling, not OS-level confinement: payments.read gates payment rows only because the wrapper module is the sole minting site — a function holding plain fs.write cannot be prevented from touching database files by effect kind alone. Keep the underlying capability behind scoped instances (fs.read("data/**"), the db.* surface behind the wrapper) and let governance postures and the OS sandbox (GOVERNANCE.md) carry the confinement that labels cannot. Second, typos vs. vocabulary: sema check lints near-misses of the built-in namespaces in a row (!{fss.read} → “did you mean fs?”), while genuinely distinct custom names are intentional and stay clean — mysql.query is vocabulary, fss.read is a typo.

These operations are real, not mocked. path.* is real path algebra (join/basename/dirname/extension/stem/normalize/…); fs.* reads, writes, appends, lists, copies, and removes real files under the project root; env.* reads/writes the real process environment; memory.* is a real per-run key/value store; proc.* and code.exec run real subprocesses and return {stdout, stderr, code}; code.patch edits files; net.* performs real HTTP over the standard library (plain http://; https:// needs a TLS build and errors clearly otherwise); db.* is a real in-process table store (insert/query/count); ui.* is real terminal I/O. Two operations are deliberate rather than stubbed: observe.* records to the run journal (that is the telemetry sink), and clock.now returns a fixed epoch so runs are reproducible and the VM and interpreter agree — real wall time is clock.wall_ms/ clock.wall_s/clock.mono_ms. Every effect is still journaled, and policy gating (§5.8) applies at the function’s effect row plus, for net, per endpoint.

net.* performs real HTTP and HTTPS (a bundled rustls TLS stack — no system library to install). net.get/post/put/patch/delete return the response body; every form takes an optional trailing options dict exposing all the HTTP knobs — headers (a dict), bearer (token) or auth (a raw Authorization value), query (a dict of params), timeout_ms, retries (with retry_backoff_ms, linear backoff on transport failures), and redirects (max redirects to follow; 0 returns the 3xx without following). net.request({url, method, …}) and net.fetch(url, {…}) return the full response {status, headers, body}. For example:

r = net.fetch("https://api.example.com/v1/items", {
    headers:  {"Accept": "application/json"},
    bearer:   secrets.token,
    query:    {"limit": "50"},
    timeout_ms: 15000,
    retries:  3,
    retry_backoff_ms: 250,
    redirects: 5,
})
# r.status, r.headers, r.body

db.* is a real embedded SQLite database by default (compiled from source, no server): db.exec(sql[, params]) runs statements, db.query/db.read(sql[, params]) return rows as dicts, db.insert(table, row) and db.count(table) are conveniences, with ? placeholders bound from a list. The database lives at <project>/.sema/db.sqlite — or wherever [db] path in sema.toml points.

The SQL backend is replaceable — by config or by a provider. A DSN in sema.toml selects the built-in SQLite location: [db] url = "sqlite:///data/app.db", "sqlite://:memory:" (ephemeral), or [db] path = "…". A non-SQLite DSN (postgres://…) is not the built-in engine and errors with a pointer unless a provider is registered.

To use a different server, register a @provides("db") provider (§5.52) — a Sema function def backend(op: str, sql: str, params: list) -> any. Every db.* call is normalized to (op, sql, params) and routed there, so you bring your own database without touching Rust. Reads return a list[dict]; writes return the row count. A ready Postgres backend over the Python bridge (psycopg) — copy this in:

import python

@provides("db")
def postgres(op: str, sql: str, params: list) -> any !{net.connect}:
    dsn = config.get("db.url")                       # e.g. postgres://user@host/app
    return python.call("psycopg_bridge", "run", [dsn, op, sql, params])

where psycopg_bridge.py is a few lines: run(dsn, op, sql, params) opens psycopg.connect(dsn), executes sql with params, and returns cur.fetchall() as dicts for reads (op in {"query","read","select"}) or cur.rowcount for writes. MySQL is the same shape with mysql.connector. Because the contract is just (op, sql, params) -> rows|count, any driver — native binding, HTTP database, or Python — plugs in identically.

Usage and spend are ambient, not threaded. with meter as u: accumulates every model call’s usage within the block into u — u.total_calls, u.prompt_tokens, u.completion_tokens, u.total_tokens, and u.cost (priced from [pricing] per_token). No (result, usage) tuples to thread. with budget(tokens=N, calls=M) as b: is a meter with a hard cap: a model call that pushes spend past the cap raises BudgetExceeded rather than silently overspending. Meters and budgets nest; each call attributes to all enclosing frames.

with meter as u:
    answer = write_report(facts)          # returns the value only
log.info("run", tokens=u.total_tokens, cost=u.cost, calls=u.total_calls)

with budget(calls=200, tokens=1_000_000) as b:
    research = deep_search(query)          # BudgetExceeded if it overspends

Certified totality — ensure total (D129). Koka’s ladder distinguishes pure (<div,exc>: no side effects, may diverge or raise) from total (a mathematical function). Sema’s !{} is the pure analogue: no capability operations, but divergence and typed errors remain possible. The total tier is claimed with a signature contract — no new keyword, the claim vocabulary is contracts (§5.4), exactly like ensure semantics(...):

def mean_floor(xs: list[int]) -> int !{}:
    require len(xs) > 0
    ensure total
    return sum(xs) // len(xs)

The claim reads: for every argument satisfying the require clauses, evaluation terminates and produces a value of the return type. require clauses are domain refinements, not exceptions — mean_floor is total on {xs : list[int] | len(xs) > 0}. The claim is verified statically by sema check AND at module registration before any def can run (sema run rejects exactly what check rejects); an unprovable claim is a loud error, never a silent acceptance. A verified clause is statically discharged: it never evaluates at runtime (total is not a value), and a claim reaching execution from an unverified path — a REPL fragment, a live patch — fails closed with a typed error. Hot-swapping any def in a module (§5.11 live heal) drops the module’s verified status: a sibling’s totality proof may depend on the patched body, so its next claimed call fails closed rather than trusting a stale proof, and a patch may not itself claim ensure total.

The verified v1 fragment is exact arithmetic — where the mathematical claim is actually provable:

Signatures: every parameter and the return are annotated with exact types — arbitrary-precision int, bool, str, exact collections (list/tuple/dict/set over exact types), and user structs/enums whose fields are recursively exact. Floats are excluded: Sema floats raise typed errors on non-finite results (§ Numerics), so even + is partial there. The effect row must be the explicit !{}.
Termination: while is rejected; loop until requires max_iters; for/comprehension iterables must be provably finite (literals, range, exact-collection parameters, locals only ever bound to finite collections, a total callee’s collection result); recursion — self or mutual — is rejected (no termination measures yet; rewrite iteratively).
Partiality discharge: // and % need a nonzero-literal divisor or a require fact (require len(xs) > 0 licenses // len(xs)); ** and shifts need a non-negative right operand the same way; sequence indexing needs require i >= 0 and require i < len(xs), dict subscripts require k in d. Facts discharge by normalized AST equality over names never assigned in the body, and the whitelisted mutating methods (append, dict insertion) are fact-monotone — they can only grow len and add keys — so a discharged fact cannot be invalidated behind the guard’s back. / is rejected even on ints: it computes the exact rational and rounds through f64, which can raise on non-finite results.
Callees: other ensure total defs in the module, module equations whose bodies stay in the exact math fragment (finite Σ/Π, polynomial arithmetic, nonzero-literal division — CAS constructs like lim, ∫, derivatives, and symbolic variables are rejected: their kernels carry typed non-convergence outcomes), and a curated builtin whitelist (len, abs, range, sum, bool, str, repr; n-ary min/max). Higher-order values are rejected — effect-row polymorphism is the documented gap.

What total does not claim, stated exactly: ResourceLimit and memory exhaustion are operational faults outside the semantic claim (the same status they have in every proof assistant’s extracted code); ensure postconditions on a total def remain runtime-checked (a failure reports a bug, it is not admitted partiality); and dynamic type errors inside bodies are the static type checker’s dimension, progressively closed as it grows. sema doc renders a Total badge only after re-running the verifier — intent is never rendered as proof. Widening the fragment — termination measures for recursion, exact QQ division under nonzero facts, float totality via interval analysis, Lean-certified escape hatches for programs outside the decidable fragment — is target spec, tracked in the D-log.

3.7 The gradual guarantee lattice

Every obligation (type, contract clause, semantic predicate, policy conformance) has a status in the extended gradual-verification lattice:

proved  >  checked  >  statistical(α)  >  best_effort  >  unchecked

proved = discharged statically (types, SMT refinements, capability reachability); checked = sound runtime check inserted with blame; statistical(α) = calibrated conformal/e-process bound under exchangeability; best_effort = evaluated but unbounded; unchecked = visible hole. The compiler inserts checks at region boundaries with blame-carrying labels naming the generative call at fault (gradual verification lineage: Bader/Aldrich/Tanter VMCAI 2018, Gradual C0, POPL 2024). The statistical(α) point is new metatheory Sema must own (05 §6.10).

Language rule: a statistical(α) obligation requires an active monitor on its input stream; without one it decays to best_effort at the type level (05 §6.7). The certificate is honest only while the deployment distribution matches calibration, and monitor is what guards that assumption. The rule applies per calibrated decision site — every calibrated ~= branch and semantics() guard, not only simulate outputs. Where no explicit monitor declaration covers a site’s input stream, the compiler derives one (§5.9, Decision record D15); a site the compiler cannot cover decays to best_effort with a diagnostic naming the missing monitor.

3.8 Bindings, mutability, and value semantics

Bindings are immutable by default; mut x = ... declares a rebindable binding whose aggregate contents may be mutated in place. Assignment to a plain binding is a compile error; every binding is monomorphic (one type for its lifetime — rebinding cannot change type). Structs and collections are value-semantic: assignment and argument passing denote the value, not a shared alias, and the compiler is free to copy-on-write. There is no observable aliasing of mutable data outside the explicit shared-state types (Atomic[T], Mutex[T]), which is what makes the §5.17 capture rule and the no-GIL runtime sound; the same capture rule applies verbatim to scope/spawn closures (§5.12), not only to parallel lambdas.

Mutation interacts with the rest of the semantics in three fixed ways:

Contracts. A struct invariant is re-checked at every mutation of a guarded field through a mut binding and at every boundary crossing — an aggregate can never be observed with a violated invariant.
Trust. Writing a field re-labels the aggregate with the meet of its old label and the written value’s label (§3.5) — mutation can only lower trust, never launder it.
Constants. Module-level plain bindings of literal or pure-!{} initializers are compile-time constants (Money.zero is this pattern via trait statics, §3.9).

The prelude state module (used by the worked example, §7) is an ordinary checkpoint store over fs.read/fs.write effects — not hidden language magic.

3.9 Methods, traits, and conformance

struct and enum bodies admit def (with contracts, effect rows, descriptors) — methods are ordinary functions with an implicit typed self; mut def marks methods that mutate self and is legal only through mut bindings (§3.8). Associated constants (Money.zero) are def-less bindings in the type body.

A trait declares required signatures (bodyless defs), optional default methods (defs with a body), and laws as contracts, which makes trait obligations first-class verification targets (§5.7) rather than documentation:

trait Mergeable:
    sem "Types with an associative combine, safe for unordered parallel reduction"
    def combine(self, other: Self) -> Self !{}                     # required
    law associative: combine(combine(a, b), c) == combine(a, combine(b, c))

struct Money (Mergeable, Semantic):
    currency: Currency
    minor_units: i64
    def combine(self, other: Money) -> Money !{}:
        require self.currency == other.currency
        return Money(currency=self.currency, minor_units=self.minor_units + other.minor_units)

Default (provided) methods. A trait method that carries a body is a default: it is written once and grafted onto every conforming type that does not override it (the type’s own definition always wins). This is Sema’s answer to implementation reuse — the legitimate core of what class inheritance is used for — without a class hierarchy. A single required method can seed an entire interface:

trait Eq:
    def eq(self, other: Self) -> bool

trait Ord (Eq):                                    # Eq is a *supertrait* of Ord
    def compare(self, other: Self) -> int          # the one required method
    def less(self, other: Self) -> bool:           # everything below is provided
        return self.compare(other) < 0
    def eq(self, other: Self) -> bool:             # satisfies the Eq obligation
        return self.compare(other) == 0
    def clamp(self, lo: Self, hi: Self) -> Self:
        return lo if self.less(lo) else (hi if hi.less(self) else self)

struct Ver (Ord):
    major: int
    def compare(self, other: Ver) -> int:          # supply `compare`, inherit the rest
        return self.major - other.major

Supertraits. trait Ord (Eq): declares that every Ord type is also an Eq type; the supertrait’s obligations flow down (a conformer must satisfy Eq’s required methods too, unless a default in the chain supplies them) and its defaults are available to Ord’s defaults. Supertrait sets meet transitively; cycles are rejected.

Bounded generics. A type parameter may name the traits it must satisfy: def maximum[T: Ord](xs: list[T]) -> T bounds T by Ord (multiple bounds join with +: [T: Eq + Ord]). Type parameters are erased at runtime (§5.29); the bound is the declared obligation — surfaced to sema check, reflection (§5.23), and docs — that lets the body use the bound traits’ surface and documents the contract to callers. The bound is enforced at call sites where the argument’s concrete type is evident — passing a Blob that does not conform to Ord to maximum is a sema check error (§3.1 type checker). It is not (in v0.1) discharged by monomorphization, so a bound on a value whose type the checker cannot resolve is left to runtime dispatch.

Trait objects (open-world polymorphism). A trait name used in type position — x: Shape, list[Shape], -> Shape — is a trait object type: any value conforming to the trait, dispatched by its runtime type. This is how you get a heterogeneous collection behind one interface (the thing class hierarchies use inheritance for), and it composes with everything else: third parties add new conformers without touching a central enum.

trait Renderer:
    def render(self) -> str
struct Text (Renderer):
    body: str
    def render(self) -> str: return self.body
struct Rule (Renderer):
    width: int
    def render(self) -> str: return "-" * self.width

def render_all(items: list[Renderer]) -> str !{}:    # one list, many concrete types
    return "\n".join([it.render() for it in items])  # dispatched dynamically

Method calls on a trait-object value resolve against the concrete runtime type (the same dispatch as x.method() everywhere); a call to a method the concrete type does not provide is a typed error at the call site. Because dispatch is by runtime type, no vtable or boxing is observable. Trait-object slots are conformance-checked (§3.1 type checker): a value whose concrete type is evident and does not conform — a Blob in a list[Shape] argument, a Shape-typed binding, or a -> Shape return — is a sema check error before the program runs. Closed-world alternatives — when the set of cases is fixed and you want exhaustiveness — remain enum + match (§5.13); trait objects are the open-world dual.

The is test. value is Type and value is not Type return bool: true iff the value’s runtime type is that concrete type, or conforms to that trait (transitively through supertraits). It is the narrowing/dispatch escape hatch for open-world code — n = n + (1 if it is Rule else 0) — and works on concrete types, traits, and built-in types (x is int). Identity comparison is meaningless under value semantics (§3.8), so is is repurposed as the type/conformance test.

Conformance is declared in the type header (struct X (TraitA, TraitB):) or out of line with impl Trait for Type: — the out-of-line form is how FFI/opaque values gain Semantic adapters (§3.2) and how prelude types conform retroactively. Conformance is checked (§5.7 static leg): a type that declares a user-defined trait but leaves a required method unimplemented — its own or a supertrait’s, and not covered by a default — is a hard sema check error naming the missing methods. Trait law clauses feed the L1 property engine: an unordered parallel reduce (§5.17) demands Mergeable with a killed-mutant record for associative, which is what “proved associative” concretely means. Core prelude traits: Semantic (embedding + canonical flattening), Iterable/Iterator (§3.1), Hashable, Eq/Ord, Mergeable. Blanket implementations and specialization are excluded from v0.1 (coherence: at most one impl per (trait, type) pair, orphan rule as in Rust).

Enum declarations and payloads. Standalone form with optional payloads:

enum Escalation:
    none
    notify(channel: str)
    page(oncall: str, deadline: Duration)

match esc:
    case Escalation.page(oncall, deadline): dispatch(oncall, deadline)
    case Escalation.notify(channel):        post(channel)
    case Escalation.none:                   pass

Variant payloads destructure positionally or by name in case patterns; enum match is exhaustiveness-checked (§5.13). The inline form (sentiment: enum Sentiment: pos | neg | neutral) remains sugar for a standalone payload-free declaration.