Sounio Compiler

SOUNIO

A self-hosted systems + scientific programming language for epistemic computing, uncertainty propagation, and algebraic effects

Website · Playground · Documentation · Manifesto · Examples · Status · Contributing

---

Sounio is a systems programming language for epistemic computing — its type system tracks not just what your data is, but how much you should trust it. Uncertainty propagation, provenance tracking, and confidence-gated execution are built into the type system, not bolted on as libraries.

New here? Read TOUR.md. Twenty claims, each one a program that bash scripts/tour.sh --full --lean runs and checks (20/20, about 4 minutes, measured 2026-10-04; --full alone runs 16 of them, the other 4 are the Lean proofs that need --lean), followed by a table of what does not work yet, with issue numbers.

Keywords: systems programming language, scientific computing language, epistemic types, uncertainty propagation, algebraic effects, self-hosted compiler, formal verification, non-associative algebra, octonions, e-graphs.

Technical Pillars & Core Keywords

Pillar	Description	Key Search Terms
Epistemic Computing	Built-in confidence-gated execution tracking and provenance tracking.	epistemic-computing, Knowledge[T], confidence-threshold
Uncertainty Propagation	GUM-compliant (Guide to the Expression of Uncertainty in Measurement) error propagation.	uncertainty-propagation, GUM-compliance, error-propagation
Systems & Science	Native Linux x86-64 ELF compilation (the only target), self-hosted compiler loop; GPU support is PTX emission for named kernel patterns, a skeleton rather than a GPU backend (TOUR.md §6).	systems-programming, scientific-computing, ptx-codegen
Algebraic Effects	Explicit side-effects declarations (IO, Mut, Div, Panic, Alloc).	algebraic-effects, effect-system, effects-with
Mathematical Rigor	Non-associative octonion basis associators, formalized Lean 4 proofs of invariants.	non-associative-algebra, octonions, lean4-proofs
Dimensional Analysis	Units are types (VAR_UNIT_DIM) and adding incompatible units is rejected. Dimensional checking is partial, not compile-time enforcement: #2751 (wrong-dimension product accepted on lean_single), #2752 (Madaros rejects let d: m).	dimensional-analysis, unit-types

The compiler is self-hosted: Sounio compiles itself. make build starts from the committed prebuilt compiler bin/souc-linux-x86_64 and rebuilds self-hosted/compiler/lean_single.sio until stage N and stage N+1 are bit-identical (a true fixed point). The original C seed, bootstrap/stage0.c (2,792 lines by wc -l, 2026-10-05), is not on the make build path: it compiles the small bootstrap/boot1.sio compiler, which compiles itself and a hello-world, and that path is exercised by scripts/ci/bootstrap_chain_gate.sh. It was used to computationally verify a new result in algebra — that the count of nonzero octonion basis associators equals |PSL(2,7)| = 168 — now submitted for publication.

This is an active research project, not a production release. Read the honest status before using it for anything serious.

Cross-Repo Example: Cognitive O-SSM on SWOW-EN

The canonical Sounio checkout now includes a bounded cross-repo example under:

• examples/cognitive_ossm/

This lane is paired with the repository:

• github.com/agourakis82/hyperbolic-semantic-networks

Workflow split and current boundary:

• Sounio provides checkable .sio implementation scaffolding and separately executable epistemic receipts.
• The hyperbolic repo exports the compact SWOW bundle in data/cpc2026/sounio_input/.
• The hyperbolic repo's Python mirror currently generates the full paper-scale O-SSM artifacts.
• The repaired native reference passes Madaros check, but current native-v2 compilation is blocked. Historical native n=100/n=1000 JSON files are excluded from parity claims.

From the Sounio repo root:

./bin/souc check examples/cognitive_ossm/run_ossm_native_reference.sio
CPC2026_SCIENTIFIC_REPO=/workspace/hyperbolic-semantic-networks \
  bash scripts/ci/cpc2026_yale_evidence_gate.sh
uv run --with numpy python scripts/research/cpc2026_ossm_subset_audit.py

---

For LLMs and Code Tools

