#+TITLE: Sol / Sakura / RNT Integration #+AUTHOR: Marcos Magueta * Purpose This document records the architectural decisions binding Sol to the Sakura relational engine (=../sakura=) and the RNT database kernel (=../RNT=). These decisions were reached by adversarial design review (2026-07-11) and are normative: later documents (the pipeline specification and the VM specification) must not contradict them without revisiting the arguments recorded here. * The Stack, As It Exists Facts established from the codebases, not decisions: - *RNT* is a database kernel currently being rewritten in OCaml (the original execution core was C++; its design carries over). Its execution core, *FOL* (=lib/backend/execution/FOL.ml=), mechanically evaluates first-order relational plans under the Volcano pull model. Every plan terminates: evaluation is model checking against one fixed, finite model, which is decidable. RNT makes no independent termination judgements; it trusts plan annotations. - *Sakura* (OCaml) is the authoritative source of semantics. It owns cardinality analysis (=Finite= / =ConstrainedFinite= / =AlephZero= / =Continuum=), termination enforcement (=TAKE= insertion), join ordering, and physical storage. - Sakura's sublanguages are cleanly separated modules: DRL (pure retrieval, total), ICL (integrity constraints as membership checks), DCL (branch management and 3-way merge over content-addressed tips), DML (delta semantics), DDL, with TCL planned. - =sublanguage.ml= classifies operations categorically: a *Query* is a natural transformation between instance functors (state unchanged); a *Transition* is a morphism in the category of database states. - RNT tuples are content-addressed: each tuple is stored under the SHA256 digest of its serialized bytes. DCL branches point to tips identified by hash. Database states are therefore already first-class Merkle-style values in this architecture. - *Karuta* is a Prolog-like language targeting the BEAM, positioned at the application layer. * Decision 1: Totality Is a Stack-Wide Invariant ** The decision Sol is total, and so is the entire database language stack. The previously entertained idea of a Turing-complete PPL (predicate procedure language) — recorded in =sakura/lib/sublanguage.ml= ("PPL -> new effect class: potentially non-terminating computation") and in =karuta-integration.org= ("a predicate procedure language might [be Turing complete]") — is *retracted*. Problems that genuinely require Turing-complete computation belong in the application layer (Karuta on the BEAM), not in the database. ** The argument - P1. A very large class of useful programs is expressible in a total language: arithmetic, data-structure algorithms, parsers, theorem provers, sorting, type checkers, relational evaluators — anything whose recursion is structural and provably terminating. - P2. Admitting unbounded recursion anywhere in the stack re-imports the halting problem into every layer above it, destroying the termination guarantee that RNT's execution core is *named after* (see =RNT/new-docs/fol.org=: "do not make the query language Turing-complete"). - P3. Stored procedures are the layer where users write the most logic; that is the worst possible place to lose the guarantee. - C. Therefore the database language is total, with no partial escape hatch inside the database. Partiality lives outside, in the application layer. * Decision 2: Sol Is the Database Language; Karuta Compiles to It ** The decision - Sol is *the* language of the Sakura/RNT RDBMS, and its VM is the database runtime. It plays the role SQL plays in PostgreSQL: the language exposed at the REPL and over the wire. - Karuta remains the application-layer language. It compiles to the s-expression interchange form and internally targets Sol; this compilation happens *inside Sakura* — Sakura hosts the Karuta front-end and lowers it onto Sol, the same way it receives Sol directly from the REPL or the wire. Karuta does not front the sublanguages directly anymore; Sol does. - The sublanguages (DRL, ICL, DCL, DML, DDL, TCL) are not separate surface languages. They are fragments of Sol, distinguished semantically (query vs. transition), not syntactically balkanized as in SQL. ** The argument - P1 (uniformity requirement). A stored relation and a computed relation must be handled identically: the same application syntax, the same membership semantics. "The same way we handle a relation stored in the database, we invoke a function facing a relational interface." - P2. Two surface languages over one semantic core is the negation of uniformity — it reproduces the SQL disease: a *collection* of sublanguages with no harmonic whole. - C. One language, Sol. Everything else (Karuta included) is a compiler front-end or client of it. * Decision 3: Transitions Are Relations Over Database States ** The decision Sol expresses state change (DML, DDL, DCL) as *relations between database states*. A database state =S= is a first-class value — which the architecture already supports, since tuples are content-addressed and branch tips are hashes. An insert is a relation: #+BEGIN_SRC sol [Insert relation: Person tuple: T before: S after: S'] #+END_SRC This proposition holds exactly when state =S'= is state =S= with =T= admitted into =Person= (which entails =T= passing every ICL constraint attached to =Person= — membership checking and integrity control are the same operation, per the language specification). Exactly *one* primitive effect exists, outside the logic, at the edge: *commit* — advancing a branch tip (HEAD) from =S= to =S'=. As in git: everything is pure value manipulation until the single mutable reference moves. ** The alternatives rejected - *Two-layer language* (pure core + imperative command shell, à la Haskell IO): honest, but bifurcates the grammar into expressions and commands — DML becomes a foreign sublanguage again, violating Decision 2's uniformity premise. - *Smalltalk message-sends with hidden effects* (=Person insert: T= mutating in place): the surface says "message", the internals perform a state morphism. Dishonest syntax — the construct's surface form would not mean what the internals do. Rejected on the syntax-honesty principle. ** The argument - P1 (uniformity). Transitions expressed as relations use the same application syntax, the same conjunction, the same proof-search semantics as everything else in Sol. - P2 (fact). Database states are already first-class Merkle values in RNT/Sakura (content-addressed tuples, hash-identified branch tips). State-as-value is not an invention; it is a recognition. - P3 (honesty). =sublanguage.ml= already classifies DML/DDL/ICL/DCL as morphisms in the category of database states. Making the states and the morphism explicit in the surface syntax makes the language say exactly what the semantics do. - C. An insert *is* a relation over states. ** What this buys Because =Insert(R, T, S, S')= is an ordinary proposition, it can be *queried* as well as *performed*: - provenance and audit are ordinary conjunctions over the state chain; - time-travel queries are membership checks against old states; - dry-run is evaluating the transition relation without committing; - a transaction is a composition of transition relations =S → S' → S''=, committed atomically by moving HEAD once, to the final state; - DCL merge is already a ternary relation over states (two tips and an ancestor) — Decision 3 makes the rest of the language match it. ** Acknowledged costs - State identity and equality must be defined precisely (hash equality of content-addressed states is the candidate, but canonical serialization must be specified). - Sequencing becomes conjunction over chained state variables; the planner must order these chains. This is real planning work, though of the same kind DCL merge already performs. * Decision 4: Sol Is a Library; RNT Links Its Compiler and VM In-Process ** The decision Sol — the whole pipeline: normalizer, planner, totality checker, and VM — is built as a host-neutral OCaml library, parameterized over a =WORLD= interface: the store that answers which relations exist, their capabilities, how membership is checked against stored tuples, and what commit means. Two hosts consume it: - *Standalone Sol*: a thin binary links the library with an in-memory or file-backed world. This world exposes only the pure fragment: no branches exist, so transition relations and commit are simply absent capabilities (see Decision 5). This satisfies the requirement that Sol be usable as a separate language for ordinary (total) programs. - *RNT*: the kernel links the library in-process as its execution layer. RNT's planned split between "terminating first-order logic and higher-order logic execution" is filled directly: the FOL core executes the finite-plan fragment (=Plan.t=, Volcano), and the HOL slot *is* Sol's engine — not a reimplementation, the same compiler internals. The world is the object manager plus the content-addressed store; commit advances a branch tip atomically inside the kernel. ** The argument The earlier framing — "Sol VM inside the kernel" versus "Sol VM as a client of the kernel" — was a false dichotomy. - P1 (requirement). Sol must run standalone, with no database present. - P2 (Decisions 2–3). Sol's VM is the database runtime, and commit — the single effect — must be atomic against RNT's branch tips. - P3. A client-process VM satisfies P1 but makes the only effect distributed, breaking P2. A kernel-welded VM satisfies P2 but cannot exist without the database, breaking P1. - C. The VM must be neither: a library over an abstract world. RNT linking it in-process preserves atomicity; the standalone host preserves independence. One implementation, two hosts — an embeddable runtime in the manner of SQLite or Lua, where one of the embeddings is the database kernel itself. The language specification already gestures at this seam: membership criteria "constructed at the host language," capabilities as declared operational permissions, =World= as a relation. The =WORLD= interface is that seam made explicit. ** Acknowledged costs - The world interface is a hard public contract. Capability negotiation — which worlds support enumeration, solving, bounded generation — must be specified precisely. - Standalone-world semantics must be a strict subset of database-world semantics, so that a program proven total against the standalone world remains total in-kernel. * Decision 5: A State Is a Branch's Whole Tree ** The decision The state values =S=, =S'= in transition relations denote *branch states*: the catalog, schemas, ICL constraints, and the extension of every relation *as one branch sees them*, as one content-addressed tree — exactly a git commit object. Concretely, =S= is the Merkle root hash of the branch's tree: a snapshot handle into the content-addressed store, cheap to hold, structurally shared with neighboring states. There is no global "database state" spanning branches. Transition relations are meaningful only within a branch: a stored procedure receives the branch's current root hash, evolves it purely — each transition producing the successor hash — and yields the final hash, which commit installs as the new tip. It works like git: all value manipulation is pure; history is a chain of whole-database states; the single effect (Decision 3) is advancing a branch tip to a new state. Consequently, transition relations exist only in the RNT/Sakura world. The standalone world has no branches, hence no transitions and no commit — standalone Sol is the pure total fragment. This is capability negotiation (Decision 4) doing its job, not a special case. ** The alternative rejected Per-relation states — the database as a bag of independently versioned relations — fail on two counts: - P1. DDL and ICL changes are also transitions (Decision 2); a per-relation state has no place to record "the schema changed" or "a constraint was added." - P2. Integrity constraints span relations (foreign keys as membership checks against *other* relations). A transition's validity must be judged against a consistent snapshot of all relations, or ICL checking is unsound. - P3 (fact). DCL already works on whole tips: a branch is one hash, and 3-way merge operates on two tips and an ancestor. Nothing is lost: in a content-addressed tree, per-relation hashes still exist as internal nodes, and unchanged subtrees share structure. ** Acknowledged costs - Hashing must be incremental — a transition recomputes hashes along the changed path only (O(path), not O(database)) — or commit throughput dies. Merkle trees provide exactly this. - Canonical serialization of states must be specified early; state equality is hash equality only if serialization is deterministic. * Decision 6: Sequencing Comes from Linear State Threading, Not Syntax Order ** The decision Transition sequencing derives *solely* from state-variable sharing, never from syntactic position: #+BEGIN_SRC sol [Insert relation: Person tuple: T1 before: S0 after: S1] :and [Insert relation: Person tuple: T2 before: S1 after: S2] #+END_SRC =:and= remains honestly commutative: swapping the conjuncts changes nothing, because the chain =S0 → S1 → S2= is carried by unification. The planner topologically sorts the state chain, the same discipline Sakura already applies when ordering joins by variable binding. State variables obey a *linear discipline*, in the manner of Mercury's =di=/=uo= (destructive-input / unique-output) modes on =io.state=: within a transaction, each state value is consumed exactly once (as =before:=) and produced exactly once (as =after:=). The felt experience is procedural — a timely order, step after step — but the order is implied by the dataflow, not decreed by the page. A transaction is a relational expression whose state variables form one linear chain from the branch tip (=S0= = HEAD) to a final state, followed by one commit of that final state (Decision 3). ** The argument - P1. =:and= means logical conjunction, and conjunction is commutative. - P2 (syntax honesty). The surface form must mean what the internals do. If evaluation order were read off the page, =:and= would be a lie — sequencing dressed as conjunction. This is the same sin the language specification already rejects in "newline adjacency secretly means conjunction." - P3. Unification is Sol's only binding mechanism; threading state through shared variables introduces no new primitive. - C. Order-from-dataflow is the only admissible sequencing. The linear mode discipline makes chain-hood a static property: a fork (two transitions consuming the same =S=) or a reuse is a mode error caught at admission, not a planner heuristic. ** Sugar policy A convenience form (e.g. a =Transaction do:= that auto-threads the state variables) is permitted *only* as sugar with a published elaboration into the explicit chain. It must never become a primitive with its own semantics. ** Acknowledged costs - Verbosity until sugar lands: users name =S0=, =S1=, =S2= explicitly. - The mode/linearity checker must be specified as part of admission checking, alongside schema and totality checks. * Decision 7: Reads Are State-Scoped ** The decision In the RNT/Sakura world, *every* read of a stored relation happens from an explicit state. In the core language, a stored-relation application carries the state it reads at: #+BEGIN_SRC sol [Person id: P age: A at: S1] #+END_SRC A scoping form is provided as sugar, with a published elaboration that distributes the state over the stored-relation applications in its body (Decision 6's sugar policy): #+BEGIN_SRC sol [At state: S1 body: [Person id: P age: A] :and [Adult person: P]] #+END_SRC At the REPL, a bare query elaborates to =at:= the current branch tip's state — one uniform rule, not a second semantics. Standalone Sol is untouched: it has no stored relations, hence no =at:=. ** The argument - P1 (Decision 6). Order on the page carries no meaning; so "read whatever the previous statement produced" is not available — it is positional order, the outlawed lie. - P2. Reads must therefore name their state, or a hidden convention decides — dishonest syntax. - P3. The alternative — all reads pinned to the transaction's initial =S0= — makes read-your-own-writes inexpressible: a procedure that inserts and then validates against the result cannot be written, even though ICL checking inside the chain already reads intermediate states. The language would forbid users what its own machinery does. - C. Reads are state-scoped in the core; terseness is recovered by sugar, never by convention. ** Acknowledged costs - =at:= becomes a reserved label on stored-relation applications; it cannot be a schema attribute name. - The elaboration of =At state: body:= must be specified precisely, including its interaction with nested =At= forms (innermost wins) and with transition relations (which are already explicit and are not rescoped). * Decision 8: The Kernel Arbitrates Only the Tip; Conflict Policy Is DCL ** The decision The only point of contention in RNT is the tip of a branch. The kernel therefore provides exactly one concurrency primitive: *atomic compare-and-swap on a branch tip* — install =Sn= as the tip iff the tip still equals the =S0= the transaction started from. Everything above that primitive is the version-control language's domain, and DCL is a fragment of Sol (Decision 2) operating on states as values (Decision 5): - *fast-forward*: the tip is an ancestor of =Sn= — install directly; - *rebase*: re-execute the procedure from the new tip — sound and safe because a transaction is a pure, total function of its initial state (Decisions 3, 6); nothing partial ever escaped; - *3-way merge*: already a ternary relation over two tips and their ancestor, with declared strategies (=PreferLeft=, =PreferRight=, =RevertToAncestor=). Conflict policy is thus *expressed in the language*, not hardcoded in the kernel. ** The argument - P1. A pure total transaction has no partial effects to undo; re-execution from a moved tip is always safe and always terminates. The classical difficulty of transaction retry does not exist here. - P2. Given P1, any policy the kernel could hardcode (retry, merge, reject) is expressible as relations over states — and DCL already contains the vocabulary. - P3 (minimality). A kernel primitive should exist only where the kernel is the sole possible arbiter. Tip installation is the one such place; policy is not. - C. Kernel = CAS on the tip. Policy = DCL, in Sol. ** Acknowledged costs - Any retry/arbitration loop is unbounded under contention. It lives outside the total language — in the commit arbiter or client, alongside the REPL loop. Sol proves each execution terminates; the arbiter decides how many executions happen. Partiality is confined to that boundary and must be documented as such, with a fairness/backoff policy. * Decision 9: No DRL Syntax — the Plan Is Chosen by Analysis ** The decision There is no distinguished DRL surface form. The user writes uniform Sol; the planner decides how each subexpression executes. Since *both* engines are total, engine choice is not a semantic distinction and must not be a syntactic one: it changes performance, never meaning (Codd's theorem licenses the lowering — the finite first-order fragment and the plan algebra are the same queries). What actually distinguishes subexpressions is what their relations *are*: - *stored relations* — scanned at an explicit state =S= (Decision 7); - *ephemeral relations* — algebraic artifacts of relational operations, carrying provenance and lineage (Sakura's existing notion); - *rule- and procedure-defined relations* — unfolded, or evaluated by fixpoint on Sol's engine. The planner — reusing Sakura's cardinality propagation (=Finite= / =ConstrainedFinite= / =AlephZero= / =Continuum=), constraint propagation, boundness/mode analysis, and join ordering — identifies maximal finite, first-order, non-recursive subexpressions and lowers them to the plan algebra (=Plan.t=) for RNT's FOL core. Everything else runs on Sol's engine, which pulls from lowered plans as cursors (Volcano composes across the seam). ** The argument - P1 (Decision 2). Sublanguages are semantic fragments, not syntactic ones; a DRL marker would re-balkanize the language. - P2 (totality, Decision 1). Both engines halt, so there is no observable semantic difference for a marker to honestly denote. - P3 (fact). Sakura already computes the needed evidence — cardinality tags, TAKE insertion, boundness-driven join ordering. The lowering criterion reuses existing analysis. - C. Fragment-by-analysis. The FOL core is an invisible optimization target; the observable contract is only the tuple stream. ** Acknowledged costs - Each lowering must be meaning-preserving and should be checkable (the =Plan.t= translation is a verifiable step, not a trusted one). - A user who needs the guarantee "this runs as a flat finite plan" gets it as a declarable *assertion* (reject if not lowerable), never as a separate language. * Decision 10: Totality Is Established at Admission, Verified in Rocq ** The decision Totality evidence is checked at *admission time*: defining a rule or procedure is itself a DDL transition (=[DefineRule ... before: S after: S']=), and the definition fails — the successor state does not come to exist — unless the evidence is present. A state containing a non-total rule is unrepresentable; queries therefore run against states where everything is already proven total and pay nothing at query time. The evidence is a closed ladder; each rung is recorded in the rule's metadata: 1. *Structural decrease* — the checker finds a strictly decreasing argument (e.g. =Tail= < =[Head | Tail]= in =Length=). Automatic; covers most honest recursion. 2. *Bounded quantification* — the searched space is =Finite= or =ConstrainedFinite= by Sakura's cardinality analysis. 3. *Symbolic discharge* — algebraic properties prove the universal or the recursion (e.g. =Plus(X, 0) = X= over all integers). 4. *Certificate* — a Rocq proof, checked before admission. Because the certificate is verified, this rung is not a trusted escape hatch. A merely *trusted* declaration remains possible only as a last resort: named, auditable, and loud. Anything fitting no rung is *rejected* — never admitted as a pending obligation. Two levels, not conflated: - *Object level*: the ladder above, run by the in-engine admission checker on each definition. - *Metatheory*: Rocq/Coq proves the guarantees of RNT/Sakura themselves — soundness of the admission checker ("any accepted rule is total"), meaning-preservation of the =Plan.t= lowering (Decision 9), soundness of ICL checking, and merge respecting its specification. Since RNT and Sakura are OCaml, the critical checkers should be *extracted* from Rocq to OCaml, so the thing proven is the thing running. ** The argument - P1 (Decision 5). States are values. A state containing an unproven rule is a state whose queries might not halt; admitting it falsifies the totality invariant *inside* every descendant state. - P2. "Obligation pending" is Coq's =admit=: tolerable in an interactive proof, poisonous in a database that other parties query concurrently. - P3. A checker that is itself unverified moves the trust boundary rather than discharging it; the Rocq metatheory closes that gap. - C. Total-or-absent at admission; verified checker; certificates as proofs, not promises. ** Acknowledged costs - The structural-decrease checker and the symbolic-discharge engine must be specified precisely (the pipeline document owns this). - Rocq extraction constrains implementation style in the affected modules (pure, extraction-friendly OCaml). - Proof maintenance is a real, ongoing cost paid for the guarantee that is the project's entire premise. * Decision 11: The Catalog Is Relations ** The decision Everything in a state is a relation, and everything is queryable — including the catalog itself. Relation definitions, schemas, rules, constraints, and capabilities are tuples in catalog relations, stored in the same content-addressed tree, read at a state like anything else: #+BEGIN_SRC sol [Relation name: N schema: Sch at: S] [Constraint name: C relation: R body: B at: S] #+END_SRC (A concrete catalog plan already exists on the Sakura/RNT side; this decision binds Sol to it.) ** What follows - DDL is DML on catalog relations: =DefineRelation= is an insert into the catalog — one mechanism, not two (Decision 3 already made DDL a transition; this removes its last special machinery). - Admission checking (Decision 10) becomes ICL on the catalog: "a rule tuple enters =Catalog.Rule= only with totality evidence" is an ordinary integrity constraint on an ordinary relation. - Introspection is an ordinary query at =S= — which merge, migrations, and tooling need anyway. ** The argument - P1 (Decision 2). A catalog reachable only through special forms is a second interface — the SQL disease; =information_schema= is SQL's own admission that it bolted this on too late. - P2. Catalog-as-relations lets Decisions 3 and 10 collapse into existing machinery instead of demanding parallel mechanisms. - C. The catalog is stored relations, guarded by ICL, versioned in the tree, queryable in Sol. ** Acknowledged costs - Metacircular bootstrap: the catalog's schema must describe itself (the fixed point every self-describing catalog has — Postgres's =pg_class= describes =pg_class=), and some base constraints must be primitive rather than ICL-expressed. * Decision 12: Subtyping Is Proven Inclusion; Identity Is Intensional; Quotients Are Canonical ** The decision Sol's type system represents subtyping, and it is *semantic* subtyping — subtyping is relation inclusion: #+BEGIN_EXAMPLE S <: T ≜ ∀x. S(x) → T(x) #+END_EXAMPLE Subsumption is not a rule added to the logic; it is the transitivity of membership: =x ∈ S ∧ S ⊆ T ⊢ x ∈ T=. A refinement is a subtype by construction (it is an intersection). =Natural <: Integer= because ℕ ⊆ ℤ. Three clauses make this precise: *** (1) Inclusion judgments go through the evidence ladder =S <: T= is a universal over a possibly infinite domain — undecidable in general. A subtyping judgment is therefore admitted by exactly the regime of Decision 10: - declared-and-checked facts for the base lattice (=Natural <: Integer= lives in the catalog, queryable, per Decision 11); - symbolic discharge for refinements (constraint implication: =x ≥ 18 → x ≥ 0=); - finite scan for finite relations; - Rocq certificate otherwise. Inclusion between arbitrary relations is never silently inferred. *** (2) Relation identity is intensional, never structural Two relations with identical label sets are not the same relation. Identity comprises the schema *and* the membership criterion (the intension) — one relation conjoined with a =GreaterThan= constraint is semantically different from its unconstrained twin — and, for ephemeral relations, provenance and lineage (Sakura's existing notions). Consequently: - shape implies nothing: no structural typing, no implicit width subtyping; - a tuple with more labels does not silently inhabit a narrower-schema relation — *projection* is the explicit morphism for forgetting attributes, and it stays explicit. *** (3) Quotient domains use canonical minimal-shape representatives Rationals expose the classical quotient problem: ℚ is ℤ × (ℤ∖{0}) quotiented by =(a,b) ~ (c,d) ⟺ ad = bc=, so ={numerator: 2 denominator: 2}=, ={numerator: 1 denominator: 1}=, and =1= all denote one value. Sol resolves quotients by *canonical representatives*, enforced by the domain's own membership criterion, and canonicalization picks the *minimal shape*: an integer-valued rational normalizes to the ground integer itself (={numerator: 2 denominator: 2}= normalizes to =1=, not to ={numerator: 1 denominator: 1}=). Therefore ℤ ⊂ ℚ holds *literally, as membership inclusion* — representation does not limit inclusion, and no injection or coercion machinery exists. Non-canonical pairs are pre-values that normalize in, via a normalization relation declared as part of the domain's catalog definition: #+BEGIN_SRC sol [RationalNormalize raw: {numerator: 2 denominator: 2} canonical: 1] #+END_SRC The alternative — setoids, where all representatives are members and every relation carries congruence obligations with a per-domain =Equal= — is rejected: congruence proofs metastasize over every rule ever defined. ** The argument - P1 (Decision 5). States are content-addressed; state equality is hash equality. If two representatives of one value could both be stored, equal databases would hash differently — hash equality would be a lie. Canonical forms are *mandated* by the Merkle store, not merely preferred. - P2. Given canonical forms, choosing the minimal shape as canonical is the unique choice under which numeric-tower inclusion (ℤ ⊂ ℚ) is true on the nose rather than simulated by coercion. - P3. Normalization is already one third of Sol's execution model ("proof search, constraint propagation, and normalization") — no new primitive is introduced. - C. Subtyping as proven inclusion, intensional identity, canonical quotients. ** Acknowledged costs - Operations over quotient domains accept mixed shapes and normalize at the boundary (e.g. =Plus= over =Rational= handles ground integers and canonical pairs). - A quotient domain without a declared normalization relation is rejected at admission: no equivalence without a normalizer. - The subtype lattice for base domains must be seeded in the catalog bootstrap (Decision 11's metacircular fixed point grows slightly). * Decision 13: OCaml for the Implementation, Rocq for the Proofs ** The decision The Sol compiler and VM are written in OCaml. The verified checkers of Decision 10 are written in Rocq and extracted to OCaml. Other languages were considered and rejected for the kernel line; the exploration appetite is spent above it: Rocq itself, Karuta on the BEAM, and wire clients in any language. ** The argument - P1 (Decision 4). Sol is a library that RNT links in-process, and RNT and Sakura are OCaml. A foreign runtime inside the kernel process reintroduces FFI seams exactly where atomicity and shared representation of content-addressed values matter most. - P2 (Decision 10). The extraction pipeline is load-bearing: "the thing proven is the thing running." Rocq's mature extraction target is OCaml; Scheme extraction is unmaintained, and no extraction to Common Lisp exists. - P3. The performance and correctness profile wanted here (native compilation, memory safety, strong static types) is OCaml's exact niche, and it is the lingua franca of compiler construction. - C. OCaml for compiler and VM; Rocq with extraction for the verified core. * Decision 14: No Application in Term Position ** The decision A block =[Relation ...]= is a proposition, never a term. Nested application as a value, as in =[Equal left: [Plus left: X right: 0] right: X]=, is rejected from the language. Statements about the results of relations are written flat, as membership: #+BEGIN_SRC sol [Plus left: X right: 0 result: X] #+END_SRC ** The argument - P1 (delimiter law). Each delimiter has exactly one role. An application that is a proposition in one position and a value in another reintroduces the position-dependent meaning the delimiter law exists to forbid. - P2 (relations are not functions). Elaborating an application into a term requires knowing which attribute is "the" result, but a relation is a set of labeled tuples with no distinguished output; label symmetry and mode freedom are core doctrine. The sugar would smuggle function orientation into the semantics, and it is only coherent at modes where the relation happens to be single valued: a partial, mode-dependent elaboration hidden behind innocent syntax. - P3 (the motivation dissolves). The nested form is a functional accent, not expressive power: =Equal(Plus(X, 0), X)= is exactly =Plus(X, 0, X)=, which is shorter and states the law as membership, which is what Sol says everything is. - C. Applications are propositions, everywhere. ** The one honest future door If ergonomic pressure ever genuinely demands nested applications, they are admissible only as sugar over relations whose catalog schema *declares* a principal result attribute and a single valuedness capability at the relevant mode, with a published elaboration (fresh variable plus flat conjunct). The privilege must be explicit and queryable, never assumed from position. Until a real program hurts without it, it is not built. * Consequences for the Pending Documents - =docs/core-design-and-pipeline.org= must treat transition relations as first-class in normalization, planning, and totality checking. - =docs/virtual-machine-specification.org= must specify: the state value representation (content-addressed), the evaluation of transition relations, and the single commit primitive as the only effectful operation in the VM. - Sol's DRL fragment must normalize to plans executable by RNT's FOL core (the =Plan.t= algebra: Scan, Project, Join, Union, Rename, Take, Materialize), with Sakura-style cardinality annotation.