Why Sema

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:

# 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) — 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 <model>; 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 — build the toolchain from source and run your first example.
• Mental Model — the deterministic core, the generative edge, the gradual guarantee lattice, and the “no silent no-ops” rule that ties them together.