On this page
Language

What the language does.
What it doesn’t. Exactly.

Four things Sounio gives you that other languages don’t. Anything not on this page is either scaffolding or missing — /proof has the honest status.

Sounio is a statically typed, natively compiled systems language. Its contribution relative to Rust (ownership / linearity), Koka (algebraic effects), and Lean (verified computation) is the epistemic dimension: gradual confidence typing, GUM uncertainty propagation, and confidence gates — all enforced by the compiler, not by convention or runtime library.

The project behind this language is described in about the Sounio programming language. What is still underway is on the Sounio programming language roadmap.

A

Confidence survives every operation.

Every value in Sounio can carry the evidence behind it. The type system enforces this at compile time — not as a lint, not as a runtime check.

Knowledge<T>

The base epistemic type. Wraps any value with a confidence level ε ∈ [0, 1], an uncertainty interval, and a provenance string. GUM uncertainty propagates automatically through arithmetic.

Knowledge<f64>, Knowledge<mg>

Validated<T>

A distinct type that can only be produced by passing a formal confidence gate. Cannot be confused with raw measurements. Confidence-gated execution branches on Validated vs. raw.

fn prescribe(d: Validated<f64, ε >= 0.82>)

Unobserved<T>

Values remain quantum-indeterminate until a comparison or I/O boundary collapses them. Bayesian and quantum measurement semantics live in the type system, not in runtime libraries.

fn observe(x: Unobserved<f64>) -> bool with Observe

Intervention<T> & Counterfactual<T>

Compiler-level types that carry causal confidence. Intervention<T> corresponds to Pearl's do-operator; Counterfactual<T> encodes hypothetical reasoning under the same discipline as observational data.

do(X = x): Intervention<f64>

Knowledge<T> progression — bare numeric to fully epistemic

  1. Tier 1

    T

    Raw scalar or structured value with no attached evidence metadata.

  2. Tier 2

    Quantity<T, Unit>

    Value promoted to dimension-aware representation with unit constraints.

  3. Tier 3

    Knowledge<T>

    Uncertainty, confidence, and source attribution become part of the value.

  4. Tier 4

    Knowledge<T, Provenance>

    Executable value with traceability chain for audit and reproducibility.

Confidence-gated execution

confidence_gate.sio 
let dose: Knowledge<f64> = Knowledge(
  500.0,
  ε=0.97,
  prov="lab_run_042"
)

// Confidence gate: only passes if ε >= 0.82
if dose.ε >= 0.82 {
  prescribe(dose)           // type: Knowledge<f64>
} else {
  request_remeasurement()
}

DIAGNOSTIC, IN FULL

E250 refuses the call. The complete help text is shown.

Before #1784 the print path kept 127 characters and dropped the rest without failing. #1794 counted 33 user-facing diagnostics over that cap — every one was cut — and the historical CI logs that quote them are incomplete in the tails. E219 was the longest casualty: 206 characters gone, mid-word, so the implemented names after st… never reached the user. The span, the code, and the tail are the diagnostic.

tests/compile-fail/extern_c_unimplemented_builtin.sio
MadarosIOE250Refused
19extern "C" {
20    fn malloc(size: i64) -> i64;
21    fn abs(x: i64) -> i64;
22}
23
24fn main() -> i64 with IO {
25    let p = malloc(64)
26    print_int(p)
27    print_int(abs(0 - 7))
28    0
29}
E250--> tests/compile-fail/extern_c_unimplemented_builtin.sio:27:15

error[E250]: call to an `extern "C"` function the native backend does not implement

| = help: only these body-less names are implemented: print, print_int, print_char, print_f64, get_arg, get_arg_count, stcut 127r_len, str_char_at, str_eq, str_slice, starts_with, str_concat, str_from_bytes, read_file, write_file, file_size, sqrt, exp, log, sin, cos, assert, heap_alloc, heap_free, f64_to_bits, bits_to_f64, syscall6, malloc, free, getpid, getppid, exit, abort, system, read_i64, write_i64, read_f64, write_f64

= note: there is no dynamic linker in this backend; an unimplemented extern compiles to an empty stub whose calls read 0

Help literal 427 characters · pre-#1784 would keep 127 and drop 300

