core design and pipeline document

1 files changed, 13 insertions, 10 deletions

diff --git a/README.org b/README.org
index 4485f07..94ab342 100644
--- a/README.org
+++ b/README.org
@@ -74,12 +74,13 @@ It covers:
 
 ** Core Design Principles and Pipeline Specification
 
-This document has not been written yet.
+See: [[file:docs/core-design-and-pipeline.org][docs/core-design-and-pipeline.org]]
 
-It should describe the deeper design principles behind Sol and the
-compiler/interpreter pipeline needed to preserve totality.
+It describes the deeper design principles behind Sol and the
+compiler/interpreter pipeline that preserves totality, as
+implemented in =lib/=.
 
-Expected topics include:
+Topics covered include:
 
 - why Sol is intentionally not Turing complete;
 - how Sol relates to Prolog, Coq, Datalog, and relational algebra;
@@ -188,10 +189,12 @@ Build with =nix develop -c dune build=; run the tests with =nix
 develop -c dune runtest=; run a program with =dune exec sol --
 file.sol=.
 
-The next documents to produce are:
-
-1. =docs/core-design-and-pipeline.org=
-2. =docs/virtual-machine-specification.org=
+Machine checked proofs live in =theories/=: the admission checker's
+core claim, that strict containment decreases a well founded
+measure, is proven in Rocq and compiled as part of the default
+build.
 
-These should build on the language specification, the integration
-decisions, and the implementation as it stands.
+The next document to produce is
+=docs/virtual-machine-specification.org=, building on the language
+specification, the integration decisions, and the implementation as
+it stands.