RFC 0001: The SEMAPRAX programming system

September 5, 2026 · View on GitHub

  • Status: Draft
  • Version: 0.2
  • Audience: language users, compiler contributors, tool authors, and agent builders

Summary

SEMAPRAX is a graph-native, contract-driven systems programming language designed for collaboration between humans and autonomous software agents.

Agents manipulate program meaning; humans read and edit source; the compiler produces native machine code or portable components.

Its design is summarized by: Meaning in. Verified machine code out.

Goals

  1. Give every public declaration a persistent semantic identity.
  2. Make types, effects, capabilities, ownership, contracts, dependencies, and target support queryable without reconstructing them from text.
  3. Accept agent changes as atomic operations against a known graph revision.
  4. Produce deterministic diagnostics and typed repairs.
  5. Provide memory safety without a mandatory tracing collector.
  6. Compile to native code for systems work and portable components for interoperability.
  7. Keep a canonical, readable, Git-friendly source projection.

Non-goals include natural language as executable authority, cryptic token-minimized syntax, unrestricted macros, a proprietary VM as the only runtime, and pretending all libraries or user interfaces are portable across every target.

Program representation

The logical program is a versioned semantic graph. Nodes include declarations, specifications, tests, packages, schemas, targets, and generated artifacts. Edges include calls, type use, implementation, capability flow, proof dependency, target availability, and ownership relationships.

Public declarations retain persistent IDs across rename and movement. Expression identities may be revision-scoped. Human source parses into the graph and canonical formatting projects it back to text.

Graph revisions are content-addressed. An operation against a stale base revision fails before mutation. A successful multi-file transaction either commits every verified operation or none.

Core language

The mature core contains records, algebraic variants, functions and closures, interfaces and implementations, constrained generics, exhaustive matching, immutable values by default, explicit mutation, Option, Result, structured concurrency, ownership and regions, effects and capabilities, contracts, state machines, and typed hygienic generation.

There is one canonical representation for imports, formatting, asynchronous control flow, optional values, results, tests, and packages. Reducing arbitrary choices reduces both human policy surface and agent retries.

This RFC defines the mature contract, not the current implementation subset. The completion matrix owns present status. Bounded language additions such as mutation, matching, text, byte data, and unsafe boundary mechanics each define their exact admission and non-claims without expanding this RFC's status narrative.

Effects and capabilities

Function types expose authority. Effects may describe database access, network destinations, filesystem paths, clock, randomness, devices, unsafe memory, blocking, or nondeterminism.

permit { clock.read }

fn tick(value: i64) -> i64
    uses { clock.read }
{
    value + 1
}

No library receives ambient authority. An application manifest grants capabilities explicitly. Callers must declare the effects of callees, and dependencies cannot silently widen application permissions. Tests can replace effects with deterministic handlers.

Contracts and verification

Preconditions, postconditions, invariants, state transitions, resource protocols, authorization rules, and bounded temporal properties belong in the program graph.

Verification is progressive:

  1. Types, effects, ownership, and exhaustiveness on every build.
  2. Cheap static contract discharge.
  3. Bounded symbolic execution or SMT checking where configured.
  4. Runtime guards for obligations not statically proven in safe profiles.
  5. Generated property tests and fuzz inputs.
  6. Explicit full-proof obligations for selected modules.

Failures should identify the violated property, a minimal counterexample when available, the semantic path, and valid typed repairs.

Memory model

The language has no mandatory global tracing collector. It combines value/stack storage, unique ownership, borrowed views, regions, shared immutable ARC, opt-in managed zones, and restricted raw memory.

The compiler infers borrowing and placement where possible. Regions make request, frame, parser, and pass allocation predictable. Managed zones permit cyclic application domains without imposing GC on servers, firmware, or hot loops.

The systems profile adds fixed-width types, explicit layout/alignment, volatile access, atomics with ordering, SIMD, memory-mapped I/O, no-allocation/no-blocking constraints, GPU kernels, and reviewable unsafe modules. Default arithmetic is checked unless a wrapping or saturating operation is named explicitly.

Concurrency

Structured tasks are the default. Every spawned task belongs to a lexical scope; cancellation, failure, and resource cleanup propagate through that scope. Cross-task values satisfy Sendable; concurrently shared values satisfy Shareable. Shared mutation requires explicit synchronization. Tests can record and replay deterministic schedules.

Components and interoperability

Packages are interface-first. A package records an interface contract, target matrix, implementations, required capabilities, ownership rules, compatibility, provenance, and conformance tests.

Two ABI paths implement the same component interface:

  • A portable canonical ABI for WebAssembly Components, sandboxes, processes, and unknown runtimes.
  • A native fast ABI for compatible architectures and runtimes, allowing borrowed slices, zero-copy buffers, specialization, and controlled inlining.