The live span is abs, not malloc: P0-F allow-listed malloc. #1801 then closed two sites that still fabricated after a refusal — the checker used to keep the declared i64 so abs() + 1 type-checked, and an empty IR stub used to fall through and read 0. Refusal is the whole object: code, span, full text, infected type, no zero.

Algebra declarations

Declare algebraic laws on types. The e-graph optimizer uses only the rewrites your algebra permits — no unsound reordering of non-commutative ops. 

algebra Octonion over f64 {
  add: commutative, associative
  mul: alternative, non_commutative
  reassociate: fano_selective
}

Units & dimensional analysis

Units are checked at compile time. A value declared as mg cannot be silently coerced to kg or dimensionless. Dimensional analysis and GUM propagation are set out in the guide to units and uncertainty. Refinement predicates (e.g. x > 0) work today; SMT integration is planned. 

let dose: mg = 500.0
let weight: kg = 78.5
// let wrong = dose + weight  ← compile error: mg + kg

GUM propagation — uncertainty flows automatically

1

Measure

Capture value + uncertainty + confidence from instrument or model.

2

Propagate

Composition rules carry uncertainty through transformations.

3

Evaluate

Confidence thresholds and effect policies decide admissibility.

4

Act

Execution continues only when evidence satisfies gate criteria.

B

Side effects live in the signature.

Side effects are visible in function signatures. Linear types enforce exactly-once resource consumption. Neither requires runtime overhead.

Built-in effects

with IO File, network, stdin/stdout — any real-world I/O.
with Panic Controlled abort path. Functions without Panic cannot panic.
with Observe Collapses Unobserved<T> to a concrete value — separates measurement from computation.
with Async Async/await, channels, spawn. Phase 1 wired (channel + send/recv + spawn); full scheduler pending.
with GPU Kernel launch, memory transfer. Syntax integrated; end-to-end path requires CUDA driver.
with Probabilistic Monte Carlo sampling, Bayesian updates. In stdlib; effect annotation enforces separation from deterministic code.

The subset rule

A function's effects must be a subset of its caller's declared effects. A function without with IO cannot call a function that has it. This is checked by the type checker, not at runtime.

Linear structs

A linear struct must be consumed exactly once — it cannot be copied, dropped silently, or moved into two branches. File handles, network connections, and cryptographic contexts are the canonical use case.

effects_and_linear.sio 
// Effects are part of the signature — callee effects must
// be a subset of the caller's declared effects.
fn read_sensor() -> Knowledge<f64> with IO, Observe {
    let raw = read_port(0x3F8)          // requires IO
    return observe(raw)                  // requires Observe
}

// Linear struct: the handle must be consumed exactly once.
linear struct FileHandle { fd: i32 }

fn close(h: FileHandle) with IO {
    syscall_close(h.fd)                 // h is consumed here
}
C

The compiler compiles itself.

The compiler is self-hosted: written in Sounio, it compiles Sounio. The bootstrap chain is verified — stage 2 and stage 3 produce byte-for-byte identical binaries.

Compilation pipeline

Step 1

Source + Types

Parser, refinement checks, and uncertainty-aware typing.

Step 2

IR + Effects

Lowering and effect analysis with provenance retention.

Step 3

Backend Select

Native and GPU target selection with capability checks.

Step 4

Runtime Evidence

Execution outputs with confidence and traceability context.

Pipeline stages

Source → Lexer → Parser Recursive-descent parser. No external parser generator.
AST → Check Bidirectional type inference + effect analysis. Knowledge<T> subtyping, confidence gates, linear resource tracking.
Check → HIR → SIR High-level IR, then Static IR (SSA form). Epistemic metadata preserved through lowering.
SIR → HLIR (e-graph) 1,000+ algebraic rewrite rules. Algebra declarations constrain which rewrites apply.
HLIR → ELF (x86-64) Native code generation. No LLVM. Bootstrap chain: C → gen1 → gen2 → gen3 (fixed point).

Reproducing the self-hosting fixed point 

# Stage 0: C compiler compiles the first Sounio compiler
./artifacts/self-hosted/souc-self-hosted-x86_64 \
    self-hosted/compiler/lean_single.sio gen1.elf

# Stage 1 → Stage 2: first self-hosted compile
./gen1.elf self-hosted/compiler/lean_single.sio gen2.elf

