CatDB Research
Menu

Formalization

Three languages, three evidence roles

Rust implements the semantic kernel, Haskell supplies an independent executable reference, and Lean checks a selected theorem subset. Agreement between programs is computational evidence, not a theorem about the whole system.

Computational evidence

Rust

The implementation covers finite schemas, mappings, instances, conservative information-loss detection, and schema diff/apply.

Independent reference

Haskell

The reference implementation evaluates the same 43 Slice 5 fixtures with zero disagreements against Rust.

Machine-checked subset

Lean

The checked subset covers the recorded path and mapping laws. Instances, migrations, query execution, storage, and distributed behavior remain separate verification targets.

Typed path composition

f:A→B,g:B→C  ⟹  g∘f:A→Cf : A \to B,\quad g : B \to C \implies g\circ f : A \to C

Selected mapping laws

F(idA)=idF(A)F(g∘f)=F(g)∘F(f)\begin{aligned}F(\mathrm{id}_A)&=\mathrm{id}_{F(A)}\\F(g\circ f)&=F(g)\circ F(f)\end{aligned}

What the Lean result covers

The result applies to its exact statements, assumptions, and audited axiom boundary. The Rust and Haskell suites provide a separate computational check for the executable semantic model.

Read the formalization roadmap