Mental Model

This is the page to hold onto. Everything else in Sema is an instance of one idea: a program has a deterministic core and a generative edge, and the language gives you one honest account of how much is guaranteed at every point between them. Understand this and the rest of the language reads as consequences.

Two regions, one language

Sema is designed on a single principle: probabilistic under the hood, deterministic at the boundary. Every construct has a nonempty deterministic guarantee — no Sema construct is purely statistical.

That splits a program conceptually into two regions:

• The deterministic core. Ordinary code — types, arithmetic, control flow, data — whose behavior is proved or checked. A function typed !{} provably performs no model calls and no I/O; it is a type-enforced sublanguage, not a convention.
• The generative edge. The places where a model is involved — a simulate def body written by a model, a semantic("…") predicate, the calibrated ~= operator. Here results are statistical: honest, graded, and carrying their evidence, never silently cast to a plain bool or str.

The two live in the same language and, crucially, share one verification story. There is no “model layer” bolted on outside a “code layer” — a model’s output and a proved property are labeled on the same lattice, and the compiler inserts checks at the boundary between them.

The !{} boundary: effects as types

The most concrete marker of the core/edge split is the effect row on every function signature. It lists the capabilities the function may use:

def normalize(x: str) -> str !{}:              # provably pure: no model, no I/O
    return x.strip().lower()

def load_docs(path: str) -> list[str] !{fs.read}:    # may read files, nothing else
    ...

simulate def title(article: str) -> str by models.writer:   # gains model.invoke
    sem "A short, faithful title for the article."

Rules that make this real rather than decorative:

• !{} is a proof, not a comment. The compiler enforces it. A !{} function cannot call one that reads files or invokes a model.
• An omitted row is inferred, never a wildcard. Writing no !{…} asks the compiler to infer the minimal row from the body (fail-closed — a function that touches nothing infers !{}). Omission never grants ambient authority. At assure silver and above an explicit row is required, so a later code.exec shows up as a signature diff, not a silent change.
• !{*} is the loud escape hatch, not the meaning of silence — the explicit all-effects top, flagged at check time and refused under any restricting policy.
• Calling an unknown operation is an error. fs.raed("x") raises at the call site rather than silently doing nothing.

The canonical effect namespaces are model.invoke/model.embed, fs.read/fs.write, net.connect/net.listen, proc.spawn, code.gen/code.exec/code.patch, db.*, env.*, observe.record, ui.*, and a few more; see the Effects reference.

The gradual guarantee lattice

Because the two regions coexist, Sema needs a way to say how much is guaranteed about any given value or obligation — a type check, a contract clause, a semantic predicate, a policy conformance. Every obligation carries a status on this lattice, strongest to weakest:

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

Status	Meaning
proved	Discharged statically — types, SMT refinements, capability reachability. No runtime cost, no possibility of failure at that point.
checked	A sound runtime check is inserted, with blame — if it fails, the error names the responsible call.
statistical(α)	A calibrated conformal/statistical bound at confidence level α, valid under exchangeability — the honest label for a model-judged predicate.
best_effort	Evaluated, but unbounded — no guarantee attached.
unchecked	A visible hole (a todo). Release builds reject reachable holes.

The governing rule is verifier-inheritance: a generative result’s guarantee level equals the strongest sound check applied to it. A raw simulate output is untrusted; add an ensure and the checked region is checked; a check semantics(…, alpha=…) types the region statistical(α). The compiler inserts the checks at region boundaries with blame-carrying labels that name the generative call at fault.

Statistics must be watched, or they decay

One rule deserves its own line, because it is what keeps statistical claims honest: a statistical(α) obligation requires an active monitor on its input stream. Without one it decays to best_effort at the type level.

The reasoning is simple. A conformal certificate is only honest while the live data distribution still matches the calibration set. A monitor (§ governance) is what watches for that assumption breaking. So a calibrated ~= branch or semantics() guard keeps its statistical(α) strength only while a monitor covers its inputs; where the compiler cannot cover a site, it decays it to best_effort and tells you, naming the missing monitor. A statistical guarantee you are not watching is not a guarantee, and Sema types it that way.

No silent no-ops

The ethos that ties the whole model together: syntax that parses must have a real effect or fail loudly. Sema exists because the harness around LLM software is full of things that look like they do something and quietly don’t — a validator no one runs, a natural-language rule that is “context, not enforced configuration,” a contract that records failure but never blocks. Sema treats that as a defect class to eliminate:

• A value that fails its contract is typed as failed and cannot flow into non-handling code. A library can advise; a compiler can block.
• ~= never returns a bare bool — it returns a graded similarity value, so a fuzzy comparison can’t be silently cast to a hard branch.
• A model’s output is untrusted until a check clears it; no trusting sink accepts it directly.
• sema check flags unrecognized directives — a mistyped or misplaced clause in a function body that no runtime handler recognizes is reported, not silently ignored.
• Degradations are surfaced, never hidden — a recoverable failure is logged to the journal and stderr, and SEMA_STRICT=1 turns every one into a hard error.

Verification by default

The last piece: verification is on by default, not opt-in. There is no testable keyword to remember. Every function is verified; the depth is a dial (bronze/silver/gold), and sema assure runs the engine — executing test blocks, fuzzing ensure properties for counterexamples, and mutation-testing at gold. Verdicts are three-state — red (a replayable counterexample with blame), amber (inadequate evidence, itself a first-class output), and green (only achievable at a stated mutation score). Green is impossible on a weak suite by construction, which is the whole point: an opt-in verification flag recreates exactly the harness failure mode Sema exists to kill.

Putting it together

When you read a Sema function, read it in these terms:

1. What is its effect row? !{} means pure core; anything else is the edge, and you can see exactly which capabilities.
2. What guarantees its results? Look for ensure/invariant (→ checked), check semantics(…, alpha=…) (→ statistical(α)), or nothing (→ best_effort).
3. If it’s statistical, is it monitored? No monitor means the label has already decayed.
4. Could anything here be a silent no-op? In Sema, no — it would have failed check or been typed as failed.

Everything else in the language is an application of this model.

Next

• Effects — the full effect system, namespaces, and how policies confine them.
• Verification — contracts, assure grades, properties, and mutation adequacy in depth.