# Mental Model > The core idea behind Sema — the deterministic core versus the generative edge, the gradual guarantee lattice, verification by default, and no silent no-ops. 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: ```sema 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](/governance/effects/). ## 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](/governance/effects/) — the full effect system, namespaces, and how policies confine them. - [Verification](/neurosymbolic/verification/) — contracts, `assure` grades, properties, and mutation adequacy in depth.