Add 4 new concept pages: Lisp vs Rust prover discussion, CL modernization initiative, corrected phases, timeline

.org-ids.json

@@ -143,7 +143,11 @@
   "5c6d7e8f-9a0b-1c2d-3e4f-5a6b7c8d9e0f": "ideas/wider-implications-three-pronged.org",
   "8b9c0d1e-2f3a-4b5c-6d7e-8f9a0b1c2d3e": "ideas/passepartout-bootstrap-mathematica.org",
   "2f3a4b5c-6d7e-8f9a-0b1c-2d3e4f5a6b7c": "ideas/practical-powers-three-pronged.org",
+  "a2811c83-b315-47fd-8ab8-25627c389d1a": "concepts/cl-modernization-timeline.org",
   "be9bccc7-5adf-4d0d-8ee4-8855892189bf": "concepts/neurosymbolic-loop-architectures.org",
   "dddd52a7-adb8-470e-a459-614ade5f76af": "concepts/closing-the-lisp-gap.org",
-  "d2722576-fc9b-4bd3-bc2f-f5692b561b4e": "concepts/academic-nearest-neighbors.org"
+  "85f963a7-a10f-45cc-ace6-6edfeefee762": "concepts/lisp-provers-and-rust-comparison.org",
+  "e199190b-5eff-4a77-8aa5-b6c77647e316": "concepts/cl-modernization-initiative.org",
+  "d2722576-fc9b-4bd3-bc2f-f5692b561b4e": "concepts/academic-nearest-neighbors.org",
+  "a6a04686-56d3-4cb0-9c3d-4722f8f586f3": "concepts/cl-modernization-corrected-phases.org"
 }

concepts/cl-modernization-corrected-phases.org

