Σε αυτή τη σελίδα

Γλώσσα

Τι κάνει η γλώσσα.
Τι δεν κάνει. Ακριβώς.

Τέσσερα πράγματα που σας δίνει η Sounio και δεν δίνουν άλλες γλώσσες. Ό,τι δεν υπάρχει σε αυτή τη σελίδα είναι είτε scaffolding είτε απουσιάζει — το /proof δίνει την ειλικρινή κατάσταση.

Η Sounio είναι statically typed, native-compiled γλώσσα συστημάτων. Η συμβολή της σε σχέση με Rust (ownership/linearity), Koka (algebraic effects) και Lean (verified computation) είναι η επιστημική διάσταση: gradual confidence typing, διάδοση αβεβαιότητας GUM και confidence gates — όλα επιβαλλόμενα από τον compiler, όχι από σύμβαση ή runtime library.

Το έργο πίσω από τη γλώσσα περιγράφεται στη σελίδα σχετικά με τη Sounio. Τα ορόσημα που απομένουν είναι στην πορεία ανάπτυξης της Sounio.

Η εμπιστοσύνη επιβιώνει σε κάθε πράξη.

Κάθε τιμή στη Sounio μπορεί να μεταφέρει τα τεκμήρια που τη στηρίζουν. Το σύστημα τύπων το επιβάλλει κατά τη μεταγλώττιση — όχι ως lint και όχι ως runtime check.

Knowledge<T>

Ο βασικός επιστημικός τύπος. Τυλίγει κάθε τιμή με επίπεδο εμπιστοσύνης ε ∈ [0, 1], διάστημα αβεβαιότητας και συμβολοσειρά provenance. Η αβεβαιότητα GUM διαδίδεται αυτόματα μέσω της αριθμητικής.


Knowledge<f64>, Knowledge<mg>

Validated<T>

Ξεχωριστός τύπος που παράγεται μόνο αφού περάσει formal confidence gate. Δεν συγχέεται με raw measurements. Η εκτέλεση με confidence gate διακλαδώνεται μεταξύ Validated και raw τιμών.


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

Unobserved<T>

Οι τιμές παραμένουν quantum-indeterminate έως ότου μια σύγκριση ή ένα όριο I/O τις καταστήσει συγκεκριμένες. Η σημασιολογία Bayesian και quantum measurement ανήκει στο σύστημα τύπων, όχι σε runtime libraries.


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

Intervention<T> & Counterfactual<T>

Τύποι επιπέδου compiler που μεταφέρουν αιτιώδη εμπιστοσύνη. Το Intervention<T> αντιστοιχεί στον do-operator του Pearl· το Counterfactual<T> κωδικοποιεί υποθετικό συλλογισμό με την ίδια πειθαρχία όπως τα observational data.


do(X = x): Intervention<f64>

Εξέλιξη Knowledge<T> — από απλό αριθμό σε πλήρως επιστημική τιμή

Tier 1
T

Raw scalar or structured value with no attached evidence metadata.
Tier 2
Quantity<T, Unit>

Value promoted to dimension-aware representation with unit constraints.
Tier 3
Knowledge<T>

Uncertainty, confidence, and source attribution become part of the value.
Tier 4
Knowledge<T, Provenance>

Executable value with traceability chain for audit and reproducibility.

Εκτέλεση με confidence gate

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()
}

output

ΔΙΑΓΝΩΣΤΙΚΟ, ΟΛΟΚΛΗΡΟ

Το E250 αρνείται την κλήση. Το πλήρες κείμενο βοήθειας εμφανίζεται.

Πριν το #1784 η εκτύπωση κρατούσε 127 χαρακτήρες. Το #1794 μέτρησε 33 διαγνωστικά πάνω από αυτό το όριο — όλα κομμένα — και τα ιστορικά CI logs είναι ελλιπή στις ουρές. Το E219 έχασε 206 χαρακτήρες στη μέση της λέξης.

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

Το ζωντανό span είναι το abs, όχι η malloc. Το #1801 έκλεισε δύο σημεία που συνέχιζαν να κατασκευάζουν μετά την άρνηση.

Δηλώσεις άλγεβρας

