virtual machine specification document

1 files changed, 9 insertions, 8 deletions

diff --git a/README.org b/README.org
index 94ab342..40d59e2 100644
--- a/README.org
+++ b/README.org
@@ -121,12 +121,13 @@ the unrestricted partiality of ordinary Turing-complete languages.
 
 ** Virtual Machine Specification
 
-This document has not been written yet.
+See: [[file:docs/virtual-machine-specification.org][docs/virtual-machine-specification.org]]
 
-It should describe the runtime architecture required to execute Sol
-programs.
+It describes the runtime architecture that executes Sol programs, as
+implemented in =lib/= and =theories/=, and what the runtime owes the
+future.
 
-Expected topics include:
+Topics covered include:
 
 - VM object model;
 - relation objects;
@@ -194,7 +195,7 @@ core claim, that strict containment decreases a well founded
 measure, is proven in Rocq and compiled as part of the default
 build.
 
-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.
+The design documents promised at the project's start now all exist:
+the language specification, the integration decisions, the core
+design and pipeline document, and the virtual machine
+specification.