The Semaprax Handbook
Ernesto, the Semaprax mascot, guides you from one .spx file to a checked,
tested project. This handbook matches Semaprax 0.9.0.
Semaprax is beta software. Syntax, protocols, and binary interfaces can change. Use it to experiment and prototype, not for production or safety-critical work.
Start here
- Install Semaprax. It has a one-command installer and a Homebrew formula.
- Write and run your first program.
- Create a project with modules and tests.
Prefer to watch first? See the recorded walkthrough.
What Semaprax is
Semaprax is a systems language where people and AI agents work on the same
program. You write .spx source. The compiler checks it and exposes a
semantic graph of declarations, types, contracts, effects, and calls.
| Idea | What it means |
|---|---|
| Readable source in Git | .spx files are the source of truth. One formatter, one layout. |
| Stable identities | Each declaration has an @id("math.add") that survives renames. |
| Contracts and effects | requires, ensures, and uses are checked by the compiler. |
| Ownership | The compiler rejects use-after-move and data races. |
| One meaning, three engines | Checked code behaves the same in the interpreter, native C11, and WebAssembly. |
The whole loop in one example
module examples.meaning;
@id("math.add")
fn add(left: i64, right: i64) -> i64
requires left >= 0
requires right >= 0
ensures result == left + right
{
left + right
}
@id("app.main")
fn main() -> i64
ensures result == 42
{
add(19, 23)
}
semaprax fmt meaning.spx # canonical layout
semaprax check meaning.spx # types, contracts, effects, ownership
semaprax run meaning.spx # prints 42
What do you want to do?
| Goal | Read |
|---|---|
| Install | Install |
| Run one file | First program |
| Build a multi-file project | First project → Modules |
| Learn the language | Essentials → Types → Ownership |
| Use functions, loops, collections | Functions · Loops · Collections |
| Model data and behavior | Classes · Matching · Contracts and effects · I/O · Resources |
| Prove properties | Laws and proofs |
| Configure a project and pick a target | Manifests → Profiles → Targets |
| Call Semaprax from Rust or JavaScript | Integrations |
| Use VS Code | Editor setup |
| Let a coding agent edit your code | Agent workflow → Semantic explorer |
| Build an agent as a Semaprax program | Agent programs → Budgets and recovery |
| Measure context size | Token reports and caches |
| Test, debug, release | Testing · Debugging · Shipping |
| Run the agent harness, check trust limits, find a specialist command | Harness · What Semaprax verifies · Specialist commands |
| Find a command | Command reference |
| Look something up | Cheatsheet · Standard library · Built-ins · Cookbook · Glossary |
For implementation details, use the source map and
the specifications in docs/.
Get help from the compiler
semaprax help # commands you need first
semaprax help all # every command
semaprax help language topics # language topics, one at a time
semaprax help diagnostic SPX-T208 # the fix for one error code