1 files changed, 176 insertions, 0 deletions
diff --git a/README.org b/README.org
new file mode 100644
index 0000000..5de75cf
--- /dev/null
+++ b/README.org
@@ -0,0 +1,176 @@
+#+TITLE: Sol
+
+Sol is a total relational language inspired by Prolog, Coq, relational
+algebra, constraint logic programming, and the message-oriented syntax
+of Smalltalk.
+
+The project explores a language where relations are the primary
+semantic objects, types are expressed as membership criteria, and
+execution is understood as proof search, constraint propagation, and
+normalization.
+
+Sol is intentionally not Turing complete. Its purpose is not to encode
+arbitrary partial computation, but to provide a disciplined environment
+for total relational computation, dependent relational typing, and
+integrity-preserving constraint systems.
+
+* Design
+
+** Language Specification
+
+The first document defines the surface language and its semantics.
+
+See: [[file:docs/language-specification.org][docs/language-specification.org]]
+
+This document covers:
+
+- core syntax;
+- atoms, labels, variables, literals, and blocks;
+- relation applications;
+- explicit conjunction and disjunction;
+- joins through unification;
+- domains as unary relations;
+- infinite domains as membership constraints rather than enumerators;
+- membership criteria;
+- constraints as relations;
+- existential and universal quantification;
+- recursion and totality;
+- higher-order relations;
+- primary and secondary type systems.
+
+This is the foundational document for Sol as a language.
+
+** Sol / Sakura / RNT Integration
+
+This document records the normative architectural decisions binding
+Sol to the Sakura relational engine and the RNT database kernel.
+
+See: [[file:docs/sakura-RNT-integration.org][docs/sakura-RNT-integration.org]]
+
+It covers:
+
+- totality as a stack-wide invariant (the Turing-complete PPL idea is
+  retracted; partiality lives in the application layer);
+- Sol as the database language and runtime, with Karuta compiling to
+  it;
+- the sublanguages (DRL, ICL, DCL, DML, DDL, TCL) as semantic
+  fragments of Sol rather than separate surface languages;
+- transitions (DML, DDL, DCL) as relations over first-class,
+  content-addressed branch states;
+- commit (advancing a branch tip) as the single primitive effect —
+  the kernel arbitrates only the tip; conflict policy is DCL;
+- Sol as a host-neutral library over a =WORLD= interface, linked
+  in-process by RNT as its higher-order execution engine and by a
+  thin standalone host;
+- sequencing by linear state threading (Mercury-style), never by
+  syntactic order;
+- state-scoped reads (=at:=);
+- plan selection by analysis (no DRL surface syntax);
+- totality established at admission via a closed evidence ladder,
+  with checkers verified in Rocq;
+- the catalog as ordinary queryable relations;
+- subtyping as proven relation inclusion, intensional relation
+  identity, and canonical representatives for quotient domains.
+
+** Core Design Principles and Pipeline Specification
+
+This document has not been written yet.
+
+It should describe the deeper design principles behind Sol and the
+compiler/interpreter pipeline needed to preserve totality.
+
+Expected topics include:
+
+- why Sol is intentionally not Turing complete;
+- how Sol relates to Prolog, Coq, Datalog, and relational algebra;
+- relations as dependent types;
+- membership checking as typing;
+- constraints as ordinary relations;
+- equality as a relation with special operational capabilities;
+- the distinction between membership, constraint propagation, and
+  generation;
+- termination and totality strategies;
+- structural recursion;
+- bounded enumeration;
+- symbolic solving;
+- stratified negation;
+- finite-world reasoning;
+- higher-order relation restrictions;
+- proof obligations and certificates.
+
+It should also describe the expected pipeline:
+
+#+BEGIN_EXAMPLE
+source text
+  parsing
+  AST construction
+  relation-expression normalization
+  schema checking
+  variable and scope analysis
+  unification planning
+  constraint planning
+  totality checking
+  solver selection
+  proof/search execution
+  residual constraints or normalized result
+#+END_EXAMPLE
+
+This document should explain how Sol remains expressive while avoiding
+the unrestricted partiality of ordinary Turing-complete languages.
+
+** Virtual Machine Specification
+
+This document has not been written yet.
+
+It should describe the runtime architecture required to execute Sol
+programs.
+
+Expected topics include:
+
+- VM object model;
+- relation objects;
+- domain relations;
+- query objects;
+- rule objects;
+- variables and logic cells;
+- substitutions;
+- unification store;
+- constraint store;
+- conjunction and disjunction execution;
+- equality handling;
+- membership checking;
+- relation indexes;
+- finite relation scans;
+- symbolic solver hooks;
+- quantifier execution;
+- tabling and memoization;
+- totality-preserving search;
+- bounded generation;
+- integrity-control hooks;
+- interaction with stored relations;
+- error and proof-obligation reporting.
+
+The VM specification should explain how Sol expressions are evaluated
+without becoming an unrestricted Prolog runtime.
+
+In particular, it should make clear how the VM distinguishes:
+
+- checking membership;
+- accumulating constraints;
+- solving symbolically;
+- enumerating finite relations;
+- bounded generation;
+- and rejecting non-total execution plans.
+
+* Current Status
+
+At the moment, the project has a working conceptual direction and a
+language specification draft.
+
+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.