• Start here: CLAUDE.md (build and run, the syntax that differs from Rust, agent tooling, known limitations) and AGENTS.md
• Prompt surface: llms.txt
• Repository scale (read before estimating size): SCALE.md · docs/audit/README.md
• Regenerate numbers: bash scripts/dev/measure_repo_scale.sh
• Repository guide: CLAUDE.md
• Syntax and workflow guide: docs/guide/LLM_PROGRAMMING_GUIDE.md
• Live Hugging Face dataset: https://huggingface.co/datasets/chiuratto-AIgourakis/sounio-code-examples
• Training dataset export: datasets/sounio-code-examples/README.md
• Dataset builder: scripts/dev/export_hf_dataset.py

This repo now ships a root llms.txt for model-aware tools and a reproducible Hugging Face-style dataset export built from the Sounio test suite. The current published dataset lives in the maintainer namespace as a public mirror until the sounio-lang Hugging Face org namespace is ready.

---

What makes Sounio different

Epistemic types as first-class citizens. Every scientific measurement has uncertainty. Most languages ignore this. Sounio's type system includes Knowledge[T] with built-in confidence, provenance tracking, and automatic GUM-compliant uncertainty propagation. The compiler can enforce confidence thresholds at compile time — a function requiring ε >= 0.82 rejects under-confident data before any code runs. No equivalent system exists in any production language.

Self-hosted compiler. The compiler bootstrapped from C through a multi-stage chain (stage0.c → boot2g.sio → self-hosted) to a true fixed-point. The default workflow is now native-only: bin/souc compiles .sio sources to temporary or named ELFs via the Madaros self-hosted engine and executes those binaries directly.

Not a Rust/Julia dialect. Own syntax (&! not &mut, var not let mut), own semantics (algebraic effects, linear types, dimensional analysis), own philosophy (epistemic computing for science).

---

Quick taste

Uncertainty propagation with provenance

fn main() with IO {
    // A drug dose with tracked confidence and evidence source
    let base_dose: Knowledge[f64] = Knowledge(15.0, ε=0.92, prov="ASHP_2020_Level1A_RCT")

    // Hospital scale measurement: high-confidence device
    let weight: Knowledge[f64] = Knowledge(78.5, ε=0.98, prov="hospital_scale_calibrated")
    let ref_wt: Knowledge[f64] = Knowledge(70.0, ε=1.0)

    // GUM propagation is automatic: ε(a*b) = ε(a) * ε(b)
    let adjusted_dose: Knowledge[f64] = base_dose * (weight / ref_wt)

    // Extract propagated confidence
    let conf = adjusted_dose.ε   // ~0.90
    println(conf)
}

Full pipeline: tests/run-pass/vancomycin_propagation.sio — real ASHP 2020 vancomycin dosing with 5-step GUM propagation.

Compile-time confidence gate

// ASHP 2020 §8.3: AUC-guided dosing requires ε >= 0.82
fn prescribe_vancomycin(dose: Knowledge[f64, ε >= 0.82]) with IO {
    println("Vancomycin prescribed")
}

fn main() with IO {
    let risky_dose: Knowledge[f64, ε=0.40] = Knowledge { value: 500.0, epsilon: 0.40 }

    prescribe_vancomycin(risky_dose)  // COMPILE ERROR: ε=0.40 < required 0.82
}

The compiler rejects this before any code runs — a hard patient-safety guarantee. See: tests/compile-fail/vancomycin_low_conf.sio

Effects and linear types

fn sqrt_approx(x: f64) -> f64 with Mut, Div, Panic {
    if x <= 0.0 { return 0.0 }
    var g = x / 2.0
    var i = 0
    while i < 50 {
        g = (g + x / g) / 2.0
        i = i + 1
    }
    return g
}

linear struct FileHandle { fd: i32 }   // must be consumed exactly once

More examples: examples/epistemic_bmi.sio, docs/guide/SOUNIO_QUICK_START.md

---

Honest Status

