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.
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 x86_64 ELF compilation, self-hosted compiler loop, PTX/GPU acceleration. | 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 | Compile-time unit checking (VAR_UNIT_DIM) to prevent physical dimension errors. | dimensional-analysis, unit-types, compile-time-units |
The compiler is self-hosted: Sounio compiles itself, bootstrapped from a 2000-line C compiler through a multi-stage chain to a true fixed-point where stage N and stage N+1 produce bit-identical binaries. 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:
- Sounio provides the executable parity path and canonical
.sioimplementation scaffolding. - 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.
From the Sounio repo root:
./artifacts/omega/souc-bin/souc-linux-x86_64-gpu run examples/cognitive_ossm/cognitive_ossm.sio
./artifacts/omega/souc-bin/souc-linux-x86_64-gpu run examples/cognitive_ossm/run_regimes.sio -- --max-trajectories 8 --max-steps 64
./artifacts/omega/souc-bin/souc-linux-x86_64-gpu run examples/cognitive_ossm/export_results.sio
For LLMs and Code Tools
- Session bootstrap:
- Run
./sounio-whereami --quick - Read ONBOARDING.md
- Read CLAUDE_HANDOFF.md
- Read CLAUDE.md
- Read AGENTS.md
- Verify the current branch before editing
- Treat
/workspace/sounioas the active remote-first workspace path - Do not propose destructive reset/clean/rebase flows to "simplify" recovery state
- Run
- 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 = prototype · tooling.editor = prototype (formatter, REPL, LSP) · tooling.package = prototype (no public registry) · closures.lambdas = stale_conflicting (spec §4.7.2 non-normative) · generics.{structs,functions,traits} = prototype · binary.source = prototype (lean_single.sio is the source of the checked binary, not the modular tree) · platform.windows = prototype.
Scale (measured, 2026-05): 4,233 tracked .sio files, ~1.84M lines (bash scripts/dev/measure_repo_scale.sh). The self-hosted compiler alone is ~542k 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 ELF; Mach-O artifact lane | 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 CLI path | PTX/kaxi code exists; end-to-end CLI path incomplete |
| 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, macOS arm64, and macOS x86_64 behind the host-aware bin/souc launcher, which is the official compiler entrypoint and routes to Madaros by default. 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 # souc 1.0.0-beta.6
$SOUC info # selected host artifact + wrapper contract
$SOUC check examples/hello.sio # type-check via checked self-hosted lane
$SOUC compile examples/hello.sio -o /tmp/souc-next
$SOUC run self-hosted/compiler/native_print_f64_smoke.sio
$SOUC compile examples/hello.sio -o /tmp/hello-macos --target aarch64-macos
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 ELF and Mach-O emission in the current self-hosted lane |
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
- Uncertainty is not optional — Every scientific value has uncertainty. Ignoring it is a bug, not a simplification.
- Provenance matters — Data without origin is data without trust.
- Propagation is automatic — Manual uncertainty calculation is error-prone. The compiler handles it (GUM/ISO 17025).
- Confidence gates execution — Low-confidence code paths require explicit acknowledgment.
- 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. This checkout ships checked self-hosted compiler artifacts for Linux x86_64, macOS arm64, and macOS x86_64 behind the bin/souc launcher. Linux x86_64 and macOS arm64 are the active first-class host lanes. The newer native-v2 aarch64 backend is still preview-grade, so Apple Silicon support in this checkout is via the self-hosted Mach-O artifact lane rather than the new preview emitter.
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, and build, but broader omega workflows and JIT-oriented tooling still live outside the checked self-hosted launcher lane.
Windows cross-compile. The PE/COFF backend (3,508 lines) is production-grade. Use --target x86_64-windows to emit Windows binaries. No pre-built .exe is shipped in this checkout.
No REPL yet. The checked self-hosted launcher does not support repl.
Debug flags. --show-ast and --show-types are supported as pass-through flags on the checked self-hosted launcher for check, run, compile, and build.
FFI. extern "C" remains limited in scope, but the old JIT-only integer FFI failure mode is gone on the native path.
GPU. PTX codegen exists in self-hosted/gpu/ but there is no end-to-end compilation path from the CLI. 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 = {1.0.0-beta.6},
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.
<p align="center"><em>At the horizon of certainty, where ancient columns meet the endless sea.</em></p> <p align="center">SOUNIO</p>