@@ -0,0 +1,22 @@
+:PROPERTIES:
+:CREATED:  [2026-06-03 Tue]
+:ID:       a6a04686-56d3-4cb0-9c3d-4722f8f586f3
+:END:
+#+title: CL Modernization — Corrected Phase Order
+#+filetags: :HOL:common-lisp:modernization:passepartout:theorem-proving:verification:
+
+* Corrected insight
+
+The prover must come first, not last. An unverified base can't bootstrap a verified upper layer. Every tool that the agent uses to build the next tool must itself be provably correct. The order flips from /easiest first/ to /most foundational first./
+
+* Corrected Phase Order
+
+** Phase 0: HOL Kernel (~500-800 lines of pure CL, verified by ACL2). The smallest, best-defined, highest-leverage artifact. Everything depends on it. A well-known mathematical specification (HOL Light's 10 primitive inference rules).
+
+** Phase 1: Minimal Verified Build System. Just enough to compile the prover and the LSP. Doesn't need to be Cargo-complete — needs to be verified.
+
+** Phase 2: Verified LSP Server. Surfaces SBCL's type inference backed by proofs.
+
+** Phase 3: Verified Language Extensions. Coalton, standard library, all proved correct.
+
+** Phase 4: Full Modernized CL Stack. Self-hosted, self-verifying.

concepts/cl-modernization-initiative.org

@@ -0,0 +1,31 @@
+:PROPERTIES:
+:CREATED:  [2026-06-03 Tue]
+:ID:       e199190b-5eff-4a77-8aa5-b6c77647e316
+:END:
+#+title: CL Modernization Initiative via Passepartout
+#+filetags: :Passepartout:build-system:coalton:common-lisp:modernization:theorem-proving:tooling:
+
+* The Initiative
+
+A plan to bring Common Lisp from the 1990s to modern standards using Passepartout as an autonomous software engineer. The gap is ~25 years of deferred ecosystem work. An agent working at 10x human velocity closes it in 2-3 years.
+
+* Four Phases
+
+1. **Build System** — =cl build= / =cl test= / =cl doc= that works like Cargo. Lockfiles, single namespace, integrated test/doc runner, parallel compilation. Wraps ASDF with modern conventions via a CL.toml manifest.
+
+2. **Tooling** — LSP server that surfaces SBCL's world-class type inference. Jump-to-definition, type-on-hover, rename, refactoring. Online (connected image) and offline (static analysis) modes. Integrates with Coalton for typed paths.
+
+3. **Language Modernization** — Coalton as first-class opt-in typing. Modern standard library (hash sets, priority queues, JSON, HTTP, async, immutable structures). Unicode-by-default. Pattern matching. All backward-compatible with the 1994 standard.
+
+4. **Prover Bootstrap + Deployment** — HOL kernel in CL verified by ACL2. Screamer-backed proof search. HOL proves meta-level properties (macro soundness, evaluator equivalence, concurrent safety). Static binary deployment via =cl build --release=.
+
+* Dependencies
+
+Phase 1 → Phase 2 → Phase 3 → Phase 4. No circular dependency. Each phase is a prerequisite for the next and produces a usable artifact.
+
+* Key Principles
+
+- Every tool is written in CL, for CL, by the agent
+- The 1994 standard is preserved — modernization lives alongside it
+- The agent is the primary consumer (human UX is secondary)
+- The HOL prover grows from use — every proved theorem is future automation

concepts/cl-modernization-timeline.org

@@ -0,0 +1,66 @@
+:PROPERTIES:
+:CREATED:  [2026-06-03 Tue]
+:ID:       a2811c83-b315-47fd-8ab8-25627c389d1a
+:END:
+#+title: CL Modernization — Timeline Estimate
+#+filetags: :HOL:common-lisp:modernization:passepartout:timeline:verification:
+
+* Timeline from Now to a Proved Lisp Machine
+
+** Phase 0: HOL Kernel in CL (~2-4 months)
+
+The smallest, most bounded piece. 500-800 lines of pure CL, well-defined mathematical spec (HOL Light's 10 primitive inference rules). Passepartout writes it, ACL2 verifies it. The first genuine artifact: a verified higher-order prover running inside CL.
+
+Dependency: Passepartout can write and debug CL code reliably. Doesn't need much else.
+
+Key risk: ACL2 verification of the kernel may require iterations — ACL2's automation is limited and some lemmas may need to be added manually.
+
+** Phase 1: Minimal Verified Build System (~4-6 months)
+
+A verified build system that can compile CL projects with deterministic lockfiles. Doesn't need to be Cargo-complete — just enough to compile the prover, the LSP, and its own source.
+
+Dependency: Phase 0 (prover proves build system correctness). Also a solid understanding of ASDF internals.
+
+Key risk: The build system touches the filesystem, subprocesses, and network — all outside the prover's pure core. Only the /dependency resolution and compilation logic/ can be fully proved. The IO layer must be trusted or wrapped in a small verified interface.
+
+** Phase 2: Verified LSP Server (~6-8 months)
+
+Bridges SBCL's compiler to the LSP protocol. Online mode (connected image) for rich interactivity. Verified to not crash, not deadlock, and produce correct type information.
+
+Dependency: Phase 1 (can build and distribute the LSP). Deep SBCL internals knowledge (the agent must learn SBCL's type inference API).
+
+Key risk: SBCL's type inference is not designed for an LSP — it's designed for compile-time warnings. Wrapping it in a responsive protocol requires significant engineering.
+
+** Phase 3: Coalton + Verified Standard Library (~12-18 months)
+
+Coalton as a first-class typed path. Hash sets, priority queues, JSON, HTTP client, async, immutable structures — all proved correct. Unicode-by-default string handling.
+
+Dependency: Phase 2 (the agent needs good tooling to develop and debug this volume of code).
+
+Key risk: The volume. This is the largest phase by lines of code. The prover has to verify thousands of modules. Verification of complex data structures (hash tables, async schedulers) is non-trivial. This is where proof costs become visible.
+
+** Phase 4: Self-Hosting, Self-Verifying CL Stack (~6-12 months)
+
+The modernized CL toolchain can compile itself. The compiler is verified. The runtime has a proved GC (at least bounded pause times). Passepartout proves its own transformation rules correct — the self-improving machine.
+
+Dependency: Phase 3. The standard library and language must be mature enough to write serious systems software in.
+
+Key risk: Self-verification is the hardest problem. Proving that the compiler compiling itself produces a correct binary requires a bootstrapping proof that few systems have attempted. The HOL prover needs to be powerful enough for this.
+
+* The Proved Lisp Machine
+
+After Phase 4: the agent runs on a proved CL, proving its own transformations as it extends itself. This is the capstone. The machine is no longer gambling on correctness — every change is verified before it applies.
+
+* Total Timeline Estimate
+
+- Optimistic (smooth sailing): ~2.5-3 years
+- Realistic (normal engineering friction): ~3.5-5 years
+- Conservative (major proof bottlenecks): ~5-7 years
+
+The primary uncertainty is Phase 3 (verified standard library volume) and Phase 4 (self-verification bootstrapping). Phase 0 and Phase 1 are relatively predictable.
+
+* What Accelerates This
+
+- A existing CL community contributing modules to verify
+- An agent that gets faster as it improves its own environment
+- Leveraging existing verified libraries (Coq, Lean, Isabelle) and adapting their proofs rather than proving from scratch

concepts/lisp-provers-and-rust-comparison.org

@@ -0,0 +1,102 @@
+:PROPERTIES:
+:CREATED:  [2026-06-03 Tue]
+:ID:       85f963a7-a10f-45cc-ace6-6edfeefee762
+:END:
+#+title: Lisp, Provers, and vs Rust
+#+filetags: :ACL2:HOL:LLM:bootstrapping:lisp:rust:theorem-proving:
+
+* Lisp vs Rust — the honest gap
+
+** True defects in Lisp (inherent, not fixable without changing what Lisp is)
+- GC pauses — everything is a tagged pointer on the heap; mitigatable but not eliminatable
+- No memory model / no Send/Sync — threads share everything; concurrency correctness is a discipline, not a guarantee
+
+** Achievable improvements (implementation/ecosystem, not philosophy)
+- Package manager and build system like Cargo (ASDF + Quicklisp is from 2005)
+- LSP-level tooling (SBCL infers types well — surface it)
+- Static binaries and deployment (save-lisp-and-die + tree-shaker exists, not standard)
+- Standard library modernization (hash sets, priority queues, JSON, HTTP, async — Clojure proved this)
+- Ecosystem scale (network effect, fixable with sustained effort)
+
+** Things I was wrong about (corrected during conversation)
+- The type system is not a fundamental limitation — Coalton embeds sound Hindley-Milner typing inside CL, preserving homoiconicity. You opt in per-file.
+- Unpredictable performance is not a language defect — it's a consequence of macro-heavy programming styles. Write in a disciplined subset with declarations and SBCL compiles to within 2x of C. The compiler is deterministic.
+- Macros don't cause unpredictability; they enable styles that confuse the optimizer. You choose not to use those styles.
+
+** Everything else is ecosystem and convention, not language capability: Unicode handling, pattern matching, async I/O, immutable data structures, module systems, error messages.
+
+** The numeric tower is a genuine trade-off: Lisp's auto-promoting math (integers, ratios, floats, complex) is mathematically correct but blocks SIMD and overflow assumptions that make Rust's arithmetic fast. Pick your priority.
+
+* Prover discussion
+
+** The architecture for a Lisp prover
+
+An autonomous agent with mathematical proving can close the gap between Lisp's flexibility and Rust's guarantees /without/ making Lisp rigid. The prover sits between the programmer and the compiler:
+
+#+BEGIN_EXAMPLE
+[Lisp code] → [Passepartout prover] → [SBCL compiler] → [binary]
+                   ↑
+         [Verified: race-free, type-safe, bounded memory, constant-factor performance]
+#+END_EXAMPLE
+
+The prover can:
+- Prove memory safety without a borrow checker — analyze call graphs and data flow
+- Predict performance — unfold macros, SSA-ize, tell the programmer what will optimize
+- Infer types across untyped CL code — flag contradictions, converge toward provably-correct programs
+
+This preserves Lisp's core property: the language stays fluid. The proving agent is an external constraint, not a compiler-enforced limitation. You can always bypass it for fast prototyping.
+
+** Where the coming shift ranks languages
+
+Rust has the most to lose — its entire value proposition is compile-time safety. An AI prover that verifies the same properties about Lisp code makes the borrow checker a solved problem. Rust keeps the advantage only as long as the prover is slower and more expensive than a type system that runs in milliseconds.
+
+Python/JS have the most surface to gain — an AI prover could give them type soundness, no null pointers, thread safety, without changing the languages.
+
+Lisp is uniquely positioned because of homoiconicity. The prover works on S-expressions, which /are/ the AST. No parse/unparse gap. The prover and programmer work on exactly the same artifact. The prover can rewrite a macro expansion without expanding it, annotate specific cons cells with lifetime constraints, and the output is standard diffable code.
+
+** ACL2 and the bootstrap
+
+ACL2 is the right foundation but not the complete solution:
+- It is first-order — can't quantify over functions, can't prove meta-level properties about the evaluator itself
+- It is interactive — human must guide the proof, lemmas must be manually provided
+- It is a subset — pure, no side effects, no CLOS, no I/O, no threading
+- It doesn't scale to everyday production code without massive human effort
+
+But ACL2 proves the architecture is viable: a Lisp-based prover verifying Lisp programs is deeply natural.
+
+** Bootstrapping a HOL prover via ACL2 + Screamer
+
+The HOL kernel is famously tiny (HOL Light: ~400 lines of OCaml, 10 primitive inference rules). The path:
+
+1. Write the HOL kernel in pure CL (~500-800 lines)
+2. ACL2 verifies the kernel implements the inference rules correctly
+3. Screamer provides the proof search engine (backtracking maps to proof tree exploration)
+4. HOL proves meta-level properties: macro soundness, evaluator equivalence, compositionality of skills, safety of self-modification
+5. HOL theorems are reflected back as ACL2 rewrite rules — automation compounds
+
+Trust chain: SBCL runtime → ACL2 (verified by its own meta-circular proof) → HOL kernel (verified by ACL2) → any HOL theorem.
+
+This is not a research problem — the kernel is a well-known artifact. It's an engineering task: transcribe HOL Light's kernel into CL, verify with ACL2, couple with Screamer.
+
+** An LLM can write the HOL kernel
+
+The HOL kernel is the ideal LLM task: ~400-800 lines of pure code, fully specified, well-documented, stateless, with unambiguous correctness criteria.
+
+Workflow: LLM writes plausible kernel → ACL2 verifies it → ACL2 catches hallucinations → iteration converges in 2-3 attempts.
+
+The LLM is allowed to be wrong. ACL2 is the filter. This is achievable today.
+
+** Comparison with Lean
+
+Lean is the standard for mathematics and Passepartout will not compete with it for that purpose:
+- mathlib4 has 100,000+ theorems. A bootstrapped HOL prover starts at zero.
+- Lean has a community of mathematicians; a Lisp prover won't attract one.
+- Lean's elaborator is the result of decades of type theory research; a HOL kernel + Screamer doesn't touch that.
+
+Where Passepartout's prover wins: it verifies /running code/, not abstract mathematics. It is embedded in a self-modifying agent. Its design is optimized for program properties (memory safety, race freedom, macro soundness), not mathematical expressiveness.
+
+Convergence is possible if the agent automates proof discovery at sufficient speed, but that question is unanswered and is the one Passepartout is designed to answer.
+
+** Key insight from the conversation
+
+The self-writing machine doesn't need to prove itself from the void. It proves each next step using everything proven before. The writer is allowed to be heuristic (LLM). The prover just needs to be conservative and accurate. Every time a human signs off on a proof, it becomes future automation.