An experimental systems programming language with a stable semantic program graph designed for humans and software agents.
Get started · Understand the model · Check the status · Read the docs
Warning
SEMAPRAX is pre-alpha research software. Its language, graph schemas, diagnostics, and ABIs can change. Do not use it for production or safety-critical workloads.
Most programming tools edit text and reconstruct meaning afterward. SEMAPRAX
keeps readable .spx source as the canonical Git representation while
exposing a deterministic, versioned semantic graph for program analysis and
agent operations.
| Principle | Practical effect |
|---|---|
| Persistent identity | Public declarations keep stable @id values across display-name changes. |
| Checked meaning | Types, effects, contracts, ownership, and call relationships are resolved before lowering. |
| Stale-safe changes | Supported semantic patches bind to a known revision and fail without changing source when replay or validation fails. |
| Shared semantics | Native and WebAssembly lanes start from the same validated HIR and cleanup meaning. |
- Rust 1.88 or newer
- Clang for native compilation
- Node.js 22 or newer for the WebAssembly examples
git clone https://github.com/wavect/semaprax.git
cd semaprax
cargo run --locked -p semaprax -- check examples/meaning.spx
cargo run --locked -p semaprax -- run examples/meaning.spxThe example prints 42.
Install the development CLI locally if you prefer shorter commands:
cargo install --path .
semaprax check examples/meaning.spx
semaprax run examples/meaning.spxPrivate-host commands require the unpublished full toolchain, not the standalone crates.io compiler package. Install it from the same checkout to create a checked calculator project from the built-in template:
cargo install --locked --path crates/semaprax-toolchain
semaprax-full new first-semaprax
cd first-semaprax
semaprax check semaprax.toml
semaprax test semaprax.tomlThe generator uses only compiled-in files and does not initialize Git, install dependencies, or access a network. Continue with the executable quickstart to run, inspect, and build the project.
To obtain the exact same four calculator files as a replayable stdout document without granting SEMAPRAX a destination or publication authority:
semaprax project-scaffold --name first-semapraxThe semaprax.project-scaffold.v1 capsule is caller-materialized data, not an
archive or atomic filesystem publication API.
semaprax graph examples/meaning.spx
semaprax context examples/meaning.spx app.main \
--depth 1 --max-bytes 65536 --max-nodes 256semaprax build examples/calculator.spx --target web \
--export calculator.add --export calculator.divide \
-o target/calculator-web
node scripts/verify-web.mjs target/calculator-webThe generated JavaScript API uses stable IDs, so a source-level display rename does not change the external key. The current boundary is intentionally limited; see Wasm Scalar Exports v1.
semaprax check examples/calculator-project/semaprax.toml
semaprax test examples/calculator-project/semaprax.toml
semaprax build examples/calculator-project/semaprax.toml \
--target web -o target/calculator-project-webThe current semaprax.toml profile names a closed source set, entry and test
modules, and selected exports. It is a bounded project input, not a dependency
manager or package registry. See Project Manifest v1
and its additive versioned extensions for exact limits.
The additive library-only Offline Multi-Package Source Capsule v1 authenticates a narrow caller-owned, effect-free scalar package source closure above exact offline resolution. Linked Scalar Core-Wasm Package Build v2 consumes only that replayed closure and retained HIR, while the separate safe publisher reuses the existing exact three-file authority state machine. Both surfaces and their hostile evidence are authored but unrun and unpromoted; they are not a package manager, target-conformance result, trusted-provenance system, or hermetic build sandbox.
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)
}
@id is the declaration's persistent semantic identity. The name add is
for humans; tools can continue to refer to math.add after a supported rename.
More examples cover control flow, effects, ownership, records, mutation, matching, and bounded byte data.
flowchart LR
S["Canonical .spx source"] --> P["Parse and verify"]
P --> H["Validated stable-ID HIR"]
H --> G["Versioned semantic graph"]
G --> Q["Context · impact · review"]
G --> T["Replay-checked transactions"]
T --> S
H --> N["C11 / Clang"]
H --> W["WebAssembly Core"]
Readable source remains the reviewable, version-controlled representation. The graph is the preferred query and change interface. A graph or evidence capsule describes meaning; it does not itself grant filesystem, build, or publication authority.
| Command | Purpose |
|---|---|
semaprax --version / version --json |
Report deterministic package and injected commit identity. |
semaprax-full doctor [--profile <id>] [--target …] [--json] |
Private offline-profile checks; production profiles currently unavailable, with no ambient-tool fallback. |
semaprax-full new <destination> |
Private full-toolchain creation and validation of a Project v1 calculator. |
semaprax check … |
Parse, resolve, type-check, and verify a file or project manifest. |
semaprax fmt <file> [--check] |
Write or check canonical formatting. |
semaprax run … / semaprax test … |
Execute an admitted file or project through the development path. |
semaprax build … --target … |
Produce an admitted native, callable, WebAssembly, Web, or npm artifact. |
semaprax graph <file> |
Emit the revisioned semantic graph. |
semaprax context <file> <id> … |
Emit bounded semantic context around a declaration. |
semaprax impact / review |
Preview supported semantic-patch consequences without writing. |
semaprax patch |
Apply a supported single-file semantic transaction. |
semaprax workspace-* |
Use the bounded managed multi-file protocols. |
Run semaprax --help for the complete command list. Many report, evidence,
workspace, and host-integration commands are narrow protocol surfaces intended
for tool authors; their versioned reference documents define the exact
admission rules and non-claims.
The current source tree also contains an exact Project v8
owned-data-api.v1 developer-preview route for --target npm and
--target rust, plus the examples/frame-payload-* validation fixtures. Its
implementation and executable evidence are authored, but the current
integration head has not completed the required exact-head hosted promotion.
The generated packages are unpublished and must not be treated as a stable or
supported general owned-data ABI. See Public Owned Data API
v1 and the completion
matrix.
The source tree also contains authored-but-unrun Project v9 flat-owned-record and Project v10 owned-UTF-8 follow-ons. Their generated packages are unpublished, neither profile is promoted, and v10 remains gated on v9 promotion. See Public Flat Owned Record API v1 and Public Owned UTF-8 API v1.
Release line: v0.2 · Maturity: pre-alpha research · Overall goal: Partial
SEMAPRAX has executable vertical slices across its language, semantic graph, agent-change workflow, native C11 lane, Core WebAssembly lane, bounded project builds, and selected host integrations. It does not yet provide the general ownership/lifetime system, package ecosystem, stable public ABIs, production application toolchain, or cross-platform validation required for 1.0.
Status has one owner: the completion matrix. It separates the long-term product contract from the current release-exit audit and links each claim to its evidence-owning specification. Historical changes belong in the changelog; future sequencing belongs in the roadmap.
The documentation has three audiences:
- Public documentation explains the language, supported workflows, and user-visible boundaries.
- Versioned reference specifications define exact wire formats, admission profiles, diagnostics, and compatibility rules for tool and host authors.
- Development documentation contains architecture, completion evidence, quality gates, roadmap sequencing, migrations, and private experiment contracts.
The book summary is the exhaustive catalog. Stable
specification paths remain in docs/ so existing citations keep working.
Read CONTRIBUTING.md and AGENTS.md before changing semantics. On Unix, the complete repository gate is:
scripts/quality.sh fullChanges to syntax, graph schemas, transactions, effects, ownership, contracts, or ABIs should begin with an RFC or an explicit update to an existing one.
Use CITATION.cff for repository metadata and CITATION.md for claim-specific evidence guidance. SEMAPRAX is maintained by Wavect GmbH and distributed under the Apache License 2.0.