Generated adapters import C headers, WIT, OpenAPI, Protocol Buffers, GraphQL, SQL schemas, JVM metadata, Apple framework metadata, and TypeScript declarations. Unsupported target/runtime combinations are explicit graph facts with compatible alternatives—not magical fallbacks.

Application model and targets

Cross-platform applications are a first-class language and compiler concern, not a later external framework. The application dialect defines typed state, actions, update functions, semantic view trees, navigation, localization, assets, accessibility, lifecycle, declared capabilities, background work, and platform-specific implementations.

Semantic controls such as headings, buttons, text fields, lists, menus, dialogs, validation states, keyboard actions, and accessible labels map to native platform meaning. The system does not promise identical pixels or force every target through a canvas:

  • web uses accessible DOM/CSS, server rendering, hydration, Wasm logic, browser shims, and Canvas/WebGPU only for custom visuals;
  • iOS/macOS use native machine code, generated Swift/Objective-C hosts, XCFrameworks or app projects, native lifecycle/accessibility, UIKit/AppKit/SwiftUI adapters, and Metal escape hatches;
  • Android uses native libraries, generated Kotlin/JNI hosts, AAR or Gradle projects, lifecycle/accessibility/input integration, Compose/View adapters, and Vulkan/platform rendering;
  • Windows and Linux use native executables, WinUI or a selected Linux adapter, native windows/menus/accessibility, packaging metadata, and accelerated custom rendering;
  • server, edge, plugins, embedded, and GPU profiles produce explicit native, WASI/Component, firmware/object, or kernel artifacts with profile-specific capability and runtime constraints.

One application may mix platform-native semantic controls with shared custom rendering. platform blocks and interface implementations provide escape hatches without leaking platform-only code into shared callers. The graph records target availability and alternatives rather than pretending a browser npm package or Android lifecycle library works everywhere.

Typical artifacts include browser Wasm/ES/HTML/CSS, native or WASI servers, Mach-O/XCFramework/Apple hosts, Android .so/AAR/Kotlin-JNI hosts, macOS bundles, Windows packages, Linux AppImage/deb/rpm integration, sandboxed Components, bare-metal firmware, and SPIR-V/WebGPU/platform kernels. Generated manifests include permissions, entitlements, content-security policy, assets, localization, deep links, packaging metadata, and mechanically derivable privacy declarations. Signing remains with platform toolchains and credentials.

Compiler pipeline

Source or semantic transaction
          |
    semantic graph
          |
 typed high-level IR
          |
 ownership + effect IR
          |
 domain dialects (async, UI, database, SIMD, GPU, components)
          |
 optimized core IR
       /     |      \
Cranelift  LLVM   WebAssembly/SPIR-V

Cranelift is the intended fast development lane. LLVM is the intended optimizing native and embedded lane. WebAssembly Components are the intended portable and sandboxed lane. The current C11 lane is an inspectable bootstrap backend.

Agent protocol

The compiler exposes graph lookup, bounded context, impact analysis, typed holes, diagnostics, repairs, and transactions. A patch may carry intended contracts, tests, allowed capability deltas, affected targets, and proof expectations. The compiler verifies claims; it never trusts them because an agent asserted them.

Semantic review summarizes behavior, API, security, memory, target, migration, and unsafe-code changes separately from textual formatting.

The first text transaction syntax is intentionally tiny. The stable protocol will be schema-versioned JSON/CBOR over a local authenticated transport.

Security and reproducibility

Packages and build scripts execute with declared capabilities: their own source, their own output directory, approved tools, and no network, home directory, or secrets by default. Package records include source, compiler, interface hash, inputs, licenses, capabilities, native and unsafe code, reproducibility, SBOM, and signatures.

Untrusted extensions normally run as capability-limited WebAssembly Components. Foreign code is classified as verified-safe, safe-wrapper, unsafe-native, sandboxed-component, or out-of-process.

Compatibility

Language syntax, graph schema, transaction schema, package format, component interface, and ABI are versioned independently. The compiler must provide deterministic migrations for canonical source and graph data whenever practical.

Breaking changes before 1.0 are expected. After 1.0, stable public interfaces follow semantic compatibility rules based on types, effects, contracts, ownership, and target support—not names alone.

Source syntax and expression trees admit at most 128 nested constructs. Inputs past that bound fail with located SPX-P207 before recursive parser or projection work; split the expression or block into named helper functions.

Open questions

  • Which ownership constraints can be inferred without hiding meaningful cost?
  • What is the smallest durable graph identity scheme across repository history and merges?
  • Which proof engine best matches progressive verification and actionable counterexamples?
  • Where should native fast-ABI compatibility stop and canonical lowering begin?
  • How should semantic merge conflicts be represented for human review?
  • Which application validation workload exposes cross-platform abstraction failures earliest?