Calculus of Constrained Constructions — a sovereign alternative to SMT solvers and refinement type systems, built from first principles. Every term carries its constraints.
C³ unifies four systems that currently do not talk to each other.
| Capability | Liquid Haskell | Z3/CVC5 | Lean 4 | Dex | C³ |
|---|---|---|---|---|---|
| Refinement types | ✓ | ✗ | ✓ | ✗ | ✓ |
| SMT constraint solving | via Z3 | ✓ | ✗ | ✗ | built-in |
| Non-linear arithmetic (CAD) | limited | partial | ✗ | ✗ | full, from scratch |
| Automatic differentiation | ✗ | ✗ | ✗ | ✓ | ✓ |
| Quantifier elimination | ✗ | partial | ✗ | ✗ | full QE via CAD |
| Proof extraction | ✗ | ✗ | ✓ | ✗ | ✓ |
| Zero external solver deps | ✗ | N/A | ✓ | ✓ | ✓ |
| Algebraic numbers (no CAS) | ✗ | ✗ | ✗ | ✗ | ✓ Thom encoding |
Full QE over real closed fields. Virtual substitution for linear/quadratic. CAD for the general case. Every result carries a proof certificate.
// ∃x. x² + bx + c = 0 → b² - 4c ≥ 0
val result = QEEngine().eliminate(QEProblem(
quantifiers = List(Quantifier.Exists("x", 0)),
matrix = QFFormula.Atom(x2 + bx + c, Relation.Eq),
freeVars = List("b", "c"),
nTotalVars = 3
))
println(result.formula) // b² - 4c ≥ 0
// ∃x. ∀y. x ≤ y → False (no least real)
val result2 = QEEngine().eliminate(QEProblem(
quantifiers = List(Quantifier.Exists("x", 0), Quantifier.Forall("y", 1)),
matrix = QFFormula.Atom(x - y, Relation.Le),
freeVars = Nil, nTotalVars = 2
))
println(result2.formula) // False
// Extract and check proof certificate
val proof = ProofCertificateExtractor.extract(problem, result)
val check = ProofChecker.check(proof)
println(check.valid) // trueAll 15 open proof obligations are tracked in OBLIGATIONS.md. No obligation is hidden. No proof gap is silent.