Restructure three-pronged → knowledge-layers: collapse 11 files to 3, integrate into main architecture
- Rename 'three-pronged' folder to 'knowledge-layers' — prong metaphor
was misleading (implied parallel tines), replaced with epistemic layers
(deductive base, empirical middle, probabilistic oracle — vertical stack)
- Collapse 11 overlapping files into 3 coherent documents:
- knowledge-layers/_index.org: core framework (two engines + one store,
World Model formula, 0-14 layer table, provenance store design,
conflict resolution, cold-start, stage mapping)
- knowledge-layers/practical-implications.org: design-world-aware-of-
physics, 10 powers, Schafmeister existence proof, epistemic transparency
- knowledge-layers/neurological-empirical.org: neural networks in
provenance framework (kept intact)
- Relocate wolfram/mathematica and Schafmeister docs to ideas/viability/
- Integrate into main architecture _index.org:
- Gate: expanded from two vectors (ACL2+LLM) to three (deductive,
provenance/empirical, LLM oracle)
- Autodidactic loop: split into Track 1 (deductive hardening, fast)
and Track 2 (empirical validation, slow, experimental-feedback-driven)
- See also: added Knowledge Layers cross-reference
- Add all-lisp geometry engine note (ideas/lisp-geometry-engine.org) as
concrete illustration of the empirical layer's effect on design work
- Rebuild site: 148 files, 0 errors
This commit is contained in:
Hermes
@@ -3,203 +3,6 @@
|
||||
:ID: 971cd9e7-2cc5-4743-8042-2469dbe4078f
|
||||
:END:
|
||||
#+title: CL Modernization
|
||||
#+filetags: :Passepartout:common-lisp:modernization:prover:tooling:build-system:HOL:ACL2:
|
||||
#+STATUS: active
|
||||
#+filetags: :redirect:
|
||||
|
||||
* What It Is and Why
|
||||
|
||||
Common Lisp is a language from the 1990s with a 1950s syntax, a 1970s package manager, and a 2000s type system — yet it has never been beaten on its core bet: unmatched macro facility, interactive development, image-based workflow, and the most powerful bottom-up programming model ever designed. The CL modernization project within Passepartout is a systematic effort to bring the Lisp ecosystem forward by 25 years without sacrificing the language's defining character.
|
||||
|
||||
This is not a language fork. It is an ecosystem upgrade that preserves the 1994 ANSI standard while adding modern conventions (lockfiles, LSP, standard library, static binaries) and a verified prover (bootstrap HOL verified by ACL2) that makes Lisp the safest language to write self-modifying code in — which is exactly what Passepartout is.
|
||||
|
||||
The central claim: Lisp's defects are not fundamental. They are deferred ecosystem work. GC pauses, the lack of a memory model, unpredictable performance, the tiny library count, the missing package manager — every single one is fixable through engineering, not through a different language. Distinguish carefully:
|
||||
|
||||
#+BEGIN_QUOTE
|
||||
**True defects** (inherent to the model, 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 by default; concurrency correctness is a discipline, not a compiler guarantee
|
||||
|
||||
**Achievable improvements** (implementation and ecosystem, not philosophy):
|
||||
- Package manager and build system like Cargo
|
||||
- LSP-level tooling that surfaces SBCL's world-class type inference
|
||||
- Static binaries and deployment
|
||||
- Modern standard library (hash sets, priority queues, JSON, HTTP, async)
|
||||
- Verified prover for memory safety, race freedom, and macro soundness
|
||||
- Ecosystem scale (a network effect, fixable with sustained effort)
|
||||
#+END_QUOTE
|
||||
|
||||
The first category — GC pauses and shared-state concurrency — is a genuine engineering constraint, but it is contingent on hardware, not a law of nature. Symbolics' Genera OS was a full operating system written in Lisp — device drivers, window system, TCP/IP, file server, all running on the Ivory processor with hardware tag checking, generational write barriers at cache level, and single-cycle CONS allocation. Lisp was a systems language; the chip was designed for it. The reason Lisp struggles on modern silicon is that 40 years of CPU design — cache lines (64 bytes for C structs), prefetchers (linear access patterns), TLBs (contiguous layout), branch predictors (C's control flow) — has been optimized for C's memory model, not for tagged pointer architectures. A RISC-V extension with ~50K additional gates (CONS with write barrier, tag dispatch, read barrier, tag extract, GC check) eliminates the hardware mismatch, as analyzed in [[id:dddd52a7-adb8-470e-a459-614ade5f76af][Closing the Lisp Gap]].
|
||||
|
||||
Without dedicated silicon, Lisp on commodity hardware has larger memory overhead and less predictable pause times on allocation-heavy workloads than C or Rust. For everything Passepartout does — knowledge management, protocol synthesis, agent coordination, verification — modern concurrent generational GCs (single-digit millisecond pauses) are entirely acceptable. The second category — the ecosystem gap — is what this project fixes.
|
||||
|
||||
* Why Lisp Is a Uniquely Good Candidate
|
||||
|
||||
Every other language has a worse starting position for this kind of bootstrap. Here is why Lisp wins:
|
||||
|
||||
**1. Homoiconicity — the prover works on the same artifact the programmer does.**
|
||||
|
||||
The AST of a Lisp program is an S-expression — the same data structure the language uses for everything else. A prover in Lisp reads code as nested lists, transforms it, annotates it, and outputs modified code without a parse/unparse cycle. In Rust or Python, the prover would need a full parser, a serializer, and to handle every AST change as a diff against the source text — introducing a translation gap where the prover's internal representation and the programmer's source can drift apart. In Lisp, the internal representation /is/ the source. The programmer types S-expressions. The prover reads S-expressions. They speak the same notation. This is not a minor convenience — it is the difference between a prover that can be built in 800 lines (HOL Light kernel) and one that requires 20,000 lines of parser, pretty-printer, and AST library.
|
||||
|
||||
**2. ACL2 — a verified Lisp prover already exists.**
|
||||
|
||||
ACL2 is a first-order theorem prover written in and for a subset of Common Lisp. It is itself meta-circularly verified — its kernel is proved correct in ACL2. This means there is a verified prover /already running in Lisp/ that can verify a higher-order kernel (HOL Light's ~400 lines). ACL2 does the first verification for free. The trust chain is:
|
||||
|
||||
#+BEGIN_EXAMPLE
|
||||
SBCL runtime → ACL2 (verified by its own meta-circular proof)
|
||||
→ HOL kernel (verified by ACL2)
|
||||
→ any HOL theorem (proved by HOL kernel)
|
||||
#+END_EXAMPLE
|
||||
|
||||
No other language has an existing verified prover that runs in the same runtime as the programs it verifies. Rust has no verified prover. Python has no verified prover. Lean has a verified kernel but does not run in Python — the prover language is separate from the target language, creating a semantic gap.
|
||||
|
||||
**3. The numerical economy argument (density 3-5×).**
|
||||
|
||||
Lisp's code density is 3-5× higher than C, Rust, or Go for the same semantic work. The social protocol alone — identity, messaging, groups, governance, federation — compresses from ~100 million lines (Twitter, Facebook, Discord, Signal, etc., each reimplementing the same primitives) to ~5,000 lines of specification and ~50,000 lines of synthesized Lisp. This 2,000× compression is not a performance claim — it is a /maintenance/ claim. 5,000 lines of spec have fewer bugs, fewer attack surfaces, and fewer compliance gaps than 100 million lines. When the prover can verify the 5,000 lines, the remaining surface shrinks to essentially zero for specification-level bugs. That is the stack effect: every reduction in complexity compounds because the prover's coverage grows with the system's clarity.
|
||||
|
||||
**4. The type system is not a limitation — Coalton proves it.**
|
||||
|
||||
Coalton embeds sound Hindley-Milner typing inside Common Lisp, preserving homoiconicity. You opt in per-file. This means a CL modernization project does not need to design a new type system — it inherits one that is already integrated and working. The type system becomes /additive/, not /prescriptive/: you can write untyped Lisp for prototypes and add Coalton annotations for production paths. This is the opposite of Rust, where type soundness is mandatory for the entire program. For a self-improving agent, the additive model is strictly better — it lets the agent work in the fluid untyped style for exploration and lock down types for verification.
|
||||
|
||||
**5. Everything else is ecosystem, not language.**
|
||||
|
||||
Unicode handling, pattern matching, async I/O, immutable data structures, module systems, error messages — every one of these is a library or convention, not a language feature gap. Clojure proved this on the JVM: twenty years of CL ecosystem neglect can be fixed in two years with sufficient automation. The gap is not in Lisp's capacity — it is in the community's labor supply. An AI agent working at 10× human velocity changes the labor equation.
|
||||
|
||||
* The Gap: Current State Assessment
|
||||
|
||||
**The performance gap** with C and Rust on hot numerical code is roughly 10-20% in SBCL, concentrated in a few well-understood weaknesses:
|
||||
|
||||
- Alias analysis — SBCL conservatively assumes any memory reference could alias any other. Rust's borrow checker gives LLVM perfect aliasing at function scope. Fixable in ~1-2 person-years.
|
||||
- LLVM backend — Clasp's hybrid approach (fast-path LLVM, slow-path runtime) is the right design but needs significant engineering.
|
||||
- PGO — SBCL has profiling (sb-sprof) but no feedback loop. Fixable in ~1 person-year.
|
||||
- SIMD — No standard SIMD library for Lisp. ~2-3 person-years for a portable abstraction.
|
||||
- Post-link optimization — SBCL's unusual code layout chokes tools like BOLT. A research problem.
|
||||
|
||||
**The ecosystem gap** is the larger barrier:
|
||||
|
||||
| Feature | Rust | Common Lisp |
|
||||
|---------|------|-------------|
|
||||
| Package manager | Cargo (lockfile, binary cache, workspaces) | Quicklisp (source-only, no lockfiles) |
|
||||
| LSP | rust-analyzer | No universal LSP |
|
||||
| Formatter | rustfmt (universal) | cl-form (not universal) |
|
||||
| Test framework | Built-in with benchmarks | Various (FiveAM, Prove) |
|
||||
| Library count | ~180k | ~2k |
|
||||
| WASM target | First-class | Modest |
|
||||
| Static binaries | First-class | Possible but non-standard |
|
||||
|
||||
The largest gap is the package manager — the single highest-leverage investment. The library count (~100× fewer) follows from the lack of a modern build tool, not from a lack of demand.
|
||||
|
||||
* Corrected Phase Plan
|
||||
|
||||
The prover must come first, not last. An unverified base cannot 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/.
|
||||
|
||||
**Phase 0: Verified HOL Kernel (~2-4 months, ~500-800 lines of CL)**
|
||||
|
||||
The HOL kernel (HOL Light's 10 primitive inference rules, ~400 lines of OCaml) is the smallest, best-defined, highest-leverage artifact in the entire project. Transcribed into pure CL and verified by ACL2, it becomes a proved higher-order prover inside the Lisp environment.
|
||||
|
||||
Why the kernel is the right first artifact:
|
||||
- /Tiny./ 500-800 lines. A well-known mathematical specification. No ambiguity about what correct means.
|
||||
- /High leverage./ The kernel is the first prover Passepartout can call. Once it exists, every subsequent phase can be verified by it.
|
||||
- /Low risk./ This is not a research problem — it is an engineering transcription of a known artifact. The only risk is ACL2 iteration time for verification.
|
||||
|
||||
Dependency: Passepartout can write and debug CL code reliably. The HOL kernel ideal for an LLM to generate: small, fully specified, stateless, unambiguous correctness criteria. ACL2 catches hallucinations. Iteration converges in 2-3 attempts.
|
||||
|
||||
**Phase 1: Minimal Verified Build System (~4-6 months)**
|
||||
|
||||
A build system that can compile CL projects with deterministic lockfiles. Does not need to be Cargo-complete — just enough to compile the prover, the LSP, and its own source.
|
||||
|
||||
Key insight: only the dependency resolution and compilation logic can be fully proved. The IO layer (filesystem, subprocesses, network) must be trusted or wrapped in a small verified interface. The build system is the first practical test of the prover — proving that dependency resolution is acyclic and that compilation is deterministic.
|
||||
|
||||
**Phase 2: Verified LSP Server (~6-8 months)**
|
||||
|
||||
Bridges SBCL's compiler to the LSP protocol. Two modes:
|
||||
- /Online (connected image):/ Rich interactivity, live type inference, jump-to-definition.
|
||||
- /Offline (static analysis):/ Works without a running image, uses proved type information.
|
||||
|
||||
Verified to not crash, not deadlock, and produce correct type information. This is the tool that makes writing the rest of the stack productive.
|
||||
|
||||
Key risk: SBCL's type inference is designed for compile-time warnings, not for a responsive protocol. Wrapping it requires significant engineering, and proving the wrapping layer is correct is non-trivial.
|
||||
|
||||
**Phase 3: Coalton + Verified Standard Library (~12-18 months)**
|
||||
|
||||
Coalton as a first-class typed path. Hash sets, priority queues, JSON, HTTP client, async scheduler, immutable data structures — all proved correct. Unicode-by-default string handling. Pattern matching. Backward-compatible with the 1994 standard.
|
||||
|
||||
This is the largest phase by lines of code. The prover has to verify thousands of modules. Verification of complex data structures (hash tables, concurrent queues, async schedulers) is non-trivial. This is where proof costs become visible — and where the agent's automation of proof discovery matters most.
|
||||
|
||||
Key risk: Volume. 12-18 months assumes the agent compounds its own proving capability during the phase. Without that, the timeline extends.
|
||||
|
||||
**Phase 4: Self-Hosting, Self-Verifying CL Stack (~6-12 months)**
|
||||
|
||||
The modernized CL toolchain compiles itself. The compiler is verified. The runtime has a proved GC (at least bounded pause times). Passepartout proves its own transformation rules correct.
|
||||
|
||||
This is the capstone: a self-improving machine that proves every change before applying it. No other language has achieved this. Even the most advanced systems (Coq, Lean) have a trusted computing base that includes the kernel and the runtime — the /rest/ of their infrastructure is unverified. CL Modernization Phase 4 aims for a verified toolchain from kernel to compiler to build system, with only the SBCL runtime left as trusted.
|
||||
|
||||
Key risk: Self-verification bootstrapping is the hardest problem in proving. Proving that the compiler compiling itself produces a correct binary requires a bootstrapping argument that few systems have ever attempted and none have fully achieved. The HOL prover needs to be powerful enough for this.
|
||||
|
||||
* Timeline
|
||||
|
||||
The estimates below assume Passepartout's capabilities compound during the project — the agent gets faster as it improves its own environment.
|
||||
|
||||
| Phase | Optimistic | Realistic | Conservative | Risk |
|
||||
|-------|-----------|------------|-------------|------|
|
||||
| Phase 0: HOL kernel | 2 months | 3 months | 4 months | ACL2 verification iteration |
|
||||
| Phase 1: Build system | 3 months | 5 months | 6 months | IO layer verification boundary |
|
||||
| Phase 2: LSP server | 4 months | 7 months | 8 months | SBCL internals complexity |
|
||||
| Phase 3: Standard library | 10 months | 15 months | 18 months | Volume, proof costs |
|
||||
| Phase 4: Self-hosting | 4 months | 8 months | 12 months | Self-verification bootstrapping |
|
||||
| **Total** | **~23 months** | **~38 months** | **~48 months** | |
|
||||
|
||||
The primary uncertainty is Phase 3 (verified standard library volume) and Phase 4 (self-verification bootstrapping). Phase 0 and Phase 1 are relatively predictable because the artifacts are small and well-defined. An optimistic 20-month timeline is possible if the agent compounds at sufficient speed and no fundamental proof barriers emerge — but 3-5 years is the realistic window.
|
||||
|
||||
What accelerates this:
|
||||
- A existing CL community contributing modules to verify
|
||||
- Leveraging existing verified libraries (Coq, Lean, Isabelle) and adapting their proofs rather than proving from scratch
|
||||
- An LLM that gets faster at generating correct code as it gains experience in the domain (this is the compounding assumption)
|
||||
|
||||
* Expected Impact
|
||||
|
||||
**On Lisp development:**
|
||||
|
||||
A modernized CL with a verified prover changes the economics of writing Lisp from /adventure/ to /engineering./ The distinguishing features that make Lisp powerful (macros, interactive development, image-based workflow) become /safe/ rather than /dangerous./
|
||||
|
||||
- Macro soundness is guaranteed by the prover, not by programmer discipline
|
||||
- Concurrency bugs are caught during compilation, not during runtime
|
||||
- Type inference across untyped code is available via the LSP, even if the file has no Coalton declarations
|
||||
- Library import is a one-line =cl add = command with deterministic lockfiles
|
||||
- Deployment is a =cl build --release= producing a static binary
|
||||
|
||||
**On Passepartout itself:**
|
||||
|
||||
Passepartout is a self-modifying agent. Every transformation it applies to its own code is a potential correctness risk. A verified Lisp stack means every self-modification is proved safe before it applies. This shifts Passepartout from /experimental/ to /capability./ The agent can reason about its own transformations with mathematical certainty, not statistical confidence.
|
||||
|
||||
This is the meaning of Phase 4: the machine is no longer gambling on correctness. Every change is verified before it applies. No LLM hallucination propagates into the running system. The agent improves safely.
|
||||
|
||||
**On the broader software landscape:**
|
||||
|
||||
A proved Lisp has implications beyond the Lisp community:
|
||||
|
||||
- /Rust loses its exclusivity on safe systems programming./ If a Lisp prover verifies memory safety, race freedom, and constant-factor performance, the borrow checker is no longer the only path to correctness. Lisp offers the same guarantees with a more flexible macro system and interactive development. The choice between Lisp and Rust becomes about workflow preference, not safety.
|
||||
|
||||
- /Python and JavaScript gain a target./ If the Lisp prover can verify compiled code, it can verify Python or JS compiled to Lisp (there are several transpilers). Statically proving correctness of dynamically-typed programs becomes tractable through the verified prover, without requiring the language itself to change.
|
||||
|
||||
- /The self-improving machine becomes a replicable architecture./ Any domain where an LLM writes code and a prover verifies it can adopt the same pipeline. The first domain is Lisp because of homoiconicity. Once the pipeline works, it can be adapted.
|
||||
|
||||
**On specification-level verification:**
|
||||
|
||||
The deepest impact is a shift from /testing as correctness/ to /proof as correctness./ In current practice, a program's correctness is approximated by test coverage, which is always incomplete. A verified Lisp toolchain can prove functional correctness for any program that runs on it. The programmer specifies what correct means (preconditions, postconditions, invariants), and the prover establishes it. Testing becomes a fallback for properties the prover cannot yet establish, rather than the primary correctness mechanism.
|
||||
|
||||
This is not a claim that all bugs disappear — the specification itself can be wrong, the runtime is still trusted, and undecidable properties remain undecidable. But the attack surface for /implementation bugs/ (the majority of security vulnerabilities) drops to near zero for any program the prover can analyze.
|
||||
|
||||
* Relationship to Passepartout
|
||||
|
||||
CL Modernization is a project /within/ Passepartout, not adjacent to it. Passepartout's architecture — fact store, gates, ACL2 prover, self-improving loop — is the engine that drives the modernization. The agent improves Lisp while running on Lisp, creating a positive feedback loop: better tooling → faster development → more capability → better tooling.
|
||||
|
||||
The relationship is symbiotic:
|
||||
- Passepartout provides the engineering capacity to close the 25-year gap
|
||||
- The modernized CL provides a verifiable foundation for Passepartout's self-modification
|
||||
- The ACL2 prover (already part of Passepartout's architecture) provides the verification for both
|
||||
|
||||
See also:
|
||||
- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Passepartout]] — the project that drives this modernization
|
||||
- [[id:dddd52a7-adb8-470e-a459-614ade5f76af][Closing the Lisp Gap]] — detailed performance and ecosystem analysis
|
||||
- [[id:c0fdec00-8a44-43f0-ac81-e8dc61411865][Passepartout Architecture]] — how the gate system and prover fit together
|
||||
- [[id:9af13fff-9725-542b-93b1-a555bc74ad72][Lisp Economics]] — why Lisp is economically viable despite its small market share
|
||||
This document has moved to [[file:../passepartout/architecture/lisp-foundation.org][Lisp Foundation]] in the Passepartout architecture tree.
|
||||
|
||||
@@ -1,18 +0,0 @@
|
||||
:PROPERTIES:
|
||||
:CREATED: [2026-05-24 Sun]
|
||||
:ID: 2afd9a3c-e96a-54c7-ac77-a05a28065b4b
|
||||
:END:
|
||||
#+title: Biology as Proof of the Lisp Model
|
||||
#+filetags: :passepartout:biology:lisp:parallels:evolution:
|
||||
|
||||
Striking parallels between microbiology and the Lisp model:
|
||||
|
||||
1. **Homoiconicity** — DNA is code and data in the same molecule; no separate source and binary
|
||||
2. **Hot-reloadable image** — alternative splicing, epigenetic marks, post-translational modifications change the running program without restart
|
||||
3. **Automatic memory management** — proteasomes degrade misfolded proteins, autophagy recycles organelles; the cell never calls free()
|
||||
4. **Interpreted dynamic language** — DNA → RNA → ribosome (interpreter) → protein; no static compilation step
|
||||
5. **Self-modifying source** — CRISPR, transposons, DNA repair modify the genome at runtime; eval on the genome
|
||||
6. **Duck typing** — protein folding depends on chemical environment, not type declarations
|
||||
7. **Concurrent real-time GC** — apoptosis breaks down cell components for recycling by neighboring cells
|
||||
|
||||
Biology chose the Lisp model because it is more robust, adaptable, and evolvable. Evolution optimized for survival in an unpredictable environment, not peak single-thread throughput. Biology is the proof that the Lisp model can be efficient at planetary scale, running on hardware that self-assembles from food. See [[id:9af13fff-9725-542b-93b1-a555bc74ad72][Lisp economics]] for how these biological parallels inform the business model.
|
||||
@@ -1,138 +0,0 @@
|
||||
:PROPERTIES:
|
||||
:CREATED: [2026-05-27 Wed]
|
||||
:ID: dddd52a7-adb8-470e-a459-614ade5f76af
|
||||
:END:
|
||||
#+title: Closing the Lisp Gap
|
||||
#+filetags: :passepartout:lisp:compiler:performance:ecosystem:asics:bootstrapping:
|
||||
|
||||
Lisp has a performance gap with C and Rust of roughly 10-20% on hot numerical code and a much larger ecosystem gap (package manager, LSP, cross-compilation, library count ~2k vs ~180k). This page diagnoses both gaps and argues that [[id:28c46769-c14b-42aa-ac7a-69d310157f8f][Passepartout]]'s architecture — fact store, gates, ACL2 prover, self-improving loop — changes the nature of the problem from community-coordination to knowledge-capture, making the gap closable in 1-2 years rather than 20-30 person-years.
|
||||
|
||||
See [[id:9af13fff-9725-542b-93b1-a555bc74ad72][why Lisp is economically viable now]] for the economic foundation. See [[id:13e6ae54-2d24-5aa0-b1cd-a7e8e749aa70][self-driving Lisp Machine]] for the hardware endpoint.
|
||||
|
||||
* The Performance Gap
|
||||
|
||||
What Lisp (SBCL) still needs to close the remaining gap with C/Rust:
|
||||
|
||||
- **Alias analysis on SBCL's IR.** Rust's borrow checker gives LLVM perfect aliasing at function scope. SBCL conservatively assumes any memory reference could alias any other. Fix: a static analysis pass proving non-aliasing for common patterns (different simple-array types, arrays vs scalars). ~1-2 person-years, biggest single investment.
|
||||
|
||||
- **LLVM backend (Clasp).** Clasp gives LLVM's full pipeline — auto-vectorization, LICM, inlining cost modeling — at the cost of fighting LLVM's static worldview with CLOS's dynamic semantics. Clasp's hybrid approach (fast-path LLVM, slow-path runtime) is the right design. ~5-10 person-years to reach SBCL's general performance with better hot-path optimization.
|
||||
|
||||
- **PGO (profile-guided optimization).** SBCL has profiling (sb-sprof) but no feedback loop — the compiler cannot reweight branches or layout hot/cold blocks. Fix: instrumentation pass that emits counter VOPs, a profile binary, and a recompilation step that annotates IR with branch weights. ~1 person-year.
|
||||
|
||||
- **Post-link optimization.** Facebook's BOLT profiles binary execution and rewrites code layout to reduce I-cache misses. SBCL's unusual code layout (trampolines, closure entry points) chokes BOLT. Hard research problem.
|
||||
|
||||
- **Vectorization VOPs.** No standard SIMD library for Lisp. Every ISA extension needs its own VOP set. C gets this via xmmintrin.h and auto-vectorization. ~2-3 person-years for a portable SIMD abstraction backed by platform VOPs.
|
||||
|
||||
* The Ecosystem Gap
|
||||
|
||||
| Feature | Rust | Common Lisp |
|
||||
|---------|------|-------------|
|
||||
| Package manager | Cargo (lockfile, binary cache, workspace) | Quicklisp (no lockfile, source-only) |
|
||||
| LSP | rust-analyzer (excellent) | No universal LSP |
|
||||
| Formatter | rustfmt (universal) | cl-form (not universal) |
|
||||
| Linter | Clippy (>700 rules) | No equivalent |
|
||||
| Doc system | rustdoc (integrated) | Conventions only |
|
||||
| Cross-compilation | --target flag | Manual, source-based |
|
||||
| Test framework | Built-in with benchmarks | Various (FiveAM, Prove) |
|
||||
| Sanitizers | ASan, TSan, MSan, UBSan | None |
|
||||
| Library count | ~180k | ~2k |
|
||||
| WASM target | First-class | Modest |
|
||||
| Mobile targets | First-class | None native |
|
||||
|
||||
The largest gaps are the package manager (the single highest-leverage investment — ~2-3 person-years + community coordination) and the library count (~100× fewer).
|
||||
|
||||
* Lisp ASICs: What They Change
|
||||
|
||||
A Lisp ASIC (Symbolics Ivory, CADR, or a modern RISC-V variant) **raises the floor** more than the ceiling:
|
||||
|
||||
**What it gives in hardware:**
|
||||
- Tag checking on every memory access — types, GC bits, forwarding pointers in parallel with ALU
|
||||
- Hardware CONS — single-cycle allocation from a dedicated region with automatic write barriers
|
||||
- Hardware GC support — generational barriers at cache level
|
||||
- Hardware generic function dispatch — type-code lookup in CAM instead of method cache
|
||||
- Hardware stack groups and shallow binding — zero-cost special variable rebinding
|
||||
|
||||
**Does it eliminate the need for compiler optimization?** Both yes and no. The worst case becomes much faster — naive code and optimized code are closer together. But the compiler still matters for instruction scheduling, inlining decisions, dead code elimination, and loop optimizations. The ASIC shifts the optimizer's job from "avoid Lisp overhead" to "use special instructions effectively." The gap between C and Lisp on hot numerical loops narrows from ~20% to maybe 5%.
|
||||
|
||||
* Embedded and Small Systems: RISC-V Lisp Extension
|
||||
|
||||
A full Lisp Machine chip doesn't make sense for embedded, but a **RISC-V extension with 5-10 Lisp primitives** does:
|
||||
|
||||
- ~5 new instructions added to a RV32/RV64 core (CONS with write barrier, tag dispatch, read barrier, tag extract, GC check)
|
||||
- Implementable as an FPGA soft-core or small coprocessor alongside a microcontroller
|
||||
- ~50K additional gates on a RISC-V e300-class core
|
||||
|
||||
This makes Lisp viable where C is currently mandatory: real-time control, sensor nodes, IoT. The hardware CONS eliminates allocation cost; the hardware read barrier eliminates GC pause unpredictability by making the collector a concurrent background task instead of a stop-the-world event. The gap goes from 10-100× (current, boxed allocation + GC) to ~2-5×.
|
||||
|
||||
**Strategic play:** Define the extension, open-source an FPGA implementation, get it ratified as a standard RISC-V extension. Then any chip vendor can add it.
|
||||
|
||||
* Why Passepartout Changes the Equation
|
||||
|
||||
The standard model for closing the library gap: *more users → more libraries → more users (virtuous cycle).*
|
||||
|
||||
Passepartout's model: *agent synthesizes libraries on demand → fewer blockers → more users.*
|
||||
|
||||
**Knowledge-capture replaces community-coordination.** The rate-limiter shifts from "people who can write Lisp libraries" to "people who can explain their domain well." A 3-hour conversation with a domain expert captures the specifications, invariants, known techniques, and correctness criteria. The agent synthesizes the library, verifies it against stored properties via ACL2, and hot-reloads it.
|
||||
|
||||
**What changes:**
|
||||
- Standard protocols (HTTP, SQL, JSON, crypto, file formats) — the agent synthesizes these from specs it has seen in training.
|
||||
- Wrapper libraries (CFFI bindings, REST clients) — mechanical, the agent handles well.
|
||||
- Domain-specific libraries — the hardest category *without* a knowledge architecture, and the most tractable *with* one. The gate becomes the bridge: human provides $10K/year-level insight, agent provides $200K/year-level engineering.
|
||||
- What stays hard: libraries where the algorithm requires original research (not yet done by anyone), libraries requiring specialized hardware knowledge the human cannot articulate, and battle-tested implementations where verification of constant-time correctness is near-impossible.
|
||||
|
||||
**Passepartout's position to direct Lisp development:**
|
||||
|
||||
1. **Instrumentation advantage.** It runs in Lisp, can profile its own execution in Lisp terms, identify SBCL's compiler bottlenecks, and generate patches — all in a closed feedback loop that C compilers lack.
|
||||
|
||||
2. **Coordination advantage by adoption.** If Passepartout becomes the standard Lisp agent framework, its tooling choices become de facto standards: ocicl with lockfiles becomes the package manager, cl-lsp gets maintenance, sb-sprof fed into the optimizer becomes the PGO pipeline.
|
||||
|
||||
3. **Automated contribution pipeline.** Profile → identify hot path in SBCL → generate candidate VOP or optimization pass → run test suite (verified by ACL2) → submit patch. Cycle time from "this would be faster if SBCL did X" to "SBCL does X" drops from years to days.
|
||||
|
||||
4. **The prover multiplier.** ACL2 makes safe optimization an engineering discipline instead of an experimental art. The agent can generate thousands of variants, verify correctness, benchmark, and keep the Pareto-optimal set — coverage a human cannot match.
|
||||
|
||||
* The Same Compression Applies to Social Infrastructure
|
||||
|
||||
The Passepartout architecture compresses the *social* ecosystem of the internet the same way it compresses the *software* ecosystem — replacing multiplicative duplication with additive specification.
|
||||
|
||||
**The problem:** Twitter (~10M lines), Facebook (~60M lines), Reddit (~5M lines), Discord (~8M lines), Signal (~3M lines), Telegram (~5M lines), LinkedIn (~15M lines), WhatsApp (~3M lines). Each independently implements the same primitives: identity, identity verification, key recovery, encrypted messaging, group messaging, moderation, content addressing, access control, payment integration, rate limiting, spam detection, reporting, appeal, ban propagation, federation, data export, deletion. Each is a separate 3-60 million line codebase with the *same semantics* but different APIs, different bugs, different compliance postures, different threat models. None compose with any other.
|
||||
|
||||
**Under Passepartout:**
|
||||
|
||||
- One spec for identity: keys, recovery, delegation, attestation. ~500 lines.
|
||||
- One spec for messaging: content-addressed, encrypted, ordered by a Merkle DAG. ~1,000 lines.
|
||||
- One spec for groups: membership, permissions, moderation. ~1,500 lines.
|
||||
- One spec for federation: cross-server state replication, conflict resolution. ~1,000 lines.
|
||||
- Gates for policy: what content types are allowed, what moderation actions exist, how appeals work. Configurable per community, enforced by the prover.
|
||||
|
||||
Total spec surface: ~5,000 lines. Total synthesized code (client + server for any platform): ~50,000 lines of Lisp.
|
||||
|
||||
**5,000 lines of spec + 50,000 lines of synthesized implementation vs ~100 million lines of independent, incompatible, duplicative implementations** that each require their own security audits, compliance reviews, and maintenance pipelines.
|
||||
|
||||
**Composition replaces isolation.** In the current model, Signal's identity system cannot talk to WhatsApp's. Reddit's moderation cannot federate with Discord's. The protocols don't compose because they were designed independently with no shared semantic foundation. In the Passepartout model, every synthesized client and server speaks the same spec. A community can use a Telegram-like frontend and a Reddit-like frontend — both synthesized from the same messaging and content-addressing specs — and they share identity, encryption, and federation because those are the same underlying specifications. The frontend is a gate: a policy on how to render the same underlying protocol data.
|
||||
|
||||
**The multiplication disappears.** Under the old model, N platforms cost N × (full stack). Under Passepartout, N communities cost one stack + N × (~100 lines of gate policy). The marginal cost of adding a new community approaches zero. This is the same argument as the library gap: N libraries × (different maintainers, different bugs, different API surfaces) collapses to N specifications × (one verified synthesized implementation).
|
||||
|
||||
**The deeper claim:** the protocol isn't a separate feature of Passepartout. It is the same compression architecture applied to a different domain — coordination infrastructure instead of library infrastructure. Both are about replacing multiplicative maintenance burden with additive specification complexity, amplified by Lisp's density and the prover's correctness guarantees.
|
||||
|
||||
* Timeline Compression
|
||||
|
||||
With the self-improving loop, the marginal cost of each incremental improvement drops to near zero. The system improves continuously rather than in discrete releases. Every time compute is added to the pipeline, the system gets faster.
|
||||
|
||||
| Gap | Human-only | AI-assisted | Passepartout loop |
|
||||
|-----|-----------|-------------|------------------|
|
||||
| SBCL alias analysis | 18 mo | 10 mo | 3-4 mo |
|
||||
| PGO pipeline | 12 mo | 6 mo | 2-3 mo |
|
||||
| Cargo-equivalent | 24 mo | 8 mo | 4-6 mo |
|
||||
| LSP server | 18 mo | 6 mo | 3-4 mo |
|
||||
| RISC-V Lisp extension | 24 mo | 12 mo | 6-8 mo |
|
||||
| Library coverage (100 APIs) | 3-5 yrs | 12 mo | 3-4 mo (synthesis) |
|
||||
| Clasp maturity | 5-10 yrs | 3-5 yrs | 1-2 yrs |
|
||||
|
||||
The meta-level effect: once the pipeline exists (profile → generate → verify → test → deploy), the system improves continuously. The gap-closing problem goes from "we need enough talented volunteers" to "we need enough compute" — and compute grows on a known exponential, while talent doesn't.
|
||||
|
||||
* Relationship to Other Concepts
|
||||
|
||||
- [[id:9af13fff-9725-542b-93b1-a555bc74ad72][Lisp economics]] — the economic viability argument provides the why; this page provides the how.
|
||||
- [[id:13e6ae54-2d24-5aa0-b1cd-a7e8e749aa70][Self-driving Lisp Machine]] — the hardware endpoint enabled by this software-level gap-closing.
|
||||
- [[id:efc76898-03f7-57ba-923d-35d65da88bb7][Sufficiency flip]] — the threshold where symbolic reasoning becomes cheaper than LLM calls; applies to compiler optimization as a domain.
|
||||
- [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][Verification appliance]] — the $5K/year hardware that replaces $500K/year in compliance costs; RISC-V Lisp extension is the technical path to making this run everywhere.
|
||||
@@ -1,29 +0,0 @@
|
||||
:PROPERTIES:
|
||||
:CREATED: [2026-05-24 Sun]
|
||||
:ID: 9af13fff-9725-542b-93b1-a555bc74ad72
|
||||
:ID: 0b5a8a74-cfd6-542d-bc88-4eb3cd8626f9
|
||||
:END:
|
||||
#+title: Lisp Economics
|
||||
#+filetags: :passepartout:economics:lisp:history:C:viability:cost:marginal:zero:
|
||||
|
||||
The 1980s trade-off was: C is cheap enough for the market. Correctness is a luxury the market cannot afford. The 2020s trade-off is: C is expensive for the market. Incorrectness has become the dominant cost of software. Lisp's verification infrastructure is now the cheaper option.
|
||||
|
||||
Four transformations flipped the economics:
|
||||
|
||||
1. **Memory is free.** 40MB runtime is noise on a $20 Raspberry Pi with 8GB RAM. In 1980, DRAM was ~$5,000/MB.
|
||||
2. **Transistors are free.** Modern ARM Cortex-A72 has billions of transistors. GC and type dispatch cost nothing because the transistors are there whether used or not.
|
||||
3. **Complexity saturates human verification.** Systems are tens of millions of lines. Testing is necessary but insufficient — zero-day vulnerabilities prove bugs survive all testing. Formal verification is the only known path.
|
||||
4. **Cost of failure exceeds cost of verification.** A single breach costs millions. Regulation mandates provable compliance. Proving correctness is cheaper than not proving it.
|
||||
|
||||
The [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][verification appliance]] (AGPL symbolic engine + RISC-V Lisp μcode on FPGA) costs $5,000/year and replaces $500,000/year in compliance audits, breach litigation, and regulatory fines. This cost structure — zero marginal cost per additional user — is what makes Lisp economically viable at scale. The [[id:13e6ae54-2d24-5aa0-b1cd-a7e8e749aa70][self-driving Lisp Machine]] is the hardware endpoint of this economic logic. For the biological analogy that explains why Lisp architecture is a natural outcome of complexity pressure, see [[id:2afd9a3c-e96a-54c7-ac77-a05a28065b4b][biology parallels]]. For the historical precedent, see the [[id:00ab3a4d-e3de-5605-a67d-12935bb36ab5][comparison with Symbolics Genera]]. The [[id:5f55bbe6-d243-5766-8ccf-5c5cc88a6542][impact on the AI industry]] is the market-side consequence.
|
||||
|
||||
* Cost Structure — Zero Marginal Cost
|
||||
|
||||
- **One-time cost:** [[id:45ea493b-94ad-5885-aa65-0c846e5c3c1d][gate-rule encoding]] for a domain (from hours for codified domains up to months for tacit domains)
|
||||
- **Near-zero marginal cost:** ACL2 proof + Screamer consistency check + VivaceGraph lookup per interaction — all CPU-native, all in-image
|
||||
- **No recurring LLM API costs** for the 80% symbolic reasoning layer
|
||||
- **After [[id:efc76898-03f7-57ba-923d-35d65da88bb7][sufficiency flip]]:** pennies per day vs dollars per day for LLM-only
|
||||
|
||||
The cost curve inverts: generation is expensive, verification is cheap. This is the inversion [[id:28c46769-c14b-42aa-ac7a-69d310157f8f][Passepartout]] exploits.
|
||||
|
||||
Token demand shifts from "every interaction burns tokens" to "only unfamiliar interactions burn tokens." Steady-state per-user LLM consumption drops by an order of magnitude.
|
||||
@@ -1,100 +0,0 @@
|
||||
: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 — Assessed Gap
|
||||
|
||||
** Inherent limits of Lisp
|
||||
|
||||
Two properties cannot be eliminated without changing what Lisp is:
|
||||
|
||||
- GC pauses — everything is a tagged pointer on the heap; mitigatable (generational, concurrent collectors) but not eliminatable
|
||||
- No memory model / no Send/Sync — threads share everything by default; concurrency correctness is a discipline enforced by code review or a prover, not by the compiler
|
||||
|
||||
These are genuine costs, but they are contingent on hardware, not laws of nature. The Symbolics Genera OS was a full operating system written in Lisp — device drivers, window system, TCP/IP, filesystem — running on the Ivory processor with hardware tag checking and single-cycle CONS allocation. Lisp was a systems language; the chip was designed for it. The reason Lisp's GC pauses are costly on modern silicon is that CPUs are optimized for C's memory model: 64-byte cache lines for structs, prefetchers for linear access, TLBs for contiguous layout. A RISC-V Lisp extension (~50K gates) eliminates the mismatch entirely.
|
||||
|
||||
Without dedicated silicon, Lisp on commodity hardware has larger memory overhead and less predictable pause times than C or Rust on allocation-heavy workloads. For Passepartout's use cases — knowledge management, protocol synthesis, agent coordination, interactive systems — modern concurrent generational GCs (single-digit millisecond pauses) are acceptable.
|
||||
|
||||
** Fixable gaps (implementation and ecosystem, not language philosophy)
|
||||
|
||||
- Package manager and build system like Cargo (ASDF + Quicklisp is from 2005)
|
||||
- LSP-level tooling that surfaces SBCL's type inference
|
||||
- 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)
|
||||
|
||||
** Common misconceptions about Lisp's limits
|
||||
|
||||
- The type system is not a fundamental limitation. Coalton embeds sound Hindley-Milner typing inside CL, preserving homoiconicity. Opt-in per-file.
|
||||
- Unpredictable performance is not a language defect — it is a consequence of macro-heavy programming styles. Write in a disciplined subset with type declarations and SBCL compiles to within 2x of C on hot paths. The compiler is deterministic.
|
||||
- Macros do not cause unpredictability; they enable styles that confuse the optimizer. The choice to use those styles is the programmer's.
|
||||
- Unicode handling, pattern matching, async I/O, immutable data structures, module systems, error messages — all library or convention work, not language capability.
|
||||
- The numeric tower (auto-promoting integers, ratios, floats, complex) is a genuine trade-off: mathematically correct, but blocks SIMD and the overflow assumptions that make Rust's arithmetic fast. Choose based on domain.
|
||||
|
||||
* Prover Architecture
|
||||
|
||||
An autonomous prover 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 proves:
|
||||
- Memory safety without a borrow checker — by analyzing call graphs and data flow
|
||||
- Performance predictability — by unfolding macros, constructing SSA form, and reporting what the optimizer will produce
|
||||
- Type soundness across untyped CL code — by inferring types, flagging contradictions, and converging toward provably-correct programs
|
||||
|
||||
This preserves Lisp's defining property: the language stays fluid. The prover is an external constraint, not a compiler-enforced limitation. The programmer can always bypass it for fast prototyping.
|
||||
|
||||
** Impact by language
|
||||
|
||||
- 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 its advantage only as long as the prover is slower and more expensive than a type system that runs in milliseconds.
|
||||
- Python and JS have the most surface to gain. A prover could give them type soundness, no null pointers, and thread safety without changing the languages — transpiling through a verified Lisp intermediate.
|
||||
- Lisp is uniquely positioned because of homoiconicity: the prover works on S-expressions, which /are/ the AST. No parse/unparse gap. The prover and the programmer work on the same artifact.
|
||||
|
||||
** ACL2 as foundation
|
||||
|
||||
ACL2 is the right foundation but not the complete solution:
|
||||
- It is first-order — cannot quantify over functions, cannot prove meta-level properties about the evaluator itself
|
||||
- It is interactive — a human must guide the proof; lemmas must be manually provided
|
||||
- It is a subset of CL — pure, no side effects, no CLOS, no I/O, no threading
|
||||
- It does not scale to everyday production code without massive human effort
|
||||
|
||||
But ACL2 proves the architecture is viable: a Lisp-based prover verifying Lisp programs is natural, not forced.
|
||||
|
||||
** Bootstrapping a HOL prover via ACL2 + Screamer
|
||||
|
||||
The HOL kernel (HOL Light: ~400 lines of OCaml, 10 primitive inference rules) is a well-known artifact — an engineering task, not a research problem. The bootstrap path:
|
||||
|
||||
1. Transcribe the HOL kernel into 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.
|
||||
|
||||
The HOL kernel is an ideal LLM task — small, fully specified, stateless, with unambiguous correctness criteria. ACL2 filters hallucinations. Iteration converges in 2-3 attempts.
|
||||
|
||||
** Comparison with Lean
|
||||
|
||||
Lean is the standard for interactive theorem proving in mathematics. Passepartout will not compete with it for that purpose:
|
||||
- mathlib4 has over 100,000 theorems. A bootstrapped HOL prover starts at zero.
|
||||
- Lean has a community of mathematicians; a Lisp prover will not attract one.
|
||||
- Lean's elaborator is the result of decades of type theory research; a HOL kernel plus Screamer does not approach it.
|
||||
|
||||
Where Passepartout's prover wins: it verifies /running code/, not abstract mathematics. It is embedded in a self-modifying agent. Its design optimizes for program properties (memory safety, race freedom, macro soundness), not mathematical expressiveness. Convergence on the mathematical side is possible if the agent automates proof discovery at sufficient speed — but that question is unanswered and is one Passepartout is designed to answer.
|
||||
|
||||
* The self-writing machine and proofs
|
||||
|
||||
The self-writing machine does not need to prove itself from the void. It proves each next step using everything proven before. The writer (LLM) is allowed to be heuristic. The prover only needs to be conservative and accurate. Every time a human signs off on a proof, it becomes future automation.
|
||||
|
||||
Reference:
|
||||
- [[id:971cd9e7-2cc5-4743-8042-2469dbe4078f][CL Modernization]] — the project that builds the prover and modernizes the CL ecosystem
|
||||
- [[id:dddd52a7-adb8-470e-a459-614ade5f76af][Closing the Lisp Gap]] — detailed performance and ecosystem analysis
|
||||
- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Passepartout]] — the architecture that houses the prover
|
||||
Reference in New Issue
Block a user