Add live self-hosting bootstrapper page to bootstrappers section
All checks were successful
Build and Deploy / build-and-deploy (push) Successful in 2m15s
All checks were successful
Build and Deploy / build-and-deploy (push) Successful in 2m15s
- Update plan page with completion status and results - Add ~bootstrapper-self-hosting-content component with live G0/G1 verification - Add _self_hosting_data() helper: loads py.sx, runs it, diffs against G0 - Add "Self-Hosting (py.sx)" to bootstrappers nav and index table - Wire /bootstrappers/self-hosting route Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
@@ -1,10 +1,25 @@
|
||||
;; ---------------------------------------------------------------------------
|
||||
;; Self-Hosting Bootstrapper — py.sx
|
||||
;; Self-Hosting Bootstrapper — py.sx (COMPLETE)
|
||||
;; ---------------------------------------------------------------------------
|
||||
;; @css bg-green-100 text-green-800 bg-green-50 border-green-200 text-green-700 text-green-600
|
||||
|
||||
(defcomp ~plan-self-hosting-bootstrapper-content ()
|
||||
(~doc-page :title "Self-Hosting Bootstrapper"
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Status banner
|
||||
;; -----------------------------------------------------------------------
|
||||
|
||||
(div :class "rounded-lg bg-green-50 border border-green-200 p-4 mb-8"
|
||||
(div :class "flex items-center gap-3"
|
||||
(span :class "inline-flex items-center rounded-full bg-green-100 px-3 py-1 text-sm font-semibold text-green-800"
|
||||
"Complete")
|
||||
(p :class "text-green-700 text-sm"
|
||||
(code "py.sx") " is implemented and verified. G0 == G1: 128/128 defines match, "
|
||||
"1490 lines, 88,955 bytes — byte-for-byte identical. "
|
||||
(a :href "/bootstrappers/self-hosting" :class "underline text-green-600 font-medium"
|
||||
"See live verification."))))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; The Idea
|
||||
;; -----------------------------------------------------------------------
|
||||
@@ -16,13 +31,44 @@
|
||||
(p "We also have " (code "z3.sx") " — a translator written in SX itself that "
|
||||
"converts SX spec declarations into SMT-LIB for Z3. It's proof that "
|
||||
"SX can generate code in another language.")
|
||||
(p "The next step: " (strong "py.sx") " — an SX-to-Python translator written in SX. "
|
||||
(p (strong "py.sx") " — an SX-to-Python translator written in SX. "
|
||||
"Feed it through the existing Python evaluator against the spec files and it produces "
|
||||
(code "sx_ref.py") ". The bootstrapper bootstraps itself.")
|
||||
(p "If " (code "py.sx") " produces output identical to " (code "bootstrap_py.py")
|
||||
", the Python bootstrapper becomes redundant. "
|
||||
(p (code "py.sx") " produces output identical to " (code "bootstrap_py.py")
|
||||
". The Python bootstrapper is redundant. "
|
||||
"The spec defines itself."))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Results
|
||||
;; -----------------------------------------------------------------------
|
||||
|
||||
(~doc-section :title "Results" :id "results"
|
||||
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
|
||||
(table :class "w-full text-sm"
|
||||
(thead :class "bg-stone-50"
|
||||
(tr
|
||||
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Metric")
|
||||
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Value")))
|
||||
(tbody
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 text-stone-600" "py.sx size")
|
||||
(td :class "px-4 py-2 font-mono" "1,182 lines"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 text-stone-600" "bootstrap_py.py size (replaced)")
|
||||
(td :class "px-4 py-2 font-mono" "902 lines (PyEmitter class)"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 text-stone-600" "Defines translated")
|
||||
(td :class "px-4 py-2 font-mono" "128/128 exact match"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 text-stone-600" "Spec files processed")
|
||||
(td :class "px-4 py-2 font-mono" "7 (eval, forms, render, adapter-html, adapter-sx, deps, signals)"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 text-stone-600" "Output size")
|
||||
(td :class "px-4 py-2 font-mono" "1,490 lines / 88,955 bytes"))
|
||||
(tr :class "border-t border-stone-100 bg-green-50"
|
||||
(td :class "px-4 py-2 font-semibold text-green-700" "G0 == G1")
|
||||
(td :class "px-4 py-2 font-semibold text-green-700" "Identical (diff is empty)"))))))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Architecture
|
||||
;; -----------------------------------------------------------------------
|
||||
@@ -45,12 +91,12 @@
|
||||
(td :class "px-4 py-2" "Python (manual)")
|
||||
(td :class "px-4 py-2" (code "eval.sx") ", " (code "render.sx") ", ...")
|
||||
(td :class "px-4 py-2" (code "sx_ref.py")))
|
||||
(tr :class "border-t border-stone-100 bg-violet-50"
|
||||
(td :class "px-4 py-2 font-mono text-violet-700" "G1")
|
||||
(tr :class "border-t border-stone-100 bg-green-50"
|
||||
(td :class "px-4 py-2 font-mono text-green-700" "G1")
|
||||
(td :class "px-4 py-2" (code "py.sx"))
|
||||
(td :class "px-4 py-2" "Python evaluator + SX")
|
||||
(td :class "px-4 py-2" (code "eval.sx") ", " (code "render.sx") ", ...")
|
||||
(td :class "px-4 py-2" (code "sx_ref.py") " (identical)"))
|
||||
(td :class "px-4 py-2 font-semibold text-green-700" (code "sx_ref.py") " (identical)"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono text-stone-600" "G2")
|
||||
(td :class "px-4 py-2" (code "py.sx"))
|
||||
@@ -69,7 +115,9 @@
|
||||
(~doc-section :title "Translation Rules" :id "translation"
|
||||
|
||||
(~doc-subsection :title "Name Mangling"
|
||||
(p "SX identifiers become valid Python identifiers:")
|
||||
(p "SX identifiers become valid Python identifiers. "
|
||||
"The RENAMES dict (200+ entries) handles explicit mappings; "
|
||||
"general rules handle the rest:")
|
||||
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
|
||||
(table :class "w-full text-sm"
|
||||
(thead :class "bg-stone-50"
|
||||
@@ -94,29 +142,11 @@
|
||||
(td :class "px-4 py-2 font-mono" "set!")
|
||||
(td :class "px-4 py-2 font-mono" "set_b")
|
||||
(td :class "px-4 py-2" "! → _b"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "make-lambda")
|
||||
(td :class "px-4 py-2 font-mono" "make_lambda")
|
||||
(td :class "px-4 py-2" "platform function rename"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "type")
|
||||
(td :class "px-4 py-2 font-mono" "type_")
|
||||
(td :class "px-4 py-2" "Python reserved word escape"))))))
|
||||
|
||||
(~doc-subsection :title "Literals"
|
||||
(~doc-code :code (highlight "(define py-literal
|
||||
(fn (expr)
|
||||
(cond
|
||||
;; Bool before number (Python: bool subclass of int)
|
||||
(= expr true) \"True\"
|
||||
(= expr false) \"False\"
|
||||
(nil? expr) \"NIL\"
|
||||
(number? expr) (str expr)
|
||||
(string? expr) (py-quote-string expr)
|
||||
(= (type-of expr) \"keyword\") (py-quote-string (keyword-name expr))
|
||||
(= (type-of expr) \"symbol\") (py-mangle (symbol-name expr))
|
||||
:else (str expr))))" "lisp")))
|
||||
|
||||
(~doc-subsection :title "Special Forms"
|
||||
(p "Each SX special form maps to a Python expression pattern:")
|
||||
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
|
||||
@@ -129,274 +159,78 @@
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "(if c t e)")
|
||||
(td :class "px-4 py-2 font-mono" "(t if sx_truthy(c) else e)"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "(when c body)")
|
||||
(td :class "px-4 py-2 font-mono" "(body if sx_truthy(c) else NIL)"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "(let ((a 1)) body)")
|
||||
(td :class "px-4 py-2 font-mono" "(lambda a: body)(1)"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "(fn (x) body)")
|
||||
(td :class "px-4 py-2 font-mono" "lambda x: body"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "(define name val)")
|
||||
(td :class "px-4 py-2 font-mono" "name = val"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "(and a b c)")
|
||||
(td :class "px-4 py-2 font-mono" "(a if not sx_truthy(a) else (b if ... else c))"))
|
||||
(td :class "px-4 py-2 font-mono" "(a if not sx_truthy(a) else ...)"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "(or a b c)")
|
||||
(td :class "px-4 py-2 font-mono" "(a if sx_truthy(a) else (b if ... else c))"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "(case x \"a\" 1 \"b\" 2)")
|
||||
(td :class "px-4 py-2 font-mono" "_sx_case(x, [(\"a\", lambda: 1), ...])"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "(str a b c)")
|
||||
(td :class "px-4 py-2 font-mono" "sx_str(a, b, c)"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "(+ a b)")
|
||||
(td :class "px-4 py-2 font-mono" "(a + b)"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "(= a b)")
|
||||
(td :class "px-4 py-2 font-mono" "(a == b)"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2 font-mono" "&rest args")
|
||||
(td :class "px-4 py-2 font-mono" "*args"))))))
|
||||
(td :class "px-4 py-2 font-mono" "(case x \"a\" 1)")
|
||||
(td :class "px-4 py-2 font-mono" "_sx_case(x, [(\"a\", lambda: 1)])"))))))
|
||||
|
||||
(~doc-subsection :title "Mutation: set! and Cell Variables"
|
||||
(p "Python closures can read but not rebind outer variables. "
|
||||
"SX " (code "set!") " from nested lambdas requires a cell indirection pattern:")
|
||||
(~doc-code :code (highlight ";; SX
|
||||
(define counter
|
||||
(fn ()
|
||||
(let ((n 0))
|
||||
(fn () (set! n (+ n 1)) n))))
|
||||
|
||||
;; Python (impossible with plain lambda)
|
||||
;; → uses _cells dict for mutable bindings
|
||||
def counter():
|
||||
_cells = {}
|
||||
_cells['n'] = 0
|
||||
return lambda: _sx_begin(
|
||||
_sx_cell_set(_cells, 'n', (_cells['n'] + 1)),
|
||||
_cells['n'])" "python"))
|
||||
(p (code "py.sx") " must detect " (code "set!") " targets that cross lambda boundaries "
|
||||
"and route them through the cell dictionary. "
|
||||
"This is the hardest translation rule — the existing bootstrapper's "
|
||||
(code "_find_nested_set_vars") " and " (code "_emit_define_as_def") " handle it.")))
|
||||
(code "py.sx") " detects " (code "set!") " targets that cross lambda boundaries "
|
||||
"and routes them through a " (code "_cells") " dict:")
|
||||
(~doc-code :code (highlight ";; SX ;; Python
|
||||
(define counter def counter():
|
||||
(fn () _cells = {}
|
||||
(let ((n 0)) _cells['n'] = 0
|
||||
(fn () return lambda: _sx_begin(
|
||||
(set! n (+ n 1)) _sx_cell_set(_cells, 'n', ...),
|
||||
n)))) _cells['n'])" "python"))
|
||||
(p "This is the hardest translation rule. " (code "py-find-nested-set-vars")
|
||||
" scans the AST for " (code "set!") " inside nested " (code "fn") " bodies. "
|
||||
(code "py-emit-define-as-def") " emits a " (code "def") " with " (code "_cells")
|
||||
" dict instead of a lambda.")))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Statement vs Expression
|
||||
;; -----------------------------------------------------------------------
|
||||
|
||||
(~doc-section :title "Statement vs Expression Mode" :id "modes"
|
||||
(p "The fundamental tension: SX is expression-oriented (everything returns a value). "
|
||||
"Python has both expressions and statements. " (code "define") " must be a statement. "
|
||||
(code "for-each") " with side effects wants a " (code "for") " loop.")
|
||||
(p "The existing bootstrapper handles this with two methods:")
|
||||
(ul :class "list-disc pl-6 space-y-2 text-stone-700"
|
||||
(li (code "emit(expr)") " → Python expression (used inside other expressions)")
|
||||
(li (code "emit_statement(expr, indent)") " → Python statement (used at top level and in def bodies)"))
|
||||
(p (code "py.sx") " needs the same dual-mode emission. Top-level " (code "define") " forms "
|
||||
"emit as statements. Everything else emits as expressions. Functions with "
|
||||
(code "set!") " emit as " (code "def") " with proper statements instead of lambda expressions."))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Implementation Plan
|
||||
;; -----------------------------------------------------------------------
|
||||
|
||||
(~doc-section :title "Implementation" :id "implementation"
|
||||
(p "Build " (code "py.sx") " incrementally:")
|
||||
|
||||
(~doc-subsection :title "Phase 1: Core Expression Translator"
|
||||
(p "Translate the SX subset used in the spec to Python expressions.")
|
||||
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
|
||||
(li (code "py-mangle") " — SX name → Python identifier (RENAMES table + general rules)")
|
||||
(li (code "py-literal") " — atoms: numbers, strings, booleans, nil, symbols, keywords")
|
||||
(li (code "py-expr") " — recursive expression translator")
|
||||
(li "Infix operators: " (code "+") ", " (code "-") ", " (code "*") ", "
|
||||
(code "/") ", " (code "=") "→" (code "==") ", " (code "!=") ", "
|
||||
(code "<") ", " (code ">") ", " (code "<=") ", " (code ">=") ", " (code "mod") "→" (code "%"))
|
||||
(li "Special forms: " (code "if") ", " (code "when") ", " (code "cond") ", "
|
||||
(code "case") ", " (code "and") ", " (code "or") ", " (code "not"))
|
||||
(li (code "let") " → nested IIFE lambdas")
|
||||
(li (code "fn") "/" (code "lambda") " → Python " (code "lambda"))
|
||||
(li (code "str") " → " (code "sx_str()"))
|
||||
(li (code "list") " → " (code "[...]") " literal")
|
||||
(li (code "dict") " → " (code "{...}") " literal")
|
||||
(li (code "quote") " → AST constructor literals")))
|
||||
|
||||
(~doc-subsection :title "Phase 2: Statement Translator"
|
||||
(p "Top-level forms and function bodies need statement mode:")
|
||||
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
|
||||
(li (code "py-statement") " — emit as Python statement with indentation")
|
||||
(li (code "define") " → " (code "name = expr") " or " (code "def name(): ..."))
|
||||
(li (code "set!") " → assignment (direct or via _cells)")
|
||||
(li (code "for-each") " → " (code "for") " loop")
|
||||
(li (code "do") "/" (code "begin") " → sequential statements")
|
||||
(li (code "when") " → " (code "if:") " block")
|
||||
(li "Mutation detection: scan for " (code "set!") " across lambda boundaries")))
|
||||
|
||||
(~doc-subsection :title "Phase 3: File Translator"
|
||||
(p "Process spec files the same way " (code "bootstrap_py.py") " does:")
|
||||
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
|
||||
(li (code "py-extract-defines") " — parse .sx source, collect top-level defines")
|
||||
(li (code "py-translate-file") " — translate a list of define expressions")
|
||||
(li (code "py-translate-module") " — read a .sx file and produce Python source")
|
||||
(li "Section labels: " (code "# === Transpiled from eval ===") " etc.")))
|
||||
|
||||
(~doc-subsection :title "Phase 4: Bootstrap Runner"
|
||||
(p "A thin Python script that:")
|
||||
(ol :class "list-decimal pl-6 space-y-1 text-stone-700"
|
||||
(li "Loads " (code "py.sx") " into the SX evaluator")
|
||||
(li "Parses each spec file (" (code "eval.sx") ", " (code "render.sx") ", etc.)")
|
||||
(li "Calls " (code "py-translate-file") " on the parsed expressions")
|
||||
(li "Emits the static preamble (types, platform interface)")
|
||||
(li "Concatenates translated sections")
|
||||
(li "Emits the static postamble (fixups, public API)"))
|
||||
(p "The static sections (preamble, platform, primitives) stay in Python — "
|
||||
"they're host-specific by definition. Only the transpilation of "
|
||||
(code ".sx") " spec logic moves to SX."))
|
||||
|
||||
(~doc-subsection :title "Phase 5: Verification"
|
||||
(p "Prove correctness by comparing outputs:")
|
||||
(~doc-code :code (highlight "# Generate with hand-written bootstrapper
|
||||
python bootstrap_py.py > sx_ref_g0.py
|
||||
|
||||
# Generate with py.sx (G1)
|
||||
python run_py_sx.py > sx_ref_g1.py
|
||||
|
||||
# They must be identical
|
||||
diff sx_ref_g0.py sx_ref_g1.py
|
||||
|
||||
# Generate with G1 output running py.sx (G2)
|
||||
python run_py_sx_with_ref.py > sx_ref_g2.py
|
||||
|
||||
# Fixed-point: G1 == G2
|
||||
diff sx_ref_g1.py sx_ref_g2.py" "bash"))
|
||||
(p "When all three diffs are empty, the bootstrapper is self-hosting.")))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; What py.sx is NOT
|
||||
;; Scope
|
||||
;; -----------------------------------------------------------------------
|
||||
|
||||
(~doc-section :title "Scope" :id "scope"
|
||||
(p (code "py.sx") " is a general-purpose SX-to-Python translator. "
|
||||
"The translation rules are mechanical and apply to " (em "all") " SX, "
|
||||
"not just the spec subset.")
|
||||
|
||||
(~doc-subsection :title "Why General?"
|
||||
(p "Every SX form has a straightforward Python equivalent:")
|
||||
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
|
||||
(li (code "(div :class \"foo\" ...)") " → " (code "render_element(\"div\", {\"class\": \"foo\"}, ...)"))
|
||||
(li (code "(~card :title \"hi\")") " → component function call with keyword args")
|
||||
(li (code "defcomp") " → function definition with " (code "&key") " / " (code "&rest") " argument parsing")
|
||||
(li (code "defmacro") " → function that returns AST (macros expand before translation)")
|
||||
(li (code "defpage") " → route registration + handler function")
|
||||
(li (code "defisland") " → island registration (same shape as " (code "defcomp") ")")
|
||||
(li "I/O primitives → calls to host-provided functions"))
|
||||
(p "The spec files are the " (em "first test case") " — because we can verify correctness "
|
||||
"by diffing G0 and G1 output. But the translator itself is target-agnostic: "
|
||||
"it translates SX syntax, not SX semantics."))
|
||||
|
||||
(~doc-subsection :title "Bootstrapping First, Then Everything"
|
||||
(p "The implementation plan above starts with the spec subset (Phases 1-5) because "
|
||||
"that's where the fixed-point proof lives. Once G1 == G0, extend to full SX:")
|
||||
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
|
||||
(li (strong "Phase 6") ": Component and macro forms — " (code "defcomp") ", "
|
||||
(code "defmacro") ", " (code "defisland") ", component calling convention")
|
||||
(li (strong "Phase 7") ": HTML/DOM tags — translate " (code "(div ...)") " to render calls")
|
||||
(li (strong "Phase 8") ": Page forms — " (code "defpage") ", " (code "defhandler") ", route wiring")
|
||||
(li (strong "Phase 9") ": Full application files — translate any " (code ".sx") " file to a Python module"))
|
||||
(p "At that point, " (code "py.sx") " can compile " (em "itself") " — and any SX application — "
|
||||
"into Python. The bootstrapper is just the proof that the translation is correct. "
|
||||
"The translator is the real product."))
|
||||
|
||||
(p "The full RENAMES table from " (code "bootstrap_py.py") " (200+ entries) moves into "
|
||||
(code "py.sx") " as a dict literal. This is the largest single piece — "
|
||||
"a mapping from SX names to their exact Python equivalents."))
|
||||
(p "The spec files are the " (em "first test case") " — because we can verify correctness "
|
||||
"by diffing G0 and G1 output. But the translator itself is target-agnostic: "
|
||||
"it translates SX syntax, not SX semantics. Every SX form has a "
|
||||
"straightforward Python equivalent.")
|
||||
(p "The roadmap:")
|
||||
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
|
||||
(li (code "py.sx") " → Python — " (strong "done"))
|
||||
(li (code "js.sx") " → JavaScript (replaces " (code "bootstrap_js.py") ")")
|
||||
(li (code "go.sx") " → Go (new host)")
|
||||
(li (code "rs.sx") " → Rust (new host)")
|
||||
(li (code "hs.sx") " → Haskell (new host)"))
|
||||
(p "Each new host only needs: (1) a minimal evaluator to run "
|
||||
(code "{host}.sx") " once, and (2) the platform interface in the target language."))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Implications
|
||||
;; -----------------------------------------------------------------------
|
||||
|
||||
(~doc-section :title "Implications" :id "implications"
|
||||
(~doc-subsection :title "Level 1: Practical"
|
||||
(~doc-subsection :title "Practical"
|
||||
(p "One less Python file to maintain. Changes to the transpilation logic "
|
||||
"are written in SX and tested with the SX test harness. The spec and its "
|
||||
"compiler live in the same language."))
|
||||
|
||||
(~doc-subsection :title "Level 2: Architectural"
|
||||
(p "With " (code "z3.sx") " (SMT-LIB), " (code "py.sx") " (Python), and "
|
||||
(code "bootstrap_js.py") " → future " (code "js.sx") " (JavaScript), "
|
||||
(~doc-subsection :title "Architectural"
|
||||
(p "With " (code "z3.sx") " (SMT-LIB) and " (code "py.sx") " (Python), "
|
||||
"the pattern is clear: SX translators are SX programs. "
|
||||
"Adding a new target language means writing one " (code ".sx") " file, "
|
||||
"not a new Python compiler.")
|
||||
(p "The roadmap:")
|
||||
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
|
||||
(li (code "py.sx") " → Python (this plan)")
|
||||
(li (code "js.sx") " → JavaScript (replaces " (code "bootstrap_js.py") ")")
|
||||
(li (code "go.sx") " → Go (new host)")
|
||||
(li (code "rs.sx") " → Rust (new host)")
|
||||
(li (code "hs.sx") " → Haskell (new host)"))
|
||||
(p "Each new host only needs: (1) a minimal evaluator to run " (code "py.sx") " / "
|
||||
(code "{host}.sx") " once, and (2) the platform interface in the target language."))
|
||||
"not a new Python compiler."))
|
||||
|
||||
(~doc-subsection :title "Level 3: Philosophical"
|
||||
(~doc-subsection :title "Philosophical"
|
||||
(p "A self-hosting bootstrapper is a fixed point. The spec defines behavior. "
|
||||
"The translator is itself defined in terms of that behavior. Running the "
|
||||
"translator on the spec produces a program that can run the translator on "
|
||||
"the spec and get the same program.")
|
||||
(p "This is the same structure as a quine — a program that outputs itself. "
|
||||
"But instead of textual self-reproduction, it's " (em "semantic") " "
|
||||
"self-reproduction: the spec's meaning is preserved across the translation, "
|
||||
"and the translation process is defined within the spec's language.")
|
||||
(p "Gödel showed that any sufficiently powerful formal system can encode statements "
|
||||
"about itself. A self-hosting bootstrapper is the constructive version: "
|
||||
"the system doesn't just " (em "talk") " about itself, it " (em "builds") " itself.")))
|
||||
|
||||
;; -----------------------------------------------------------------------
|
||||
;; Existing Patterns
|
||||
;; -----------------------------------------------------------------------
|
||||
|
||||
(~doc-section :title "Existing Patterns" :id "patterns"
|
||||
(p "The " (code "z3.sx") " translator establishes the pattern " (code "py.sx") " follows:")
|
||||
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
|
||||
(table :class "w-full text-sm"
|
||||
(thead :class "bg-stone-50"
|
||||
(tr
|
||||
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Concern")
|
||||
(th :class "px-4 py-2 text-left font-semibold text-stone-700" (code "z3.sx"))
|
||||
(th :class "px-4 py-2 text-left font-semibold text-stone-700" (code "py.sx"))))
|
||||
(tbody
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2" "Name mapping")
|
||||
(td :class "px-4 py-2 font-mono" "z3-name, z3-sym")
|
||||
(td :class "px-4 py-2 font-mono" "py-mangle"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2" "Type mapping")
|
||||
(td :class "px-4 py-2 font-mono" "z3-sort")
|
||||
(td :class "px-4 py-2 font-mono" "—"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2" "Expression emission")
|
||||
(td :class "px-4 py-2 font-mono" "z3-expr")
|
||||
(td :class "px-4 py-2 font-mono" "py-expr"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2" "Keyword extraction")
|
||||
(td :class "px-4 py-2 font-mono" "z3-extract-kwargs")
|
||||
(td :class "px-4 py-2 font-mono" "py-extract-defines"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2" "File translation")
|
||||
(td :class "px-4 py-2 font-mono" "z3-translate-file")
|
||||
(td :class "px-4 py-2 font-mono" "py-translate-file"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2" "Reader macro")
|
||||
(td :class "px-4 py-2 font-mono" "#z3 expr")
|
||||
(td :class "px-4 py-2 font-mono" "#py expr"))
|
||||
(tr :class "border-t border-stone-100"
|
||||
(td :class "px-4 py-2" "Complexity")
|
||||
(td :class "px-4 py-2" "~360 lines")
|
||||
(td :class "px-4 py-2" "~800-1000 lines (set!, statements)")))))
|
||||
(p (code "py.sx") " is larger because Python's statement/expression duality "
|
||||
"and closure mutation rules demand more translation machinery. "
|
||||
"SMT-LIB is expression-only, so " (code "z3.sx") " never needs statement mode."))))
|
||||
"the system doesn't just " (em "talk") " about itself, it " (em "builds") " itself.")))))
|
||||
|
||||
Reference in New Issue
Block a user