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: 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: 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;
• OCaml for the implementation, Rocq for the proofs, extraction binding the two;
• applications as propositions everywhere: no relation application in term position, statements about results written flat as membership;
• relation references as a term kind, written #Name: relations as data for transitions, higher-order arguments, and the catalog.

Core Design Principles and Pipeline Specification

See: docs/core-design-and-pipeline.org

It describes the deeper design principles behind Sol and the compiler/interpreter pipeline that preserves totality, as implemented in lib/.

Topics covered 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:

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

This document should explain how Sol remains expressive while avoiding the unrestricted partiality of ordinary Turing-complete languages.

Virtual Machine Specification

See: docs/virtual-machine-specification.org

It describes the runtime architecture that executes Sol programs, as implemented in lib/ and theories/, and what the runtime owes the future.

Topics covered 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

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. Worked examples live in examples/ (see examples/README.org); machine checked proofs in theories/ (structural and lexicographic decrease, extracted into admission; the interval characterizations behind propagation).

Tooling: sol lsp is a language server publishing admission diagnostics (totality, schemas, integrity) as you type; editors/emacs/sol-mode.el provides highlighting, navigation, an inferior REPL and eglot wiring. See docs/tooling.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.

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.