Map of Content

overview

Every note of the Sophia vault, in reading order. How the vault is organised: Start Here. The mathematics behind the design is in the CT-ML wiki, Track F; links to it below are ordinary web links.

0. The idea

• The Original Idea — the project as it was first written down: one graph database for code in every language and all its IRs, equivalence proofs instead of an FFI, hashes instead of names
• Design Overview — what that becomes once made precise, and the three claims the project makes
• Glossary — the vocabulary, including where it departs from the original text

1. Identity: what a node is

1. Core Calculus — the one language every frontend elaborates into; definitional versus propositional equality; the Prf/Cmp split
2. Hashing and Identity — Merkle hashing of canonical forms; binders, cycles, three hashes per definition
3. Multi-AST Layering — terms, types and proofs as one syntax; source, core, MLIR and LLVM as layers connected by functors
4. Graph Schema — node and edge kinds, the EQUIV edge, three storage backends
5. Naming and Change Propagation — names as mutable labels over immutable hashes

2. Equivalence: when two nodes are the same

6. Equivalence and Witnesses — the ladder from alpha to asserted; congruence; the cross-language relation; refinement
7. Cross-Language Semantic Hazards — the concrete ways “the same” turns out to be false
8. Effects Memory and Resources — effect rows, regions and borrows; four memory models under one roof
9. Trusted Computing Base — what must be correct for any of this to mean anything
10. Tests and Documentation as Nodes — evidence that is not proof, and prose that is not code

3. Compilation: a compiler as queries

11. Compilation as Query — passes as rules, saturate then extract, incrementality for free
12. Query Cookbook — concrete queries in SQL, Cypher and Datalog
13. Content-Addressed Precompilation — the original Julia motivation, made precise

4. Plans and risks

14. Roadmap — milestones M0–M7, and why M3 is where the project justifies itself
15. Open Problems and Risks — what may sink it
16. Repository Layout — where code and notes live; Code Map — the per-file design notes

5. State of the art

State of the Art is the index. By topic: content-addressed code · e-graphs · incremental computation · graph databases for code · code indexing · IR formats · graph IRs · equivalence checking · verified compilation · superoptimisation · interoperability · semantics of real languages · semantics frameworks · dependent types · Julia compilation

6. Background cards

Background Concepts is the index: LLVM and MLIR, Unison, hashing, rewriting, operational semantics and effect systems, type theory, Julia internals, databases.

7. Theory: where each design note’s mathematics lives

design note	CT-ML wiki
Core Calculus	Category with Families · Curry–Howard–Lambek · Call-by-Push-Value
Hashing and Identity	Abstract Syntax with Binding · Polynomial Functor · Bisimulation
Multi-AST Layering	Polynomial Functor · Institution · Natural Transformation
Graph Schema	Attributed C-Set · Algebraic Database
Equivalence and Witnesses	Congruence · Contextual Equivalence · Logical Relations · Cartesian Bicategory
Effects Memory and Resources	Algebraic Effects and Handlers · Freyd Category · Linear-Non-Linear Adjunction
Compilation as Query	E-Graph · Least Fixed Point · Change Action · Double-Pushout Rewriting
Query Cookbook	Conjunctive Query · Provenance Semiring · Monad Comprehension
Trusted Computing Base	Compiler Correctness · Provenance Semiring
Naming and Change Propagation	Relational Lens