Δηλώστε αλγεβρικούς νόμους για τους τύπους. Ο e-graph optimizer χρησιμοποιεί μόνο τα rewrites που επιτρέπει η άλγεβρά σας — χωρίς μη έγκυρη αναδιάταξη μη αντιμεταθετικών πράξεων.

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

Μονάδες και διαστατική ανάλυση

Οι μονάδες ελέγχονται κατά τη μεταγλώττιση. Μια τιμή που δηλώνεται ως mg δεν μπορεί να μετατραπεί σιωπηρά σε kg ή σε dimensionless. Η διαστατική ανάλυση και η διάδοση GUM περιγράφονται στον οδηγό για μονάδες και αβεβαιότητα. Τα refinement predicates (π.χ. x > 0) λειτουργούν σήμερα· η ενσωμάτωση SMT έχει προγραμματιστεί.

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

Διάδοση GUM — η αβεβαιότητα ρέει αυτόματα

Measure

Capture value + uncertainty + confidence from instrument or model.

Propagate

Composition rules carry uncertainty through transformations.

Evaluate

Confidence thresholds and effect policies decide admissibility.

Act

Execution continues only when evidence satisfies gate criteria.

Οι επιδράσεις ανήκουν στην υπογραφή.

Οι παρενέργειες είναι ορατές στις υπογραφές των συναρτήσεων. Οι γραμμικοί τύποι επιβάλλουν κατανάλωση πόρων ακριβώς μία φορά. Κανένα από τα δύο δεν απαιτεί runtime overhead.

Ενσωματωμένες επιδράσεις

with IO Αρχεία, δίκτυο, stdin/stdout — κάθε I/O με τον πραγματικό κόσμο.

with Panic Ελεγχόμενη διαδρομή abort. Συναρτήσεις χωρίς Panic δεν μπορούν να προκαλέσουν panic.

with Observe Μετατρέπει το Unobserved<T> σε συγκεκριμένη τιμή — διαχωρίζει τη μέτρηση από τον υπολογισμό.

with Async Async/await, κανάλια και spawn. Η Φάση 1 είναι συνδεδεμένη (channel + send/recv + spawn)· ο πλήρης scheduler εκκρεμεί.

with GPU Εκκίνηση kernel και μεταφορά μνήμης. Η σύνταξη είναι ενσωματωμένη· η διαδρομή από άκρο σε άκρο απαιτεί CUDA driver.

with Probabilistic Monte Carlo sampling και Bayesian ενημερώσεις. Υπάρχει στη stdlib· η annotation διαχωρίζει τον πιθανοτικό από τον ντετερμινιστικό κώδικα.

Ο κανόνας του υποσυνόλου

Οι επιδράσεις μιας συνάρτησης πρέπει να είναι υποσύνολο των δηλωμένων effects του caller. Μια συνάρτηση χωρίς with IO δεν μπορεί να καλέσει συνάρτηση που το έχει. Αυτό ελέγχεται από τον type checker, όχι στο runtime.

Γραμμικές δομές

Μια linear struct πρέπει να καταναλωθεί ακριβώς μία φορά — δεν μπορεί να αντιγραφεί, να απορριφθεί σιωπηρά ή να μετακινηθεί σε δύο branches. File handles, συνδέσεις δικτύου και cryptographic contexts είναι οι χαρακτηριστικές χρήσεις.

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
}

output

Ο compiler μεταγλωττίζει τον εαυτό του.

Ο compiler είναι self-hosted: γραμμένος σε Sounio, μεταγλωττίζει Sounio. Η αλυσίδα bootstrap έχει επαληθευτεί — το stage 2 και το stage 3 παράγουν δυαδικά αρχεία πανομοιότυπα byte προς byte.

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

Source → Lexer → Parser Αναδρομικός parser καθόδου. Δεν χρησιμοποιείται εξωτερικός parser generator.

AST → Check Αμφίδρομη inference τύπων και ανάλυση effects. Υποτύποι Knowledge<T>, confidence gates και παρακολούθηση γραμμικών πόρων.

Check → HIR → SIR High-level IR και στη συνέχεια Static IR (μορφή SSA). Τα επιστημικά μεταδεδομένα διατηρούνται στο lowering.