# Stage 2 → Stage 3: fixed-point check
./gen2.elf self-hosted/compiler/lean_single.sio gen3.elf

# Must be identical — this is the fixed point.
sha256sum gen2.elf gen3.elf

Achieved 2026-03-23. Recorded SHA-256 (CHANGELOG): 7b588877f870… (741 KB). See /proof §2 for the full verification.

E-graph optimizer

The optimizer implements equality saturation over an e-graph — the same approach used by egg/egglog but running inside a Sounio compiler written in Sounio. 1,000+ algebraic rewrite rules, all at FAIL=0 in the test gate. Algebra declarations constrain which rewrites apply per type.

Common commands

$ souc check file.sio Type-check; no output generated.
$ souc run file.sio Compile to temp ELF, execute, clean up.
$ souc compile file.sio -o out.elf Direct native compilation to ELF.
$ souc check --show-types file.sio Dump inferred types (JIT mode only).
D

What is wired. What is not.

What is and isn't wired up end-to-end. The anti-slop move is to say this explicitly before the reader discovers it.

Same contract as the homepage and README.md — regenerated from artifacts.

Stdlib 可靠性門控: stdlib reliability · not in CI · artifact 2026-05-12 · engine unnamed · 來源: artifacts/stdlib/stdlib_reliability_status.v1.json

正常運行

  • Epistemic core — Knowledge[T] with GUM propagation, provenance tracking, and compile-time confidence gates (vancomycin fixtures)
  • Self-hosted compiler — Fixed-point verified (cycle parity=true); 172 self-hosted source files
  • Algebra — Clifford, Cayley-Dickson, octonions — 168 theorem verified computationally
  • Native codegen — Linux x86-64 static ELF only (TOUR.md section 6); no macOS, Windows or AArch64 target ships
  • Optimizer — 1,000+ e-graph rewrite rules with FAIL=0 in optimizer tests
  • Language server — LSP smoke gate pass; hover, defs, refs, rename, formatting, semantic tokens
  • Closure literals — Named function refs and closure tests in tests/run-pass/ (see README resolved list)

腳手架/草圖

  • Stdlib end-to-end tests — Stdlib end-to-end: 196 of 533 test programs pass (165 fail, 172 skipped), measured 2026-10-06 with `bash scripts/stdlib/run_stdlib_e2e.sh`; result in `artifacts/stdlib/stdlib_e2e_result.v1.json`
  • Theorem prover — Large arena and data structures; full inference logic not complete
  • Epistemic modules — Many modules are signatures with minimal bodies (~70% scaffolding)
  • Neural networks — Quaternion/octonion NN lanes exist but are not all end-to-end stable
  • Genomics — Several files are stubs disabled on parser limitations
  • Async runtime — Self-hosted async tests pass per KNOWN_LIMITATIONS.md; broader runtime integration still partial
  • Geometry engine — Extended geometry paths disabled; core engine partial

缺失

  • Epistemic ODE solver (general RHS) — Exponential decay works; general RHS needed for full PBPK epistemic integration
  • Ontology federation — Local ontology work exists; 15M-term federated query not implemented
  • General GPU backend — `souc build --backend gpu` emits PTX for a skeleton of named kernel patterns (empty bodies), not a general GPU backend (TOUR.md section 6)
  • Windows, macOS and AArch64 — Not targeted: the compiler emits Linux x86-64 static ELF only
  • WASM backend — Blocked draft (#2237); not shipped
  • Checked launcher REPL — README Known Limitations: bin/souc does not expose repl; separate REPL beta exists outside default lane

GPU path

Kernel syntax is integrated into the language — a Sounio function annotated with GPU compiles to PTX via a backend bridge. The world's first GUM uncertainty propagation through a GPU WMMA kernel is verified in tests/stdlib/gpu/ (GPU public contract · not in CI · artifact 2026-03-09 · engine unnamed). The end-to-end driver path requires a CUDA-capable host — gpu/lib.sio is currently an empty stub.

Test gate snapshot

Stdlib reliability gate: stdlib reliability · not in CI · artifact 2026-05-12 · engine unnamed See /proof §4.

Getting started Honest status → Language guide (docs) →