23 lines
1.1 KiB
Org Mode
23 lines
1.1 KiB
Org Mode
: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.
|