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

project index: what+why only, no jargon without links; architecture: explain Lisp and ACL2 at first mention

Browse Source
This commit is contained in:
Hermes
2026-05-24 19:57:55 +00:00
parent 73dea1f654
commit 5086ac4fbe
3 changed files with 37 additions and 18 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
projects/passepartout/architecture/architecture.org
View File

@@ -22,7 +22,7 @@ Each is described below.
**The environment: one address space.**
The environment eliminates the layered trust model of a conventional OS by eliminating the layers. Instead of an editor that sends keystrokes through a terminal emulator to a shell that forks processes that read files through a kernel VFS layer — each boundary a potential vulnerability — the environment runs everything in a single Lisp address space.
The environment eliminates the layered trust model of a conventional OS by eliminating the layers. Instead of an editor that sends keystrokes through a terminal emulator to a shell that forks processes that read files through a kernel VFS layer — each boundary a potential vulnerability — the environment runs everything in a single Lisp address space. (Lisp is a family of programming languages where code and data share the same representation. This property means the machine can verify what code does and modify itself without restarting. It is the foundation that makes the entire architecture possible.)
The editor is a Lisp function that manipulates text buffers in the evaluated memory graph. The shell is a Lisp read-eval-print loop that compiles to the same evaluator. The browser renders HTML through a Lisp-based rendering engine, not a separate process. The agent runtime invokes Lisp functions, not subprocesses. (The specific implementations that realize this today use Lish for the shell and editor, Nyxt for the browser, and SBCL as the host Lisp — but the architectural principle is uniform semantics in one address space, not these particular packages.)
@@ -53,7 +53,7 @@ The gate is a function that takes (action, context, policy) and returns (permit
The gate combines two decision layers:
1. ACL2-verified decision procedures for security-critical checks — access control, message authentication, capability resolution. These are provably correct for their domain.
1. ACL2-verified decision procedures for security-critical checks — access control, message authentication, capability resolution. (ACL2 is a theorem prover and programming language for formal verification. It proves that code behaves correctly for all possible inputs, not just the ones tested.)
2. An LLM for natural-language reasoning — parsing the user's intent, evaluating whether an action falls within policy boundaries that require human judgment.
The LLM layer is probabilistic. The ACL2 layer is deductive. The gate architecture ensures the deductive layer is authoritative where it applies and the probabilistic layer is bounded by it — the LLM cannot overrule a verified denial.