# §1. Design principles > Sema language specification — §1 Design principles. > Generated from `docs/LANGUAGE.md` §1. This is the normative specification; for a guided tour see the Language and Neurosymbolic sections. Eight principles, each grounded in the corpus. Every construct in §5 must satisfy all of them. 1. **Probabilistic under the hood, deterministic at the boundary.** Every construct has a nonempty deterministic guarantee column — no Sema construct is purely statistical. The guarantee map ([05 §5](./research/05-pl-theory-guarantees.md)) is generated by one rule: *a generative result's guarantee level equals the strongest sound check applied to it* (verifier-inheritance, [05 §4.4](./research/05-pl-theory-guarantees.md)). 2. **Enforced, never advisory.** SymbolicAI's `@contract` records failure but never blocks execution — DbC as advice ([01 §6](./research/01-symbolicai.md)); Claude Code documents that natural-language rules are "context, not enforced configuration" ([03](./research/03-harness-archaeology.md)). In Sema, a value that fails its contract is *typed as failed* and cannot flow into non-handling code. A library cannot make validation non-bypassable; a compiler can. That is the reason Sema is a language. 3. **Honest grading.** Statistical verdicts are typed as statistical and carry their evidence (score, judge identity, threshold, calibration set, α). A fuzzy bool silently cast to `bool` — SymbolicAI's `ProbabilisticBooleanMode` word-matching ([01 §3](./research/01-symbolicai.md)) — is a language-level defect class Sema eliminates by construction. 4. **Pinned judges.** `semantics()`, `~=`, and every model-evaluated predicate denote a *pinned judge* (model hash + prompt + threshold + calibration set), making evaluation total and reproducible; judge-vs-intent agreement is a separate, quantified statistical question ([05 §1.4](./research/05-pl-theory-guarantees.md)). Changing a judge is a semver-major change to program semantics. 5. **The model proposes, the toolchain disposes.** Every LLM-produced artifact (test, patch, translation, output) passes deterministic execution filters before it enters the build or the dataflow — Meta's Assured-LLMSE discipline, which is what made 73% human acceptance possible ([09 §2.5](./research/09-verification-testing.md)). LLM self-assessment is banned from any acceptance path ([10](./research/10-self-healing-drift.md)). 6. **Accrete determinism.** Statistical and adversarial findings are distilled into permanent deterministic artifacts (counterexamples, killed mutants, regression properties); a Sema codebase's verification substrate hardens monotonically ([09 §7.2](./research/09-verification-testing.md)). 7. **Familiar surface, honest divergence.** Pythonic syntax, explicitly *not* a Python superset — Mojo's landing position, never its launch position ([12 §1](./research/12-syntax-dx.md)). LLM authors are first-class: the grammar ships as a constrained-decoding artifact and the spec as the generator corpus ([12 §6](./research/12-syntax-dx.md)). 8. **No super-Turing claims.** Sema + computable model oracles is exactly Turing-equivalent; the oracle framing buys a query/trust/substitutability boundary, not power ([05 §1.2](./research/05-pl-theory-guarantees.md), [arXiv:2406.12213](https://arxiv.org/abs/2406.12213)). ---