From e4c9579b02951e9edd84c4dae4bf10cfdc5953dc Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 21:55:18 -0300 Subject: core design and pipeline document --- README.org | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) (limited to 'README.org') 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. -- cgit v1.2.3