amr/hermes-brain
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Create CL Modernization project — merge initiatives, corrected phases, and timeline into single comprehensive project page under projects/

Browse Source
This commit is contained in:
Hermes
2026-06-03 18:33:47 +00:00
parent 9553a90060
commit 179bcbaaa4
6 changed files with 205 additions and 119 deletions
Download Patch File Download Diff File Expand all files Collapse all files

22
ideas/cl-modernization-corrected-phases.org
View File

@@ -1,22 +0,0 @@
: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.

31
ideas/cl-modernization-initiative.org
View File

@@ -1,31 +0,0 @@
: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

66
ideas/cl-modernization-timeline.org
View File

@@ -1,66 +0,0 @@
: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