diff options
Diffstat (limited to '')
| -rw-r--r-- | README.org | 17 |
1 files changed, 9 insertions, 8 deletions
@@ -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. |