# Why Sema > The problem Sema solves — untyped glue around model calls — and the bet it makes: one language where the deterministic core and the generative edge share one verification story. Sema is an AI-native, **neurosymbolic** programming language. Its surface is Python-shaped — indentation blocks, `def`, `struct`, `enum`, traits — but its semantics are new: **models, contracts, effects, and semantics are first-class language constructs, not library calls.** A model can implement a function; similarity is an operator; the capabilities a function may use are part of its type; and contracts are checked, not hoped for. This page explains the problem Sema exists to solve, and the single bet it makes in response. ## The problem: LLM software is untyped glue An application built around a language model today is, structurally, a pile of glue. The model call sits in the middle of a Python function, and everything that makes it *reliable* is bolted on around it, by hand, per project: - A **grammar or JSON schema** is stapled to the output so it parses. - **Retry loops** re-ask when the output is malformed or fails a validator. - **Validators and guardrails** check the result after the fact, in a separate layer that the type system knows nothing about. - **Policies** ("never call this endpoint", "don't run shell") live in review comments, a linter, or a runtime harness — anywhere except the code's type. - **Usage and cost** are threaded through as extra return values, or scraped from logs. This is the harness. Coding agents work *because* of their harness — constrained decoding rescues syntax, repo maps rescue relevance, linters and type checkers rescue correctness, repair loops rescue completeness. The machinery is essential. The problem is *where it lives*: outside the language, reimplemented for every tool, bypassable by construction, and unusable on-device. And crucially, the language underneath sees none of it. To Python, a model call is just a function that returns a string. There is no type that says "this value came from a model and has not been checked." There is no type that says "this function is allowed to read files but not open sockets." A validator that a caller forgets to run is simply not run — silently. A contract in SymbolicAI *records* a failure but never *blocks* execution; a natural-language rule in an agent harness is "context, not enforced configuration." A library can advise. It cannot make a check non-bypassable. Only a compiler can. ## The bet: one verification story for the whole program Sema's bet is that the deterministic core of a program and its generative edge should live in **one language, with one verification story** — so that "ask a model" and "prove a property" are equally first-class, and the same machinery guards both. That means moving the harness *into* the language: ```sema # A function whose body is written by a model — but fenced by a type, an # effect row, a token budget, and a semantic contract that is actually checked. simulate def summarize(article: str) -> str by models.writer: sem "A faithful, single-paragraph summary of the article." budget tokens=400 ensure len(result) < len(article) check semantics("the summary makes no claim absent from the article") # The deterministic core stays provably model-free and I/O-free. def dedup_titles(titles: list[str]) -> list[str] !{}: return semantic.dedup(titles, 0.86) ``` Read what each construct is doing, because none of it is a library call: - `simulate def … by models.writer` — the model *implements the body*. `models.writer` is a pinned, first-class model value (a hash, a revision, a role), never a floating `"latest"`. - `sem "…"` — the natural-language descriptor the model works from, part of the compiled artifact, not a runtime string. - `budget tokens=400` — a hard, typed budget the scheduler enforces; overspend is a typed error, not silent. - `ensure …` and `check semantics(…)` — a *hard* contract and a *monitored* semantic one. A value that fails `ensure` is typed as failed and cannot flow onward. `summarize`'s output is `untrusted` until a check clears it. - `!{}` on `dedup_titles` — a proof that this function performs **no model calls and no I/O**. The deterministic core is a type-enforced sublanguage, not a convention. The result is one program in which a model's output and a proved property carry graded, honest labels on the *same* lattice — from `proved` down to `best_effort` (see [Mental Model](/start/mental-model/)) — and the compiler inserts the checks at the boundary between them. ## Contrast: Python-as-glue vs. Sema-as-language | Concern | Python + a harness | Sema | |---|---|---| | Model call | A function returning a string | `simulate def … by `; output typed `untrusted` | | Output shape | Schema stapled on; retry loop by hand | Constrained decoding to the declared return type | | A validator you forgot | Silently not run | A failed contract is *typed as failed*; it cannot flow onward | | Capabilities | Convention, a linter, or a runtime sandbox | An effect row in the type: `!{fs.read, model.invoke}` | | Policy | Review comments; external harness | `policy` with `allow:`/`forbid:` and examples verified at load | | Cost / usage | Threaded return values, log scraping | Ambient `with meter as u:` / `with budget(…)` | | Similarity | An SDK call returning a float | `~=`, a calibrated operator returning a graded value | | Guarantees | Untracked | The gradual guarantee lattice, per decision site | The point is not that Python can't do these things — with enough glue, it can. The point is that in Python the guarantees are *optional and invisible*: nothing in the type of a value tells you whether it was checked, where it came from, or what it is allowed to touch. In Sema those facts are in the type, and the compiler will not let you ignore them. ## Why a language, and not a framework Every surveyed AI DSL and framework either died or stopped at the schema boundary, because **library-level enforcement is bypassable by construction.** A library cannot make validation non-bypassable, cannot type a value as `untrusted` across a whole program, and cannot prove a function performs no I/O. A compiler can. That is the reason Sema is a language rather than a Python package. Two honest boundaries follow from the same principle: - Sema is **explicitly not a Python superset.** It keeps the Pythonic surface (the familiar one, the one code LLMs already write well) but drops the dynamic features that defeat static guarantees — no classes or inheritance (traits and algebraic data types instead), no monkey-patching, no wildcard imports. - Foreign code **weakens guarantees on purpose.** Inline Python or C is confined and best-effort; the strong claims hold for Sema code, and the boundary is visible in the types. :::note Sema has a working Rust reference implementation — a tree-walking interpreter, an opt-in bytecode VM, a CLI, an LSP, and native model backends. Everything on this page runs. The next two pages get you from zero to a running program. ::: ## Next - [Installation](/start/installation/) — build the toolchain from source and run your first example. - [Mental Model](/start/mental-model/) — the deterministic core, the generative edge, the gradual guarantee lattice, and the "no silent no-ops" rule that ties them together.