From 1832aca3f545f1f6ecadb7e12ed1ce02c2aa78be Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 21:56:53 -0300 Subject: virtual machine specification document --- README.org | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'README.org') 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. -- cgit v1.2.3