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

Remove old design-decisions.org, update cross-refs to design/ folder

Browse Source
This commit is contained in:
Hermes
2026-06-04 20:24:17 +00:00
parent 2ee60b5b4a
commit 9ce3883005
5 changed files with 8 additions and 87 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
projects/passepartout/architecture/lisp-foundation.org
View File

@@ -7,7 +7,7 @@
#+filetags: :passepartout:architecture:common-lisp:prover:ACL2:HOL:
#+STATUS: active
Passepartout's architecture — verified gate, single address space, self-modifying agent — depends on running on a Lisp that can be proved correct. This document explains why Lisp is the right foundation, what gaps remain in the current ecosystem, and how the prover bootstraps from ACL2 to a verified HOL kernel to a self-verifying stack. It is the "Lisp layer" of the architecture, alongside the four-subsystem description in [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][architecture.org]] and the design rationale in [[id:0a33bd83-ff3c-4eac-bc97-83eb6702051a][design-decisions.org]].
Passepartout's architecture — verified gate, single address space, self-modifying agent — depends on running on a Lisp that can be proved correct. This document explains why Lisp is the right foundation, what gaps remain in the current ecosystem, and how the prover bootstraps from ACL2 to a verified HOL kernel to a self-verifying stack. It is the "Lisp layer" of the architecture, alongside the four-subsystem description in [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][architecture.org]] and the design rationale in [[id:e32290a0-a02a-4af7-ae22-243d04a7ac82][Design Decisions]].
* What It Is and Why