embedding surface, host world test, deep recursion, line tracking

1 files changed, 25 insertions, 4 deletions

diff --git a/README.org b/README.org
index 5de75cf..4485f07 100644
--- a/README.org
+++ b/README.org
@@ -164,13 +164,34 @@ In particular, it should make clear how the VM distinguishes:
 
 * Current Status
 
-At the moment, the project has a working conceptual direction and a
-language specification draft.
+The language has a specification, a set of normative integration
+decisions, and a working first implementation in OCaml:
+
+- a parser for the surface syntax under the delimiter law;
+- a loader whose admission enforces totality: structural decrease
+  witnesses on recursive rules, schema and domain checks on facts,
+  membership criteria (refinements and foreign keys) solved against
+  the complete extension;
+- a solver with dynamic goal selection, so conjunction is
+  commutative in fact and non total plans are rejected instead of
+  attempted;
+- decidable negation, Exists and ForAll;
+- backward-solving arithmetic over the integers and rationals with
+  minimal shape preserved;
+- a =WORLD= functor for embedding, exercised by a host-defined
+  catalog in the tests, and a standalone binary with a REPL.
+
+See =docs/vm.org= for behavior, =docs/terms.org= for the term
+algebra.
+
+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=
 
-These should build on the language specification and clarify how Sol
-can be implemented while preserving totality.
+These should build on the language specification, the integration
+decisions, and the implementation as it stands.