Ο μεταγλωττιστής που
μεταγλωττίζει τον εαυτό του.
Το souc είναι γραμμένο στη Sounio. Το bootstrap ξεκινά με seed binary μεταγλωττισμένο σε C, περνά από τρία στάδια και ολοκληρώνεται όταν τα στάδια 2 και 3 παράγουν πανομοιότυπη έξοδο SHA-256. Το fixed point είναι το τεκμήριο αυτοσυνέπειας.
Effects live in the signature
The checker reads colour before you read the name.
Nine algebraic effects, plus linear as a type qualifier. A solid border is written in
with. A dashed border is recovered from a callee. A struck badge is no longer
live in this frame. A function without with IO cannot call one that has it.
fn read_sensor () -> Knowledge<f64> with IO Observe
website/src/pages/language.astro · effectsExample · subset rule, not a handler
fn calibrate (sensor: &!Sensor, bias: f64) with Mut
with &! is exclusive mutation, not Rust &mut. The three
renderings are the badge vocabulary. This page does not claim Sounio has effect handlers.
Tokens: --color-effect-{io,mut,div,panic,alloc,async,gpu,prob,observe} and
--color-type-linear. Linear is a type qualifier, not a tenth effect.
Bootstrap σε τρία στάδια.
Δεν απαιτείται εμπιστοσύνη στο seed binary. Η αναπαραγωγιμότητα είναι η εγγύηση: αν τα gen2.elf και gen3.elf διαφέρουν, ο compiler έχει σφάλμα.
Stage 0
Seed μεταγλωττισμένο σε C
Ελάχιστη υλοποίηση σε C του parser και emitter της Sounio. Η μοναδική της εργασία είναι να μεταγλωττίσει το lean_single.sio σε λειτουργικό binary. Δεν θεωρείται έμπιστη μετά το στάδιο 1.
Stage 1
Πρώτο self-hosted στάδιο
Το seed binary μεταγλωττίζει το lean_single.sio σε gen1.elf. Αυτό είναι το πρώτο binary της Sounio που μεταγλωττίστηκε από τη Sounio.
Stage 2 ≡ Stage 3
Επαληθευμένο fixed point
gen1.elf → gen2.elf και μετά gen2.elf → gen3.elf. Τα SHA-256 των δύο πρέπει να είναι πανομοιότυπα. Αυτό είναι το τεκμήριο αυτοσυνέπειας του compiler.
Εκτελέστε το μόνοι σας
# Stage 0 → 1: C seed compiles the Sounio compiler
./artifacts/self-hosted/souc-self-hosted-x86_64 \
self-hosted/compiler/lean_single.sio gen1.elf
# Stage 1 → 2: first self-hosted compile
./gen1.elf self-hosted/compiler/lean_single.sio gen2.elf
# Stage 2 → 3: fixed-point check
./gen2.elf self-hosted/compiler/lean_single.sio gen3.elf
# These two SHA-256 digests must be identical.
sha256sum gen2.elf gen3.elfΤέσσερις φάσεις του compiler.
Κάθε φάση είναι ξεχωριστό module στο self-hosted/compiler/. Οι επιστημικοί τύποι παρακολουθούνται σε κάθε φάση· το confidence lattice δεν διαγράφεται ανάμεσα στο HLIR και το emit.
Ανάλυση (Parse)
parser/items.sio
Parser recursive descent. Παράγει unresolved AST με annotations effects, clauses where και δηλώσεις algebra. Δεν υπάρχει σιωπηρή ανάκτηση tokens — κακοσχηματισμένη είσοδος είναι hard error.
Έλεγχος (Check)
check/mod.sio
Type checker με bidirectional inference. Επιλύει widening του Knowledge<T>, ενοποίηση effect rows και περιορισμούς confidence gates. Όλες οι επιστημικές υποχρεώσεις διεκπεραιώνονται εδώ ή απορρίπτονται με typed error.
HLIR
hlir/mod.sio
High-level intermediate representation. Εδώ εκτελείται rewriting e-graph με περισσότερους από 1000 κανόνες. Η διάδοση αβεβαιότητας GUM χαμηλώνεται σε explicit variance-carrying nodes πριν από το emit.
Παραγωγή (Emit)
emit/mod.sio
Backend dispatcher. Η διαθέσιμη διαδρομή είναι native x86_64 (System V ABI, static Linux ELF). Η GPU διαδρομή παράγει PTX μόνο για σκελετό ονομασμένων kernel patterns (TOUR.md §6). Οι linear types επιβάλλουν κάθε resource να καταναλώνεται ακριβώς μία φορά.
Ένας διαθέσιμος στόχος.
Ο compiler στοχεύει μόνο Linux x86-64 (TOUR.md §6). Το epistemic layer δεν είναι runtime library — χαμηλώνεται στον ίδιο machine code που μεταφέρει τον υπολογισμό. Οι άλλοι emitters στο source tree είναι προσχέδια ή σκελετοί και παρατίθενται ώστε η κατάστασή τους να μην υπερερμηνεύεται.
x86_64
Διαθέσιμο
System V ABI. Ο κύριος στόχος ανάπτυξης και παραγωγής. Το souc εκτελείται εδώ. Η confidence του Knowledge<T> αποθηκεύεται ως struct field· η διάδοση GUM μεταγλωττίζεται σε scalar arithmetic.
ARM64, macOS, WASM
Δεν διατίθεται
Μη υποστηριζόμενοι στόχοι. Τα binaries είναι static Linux ELF και δεν εκτελούνται σε macOS. Το WASM backend είναι blocked draft (#2237). Το Cranelift JIT δεν διατίθεται πλέον (CHANGELOG 2.1.0).
PTX
Σκελετός εκπομπής
souc build --backend gpu παράγει έγκυρο PTX για σκελετό named kernel patterns: kernels με κενά bodies, χωρίς arithmetic και χωρίς memory access (μετρήθηκε 2026-10-04, examples/kernel_vec_add.sio). Δεν είναι γενικός GPU backend.
Lean 4 για τις δύσκολες αποδείξεις.
Εκεί όπου ο type checker επιβάλλει, το Lean επαληθεύει. Οι δύο βασικές ιδιότητες του epistemic type system — GUM conservativity και confidence monotonicity — διατυπώνονται ως θεωρήματα και αποδεικνύονται στο formal/EpistemicEffects.lean.
gum_conservativity
Αποδεδειγμένο
Η διάδοση αβεβαιότητας GUM μέσω αριθμητικής δεν αυξάνει ποτέ την confidence. Σύνθεση επιστημικών πράξεων δεν μπορεί να κατασκευάσει βεβαιότητα που δεν υπήρχε στις εισόδους.
confidence_monotonicity
Αποδεδειγμένο
Το widening μιας τιμής Knowledge<T> (αύξηση του ε) δεν μπορεί να παράγει στενότερο confidence interval. Η διάταξη του confidence lattice είναι monotone σε όλες τις type operations.
substitution_lemma
Ανοιχτή υποχρέωση
Η substitution επιστημικών values σε effect-typed terms διατηρεί το effect row. Η δομή της απόδειξης υπάρχει· απομένει μία υποχρέωση indexed induction.
Πηγή:
formal/lean4/EpistemicEffects.lean
(589 lines, 0 sorry).