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