implementation language decision: ocaml with rocq extraction

1 files changed, 26 insertions, 0 deletions

diff --git a/docs/sakura-RNT-integration.org b/docs/sakura-RNT-integration.org
index 78ad5e2..145c01e 100644
--- a/docs/sakura-RNT-integration.org
+++ b/docs/sakura-RNT-integration.org
@@ -709,6 +709,32 @@ ever defined.
 - 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.
+
 * Consequences for the Pending Documents
 
 - =docs/core-design-and-pipeline.org= must treat transition relations