A local development server for the Sounio programming language, which bills itself as a systems language with epistemic types for uncertainty propagation and scientific computing. The server wraps the souc compiler toolchain to check syntax, compile .sio source files to native ELF binaries, run executables, and execute test suites without leaving your editor. Useful if you're experimenting with Sounio's Knowledge types or algebraic effect system and want inline feedback on whether your confidence thresholds and GUM propagation actually compile. The language itself is in beta and self hosted, so expect a moving target. This is for people who want to try a research language with first class uncertainty tracking, not a production toolchain.
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.
Keywords: systems programming language, scientific computing language, epistemic types, uncertainty propagation, algebraic effects, self-hosted compiler, formal verification, non-associative algebra, octonions, e-graphs.
| 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.
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-networksWorkflow split:
.sio implementation scaffolding.data/cpc2026/sounio_input/.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
./sounio-whereami --quick/workspace/sounio as the active remote-first workspace pathbash scripts/dev/measure_repo_scale.shThis 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.
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 self-hosted compiler 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).
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.
// 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
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
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.
| 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) |
| 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 |
| 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/.
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.
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. 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 self-hosted/compiler/lean_single.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
For detailed setup: INSTALL.md · docs/guide/MINIMUM_VIABLE_SOUNIO.md
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.
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/ |
See docs/MANIFESTO.md for the full philosophy.
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
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}
}
Apache-2.0. See LICENSE.
At the horizon of certainty, where ancient columns meet the endless sea.
SOUNIO