Odel
Sounio Compiler

Sounio Compiler

Local
@sounio-lang6LeanApache-2.0Updated Today

Check, compile, run, and test Sounio programs locally.

Sounio

SOUNIO

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

Sounio Website Playground Version 2.1.0 Apache-2.0 License ~6.1k tracked .sio files; see SCALE.md

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.

Technical Pillars & Core Keywords

PillarDescriptionKey Search Terms
Epistemic ComputingBuilt-in confidence-gated execution tracking and provenance tracking.epistemic-computing, Knowledge[T], confidence-threshold
Uncertainty PropagationGUM-compliant (Guide to the Expression of Uncertainty in Measurement) error propagation.uncertainty-propagation, GUM-compliance, error-propagation
Systems & ScienceNative x86_64 ELF compilation, self-hosted compiler loop, PTX/GPU acceleration.systems-programming, scientific-computing, ptx-codegen
Algebraic EffectsExplicit side-effects declarations (IO, Mut, Div, Panic, Alloc).algebraic-effects, effect-system, effects-with
Mathematical RigorNon-associative octonion basis associators, formalized Lean 4 proofs of invariants.non-associative-algebra, octonions, lean4-proofs
Dimensional AnalysisCompile-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 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

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.cboot2g.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-07-11): 6,130 tracked .sio files, ~2.21M lines (bash scripts/dev/measure_repo_scale.sh). The self-hosted compiler alone is ~555k lines — not a small experiment. Full audit: docs/audit/README.md · SCALE.md.

What WORKS (evidence-backed lanes)

ComponentStatusEvidence
Epistemic coreKnowledge[T] + GUM + provenanceNamed package / conformance gates
Self-hosted compilerLexer → codegen; fixed-point bootstraplean_single fixed-point + native-v2 spine gates
OntologyGenerated bundles + validation harnessrun_ontology_validation.sh + compile gates
Native codegenLinux ELF; Mach-O artifact laneSelf-host + native-v2 gates
Core stdlib slicesStats, linalg, ODE, etc.stdlib_science_pipeline_gate, reliability inventory
Language serverLSP 3.17 subsetRelease binary + protocol tests (prototype per registry)

What's SCAFFOLDING or PARTIAL

ComponentReality
~46% of stdlib modulesClassified scaffold in audit A.2 — code without executable proof
32 stdlib smoke testsPrint FOO_OK only; do not exercise module logic
129 CI gate scriptsMost are not on make check / GitHub CI (audit A.4)
GPU CLI pathPTX/kaxi code exists; end-to-end CLI path incomplete
Theorem prover / async / geometryLarge or stub surfaces — see module audit JSON

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

TierModulesMeaning
works66Tests, gates, or mass with executable evidence
scaffold59Code present; no direct executable proof in tree
doc-only roots3Non-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 Linux ELF artifacts; macOS is a cross-compile target rather than a host-native binary lane. 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 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
$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

DirectoryPurpose
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

  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. 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, 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.

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.

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

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   = {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