SIR → HLIR (e-graph) Πάνω από 1.000 αλγεβρικοί κανόνες rewrite. Οι algebra declarations περιορίζουν ποια rewrites επιτρέπονται.

HLIR → ELF (x86-64) Native code generation χωρίς LLVM. Αλυσίδα bootstrap: C → gen1 → gen2 → gen3 (fixed point).

Αναπαραγωγή του 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

Επιτεύχθηκε στις 2026-03-23. Καταγεγραμμένο SHA-256 (CHANGELOG): 7b588877f870… (741 KB). Δείτε /proof §2 για την πλήρη επαλήθευση.

E-graph optimizer

Ο optimizer υλοποιεί equality saturation πάνω σε e-graph — την ίδια προσέγγιση με τα egg/egglog, αλλά μέσα σε compiler της Sounio γραμμένο σε Sounio. Πάνω από 1.000 αλγεβρικοί κανόνες rewrite, όλοι με FAIL=0 στο test gate. Οι algebra declarations περιορίζουν ποια rewrites εφαρμόζονται ανά τύπο.

Συνηθισμένες εντολές

$ souc check file.sio Έλεγχος τύπων· δεν παράγεται έξοδος.

$ souc run file.sio Compile σε προσωρινό ELF, εκτέλεση και καθαρισμός.

$ souc compile file.sio -o out.elf Άμεση native μεταγλώττιση σε ELF.

$ souc check --show-types file.sio Εμφάνιση των inferred types (μόνο σε JIT mode).

Τι είναι συνδεδεμένο. Τι δεν είναι.

Τι είναι και τι δεν είναι συνδεδεμένο από άκρο σε άκρο. Η σοβαρή τεχνική τεκμηρίωση το δηλώνει ρητά πριν το ανακαλύψει ο αναγνώστης.

Το ίδιο συμβόλαιο με την αρχική σελίδα και το README.md — αναδημιουργείται από 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

Η σύνταξη kernel είναι ενσωματωμένη στη γλώσσα — μια συνάρτηση Sounio με annotation with GPU μεταγλωττίζεται σε PTX μέσω backend bridge. Η διάδοση αβεβαιότητας GUM μέσω GPU WMMA kernel επαληθεύεται στο tests/stdlib/gpu/ (GPU public contract · not in CI · artifact 2026-03-09 · engine unnamed). Η διαδρομή driver από άκρο σε άκρο απαιτεί host με CUDA — το gpu/lib.sio είναι επί του παρόντος κενό stub.

Snapshot του test gate

Reliability gate της stdlib: stdlib reliability · not in CI · artifact 2026-05-12 · engine unnamed Δείτε /proof §4.

Ξεκινήστε Ειλικρινής κατάσταση → Οδηγός γλώσσας (docs) →

Τι κάνει η γλώσσα.Τι δεν κάνει. Ακριβώς.

Η εμπιστοσύνη επιβιώνει σε κάθε πράξη.

Knowledge<T>

Validated<T>

Unobserved<T>

Intervention<T> & Counterfactual<T>

T

Quantity<T, Unit>

Knowledge<T>

Knowledge<T, Provenance>

Το E250 αρνείται την κλήση. Το πλήρες κείμενο βοήθειας εμφανίζεται.

Δηλώσεις άλγεβρας

Μονάδες και διαστατική ανάλυση

Measure

Propagate

Evaluate

Act

Οι επιδράσεις ανήκουν στην υπογραφή.

Ενσωματωμένες επιδράσεις

Ο κανόνας του υποσυνόλου

Γραμμικές δομές

Ο compiler μεταγλωττίζει τον εαυτό του.

Source + Types

IR + Effects

Backend Select

Runtime Evidence

Στάδια pipeline

E-graph optimizer

Συνηθισμένες εντολές

Τι είναι συνδεδεμένο. Τι δεν είναι.

Ειλικρίνεια χρόνου εκτέλεσης (συγχρονισμένη)

Λειτουργεί

Σκαλωσιά

Λείπει

Διαδρομή GPU

Snapshot του test gate

Τι κάνει η γλώσσα.
Τι δεν κάνει. Ακριβώς.