This is an active research repository. Public claims are registry-backed; see docs/serious-language/public-claim-registry.v1.tsv (authoritative for every feature's maturity tier).

PL adoption audit (2026-05-27): docs/audit/PL_ADOPTION_AUDIT_2026-05-27.md — bone-honest stocktake of what a stranger cloning this repo will find, with live probes. The two biggest adopter-unlock gaps are (G1) closing the multi-module bundle compile and (G2) the CLI exit-code contract (G2 fixed 2026-05-27 in this commit).

Registry rows you should read before drawing conclusions: stdlib.surface = validated_research (bounded support contract only; not broad all-file callability) · tooling.editor = validated_research (checked formatter, REPL, preview LSP, and editor wiring; not mature IDE support) · tooling.package = validated_research (local packages only; no public registry) · closures.lambdas = stale_conflicting (spec §4.7.2 non-normative) · generics.{structs,functions,traits} = prototype · binary.source = validated_research (checked Madaros prebuilt is built from the modular tree; lean_single.sio remains the bootstrap seed) · platform.windows = prototype.

Scale (measured 2026-10-05): 8,777 tracked .sio files, ~3.37M lines (bash scripts/dev/measure_repo_scale.sh). The self-hosted compiler alone is ~639k lines — not a small experiment. Full audit: docs/audit/README.md · SCALE.md.

What WORKS (evidence-backed lanes)

Component	Status	Evidence
Epistemic core	Knowledge[T] + GUM + provenance	Named package / conformance gates
Self-hosted compiler	Lexer → codegen; fixed-point bootstrap	lean_single fixed-point + native-v2 spine gates
Ontology	Generated bundles + validation harness	run_ontology_validation.sh + compile gates
Native codegen	Linux x86-64 static ELF, the only target	Self-host + native-v2 gates
Core stdlib slices	Stats, linalg, ODE, etc.	stdlib_science_pipeline_gate, reliability inventory
Language server	LSP 3.17 subset	Release binary + protocol tests (prototype per registry)

What's SCAFFOLDING or PARTIAL

Component	Reality
~46% of stdlib modules	Classified scaffold in audit A.2 — code without executable proof
32 stdlib smoke tests	Print FOO_OK only; do not exercise module logic
129 CI gate scripts	Most are not on make check / GitHub CI (audit A.4)
GPU	souc build --backend gpu emits valid PTX only for empty-bodied kernels: an emission skeleton, not a backend (TOUR.md §6)
Theorem prover / async / geometry	Large or stub surfaces — see module audit JSON

Stdlib module audit (A.2, not file-count folklore)

Tier	Modules	Meaning
works	66	Tests, gates, or mass with executable evidence
scaffold	59	Code present; no direct executable proof in tree
doc-only roots	3	Non-module files at stdlib/ root

Do not cite 814/910 (89%) as "stdlib completeness" — that is harness inventory, mixes real tests with smoke placeholders, and differs from the reliability gate inventory. See audit artifacts under artifacts/audit/.

---

The 168 Theorem

While developing Sounio's octonion multiplication backend, we discovered and proved a combinatorial fact that appears not to have been explicitly stated in the literature:

The number of ordered triples (i, j, k) in {1,...,7}^3 for which the octonion basis associator [e_i, e_j, e_k] is nonzero is exactly 168 = |PSL(2,7)|.

The decomposition is 343 = 133 (repeated indices) + 42 (Fano-line triples) + 168 (non-collinear triples). We also report that sedenion nonzero associator counts are multiples of 168, and that the primitive zero-divisor pair count 336 = 2 x 168.

The result was verified computationally in Sounio and independently reproduced in Python/NumPy.

Paper: "The 168 Theorem: PSL(2,7) Governs Non-Associativity and Zero-Divisor Structure in the Cayley-Dickson Tower" — Agourakis & Gerenutti (2026). Submitted to Advances in Applied Clifford Algebras.

---

Get started

This checkout ships checked self-hosted compiler artifacts for Linux x86_64 behind the host-aware bin/souc launcher, which is the official compiler entrypoint and routes to Madaros by default. The checked bin/souc-* binaries are static Linux ELF artifacts; Linux x86-64 is the only target, and the binaries do not run on macOS (TOUR.md §6). No Rust build step is required for the default workflow.

git clone https://github.com/sounio-lang/sounio.git
cd sounio

export SOUC="$(pwd)/bin/souc"
export SOUNIO_STDLIB_PATH="$(pwd)/stdlib"

$SOUC --version                              # Madaros v0.80.0 (compiler build; the language release is 2.1.0)
$SOUC info                                   # selected host artifact + wrapper contract
$SOUC check examples/hello.sio               # type-check via checked self-hosted lane
$SOUC init hello_pkg && cd hello_pkg         # create a minimal sounio.toml project
$SOUC check && $SOUC run && $SOUC build      # project entrypoint -> ELF
$SOUC run examples/native/hello.sio          # compile to a temp ELF and execute it
$SOUC compile examples/hello.sio -o /tmp/souc-next

If you need the legacy bootstrap path explicitly:

SOUNIO_SOUC_ENGINE=lean_single \
  $SOUC compile self-hosted/compiler/lean_single.sio -o /tmp/souc-next

For detailed setup: INSTALL.md · docs/guide/MINIMUM_VIABLE_SOUNIO.md

Editor integration

The Sounio language server (bin/sounio-lsp) ships with the checkout and is the same binary published at sounio-lsp-v0.3.0-r1. Point any LSP-aware editor (VS Code, Neovim, Helix, Zed, etc.) at the binary with file-type .sio. Capabilities and the change log live in tools/lsp/CHANGELOG.md; Sprint-2 backlog in tools/lsp/SPRINT2_TODO.md.

---

Architecture

Pipeline: Source → Lexer → Parser → AST → Check → HIR → SIR → HLIR (SSA) → Codegen

Directory	Purpose
self-hosted/lexer/, parser/	Frontend (tokenizer, recursive descent)
self-hosted/check/, types/	Bidirectional type inference + algebraic effects
self-hosted/ir/	IR lowering, optimization, e-graph equality saturation
self-hosted/native/	Native x86-64 ELF emission (Mach-O, AArch64 and PE/COFF code there is unshipped preview)
self-hosted/compiler/	Codegen drivers (lean, IR)
stdlib/epistemic/	Knowledge[T], uncertainty (GUM), provenance
stdlib/units/	Dimensional analysis
bootstrap/	stage0 (C) → boot2g → self-hosted chain
formal/	Lean 4 proofs (epistemic type invariants)
tests/	run-pass/, compile-fail/, ui/, stdlib/

---

Design Principles

1. Uncertainty is not optional — Every scientific value has uncertainty. Ignoring it is a bug, not a simplification.
2. Provenance matters — Data without origin is data without trust.
3. Propagation is automatic — Manual uncertainty calculation is error-prone. The compiler handles it (GUM/ISO 17025).
4. Confidence gates execution — Low-confidence code paths require explicit acknowledgment.
5. One type definition, compiler guarantees everything — Define your epistemic constraints once; the compiler enforces them across all operations.

See docs/MANIFESTO.md for the full philosophy.

---

Known Limitations

Platform. Linux x86-64 only. The compiler and the programs it emits are static Linux ELF and do not run on macOS; there is no macOS, Windows or AArch64 target (TOUR.md §6).

Native startup cost. Native execution still requires producing a host binary before launch, so there is a small startup cost compared with an in-process executor.

Launcher contract. bin/souc now provides compatibility commands for check, run, compile, build, and init. When invoked inside a directory with sounio.toml, check, run, and build resolve the project entrypoint from [[bin]].path, [project].entry, or src/main.sio. Broader omega workflows and JIT-oriented tooling still live outside the checked self-hosted launcher lane.

Other targets. PE/COFF, Mach-O and AArch64 emitters exist in self-hosted/native/ but are not shipped or attested targets. The WASM backend is a blocked draft (#2237). The Cranelift JIT is no longer shipped (CHANGELOG 2.1.0).

REPL. The checked self-hosted launcher supports souc repl for a file-backed interactive loop.

Debug flags. --show-ast and --show-types are unavailable under the default Madaros engine (error: madaros build: unsupported option); they work under SOUNIO_SOUC_ENGINE=lean_single.

FFI. extern "C" remains limited in scope, but the old JIT-only integer FFI failure mode is gone on the native path.

GPU. souc build --backend gpu (Madaros) emits valid PTX only for kernels with empty bodies: no arithmetic, no memory access. It is an emission skeleton of named kernel patterns, not a GPU backend (TOUR.md §6). SPIR-V/Metal/WGSL files exist as stubs.

Full list: docs/compiler/KNOWN_LIMITATIONS.md

---

Citation

If you use Sounio in academic work:

@software{sounio2026,
  title     = {Sounio: A Systems Programming Language for Epistemic Computing},
  author    = {Agourakis, Demetrios Chiuratto and Gerenutti, Marli},
  year      = {2026},
  version   = {2.1.0},
  doi       = {10.5281/zenodo.18726647},
  url       = {https://github.com/sounio-lang/sounio},
  note      = {Self-hosted compiler with epistemic types and Lean 4 verification}
}

---

License

Apache-2.0. See LICENSE.

---

At the horizon of certainty, where ancient columns meet the endless sea.

SOUNIO