Show HN: Lean4 proof that SSOT requires definition-time hooks and introspection
I formalized the Single Source of Truth (SSOT) principle in Lean 4 (~2.1k LOC, zero sorry) and proved two core results: Structural SSOT is achievable only when a language provides definition-time hooks and runtime introspection. Macros/codegen (before definition) and reflection (after definition) are insufficient. These requirements are derived, not chosen: because structural facts are fixed at definition, derivation must occur at definition time and be introspectable to verify DOF = 1. Would appreciate review, critique, or independent checking of the Lean scripts. Comments URL: https://news.ycombinator.com/item?id=46537459 Points: 7 # Comments: 4
I formalized the Single Source of Truth (SSOT) principle in Lean 4 (~2.1k LOC, zero sorry) and proved two core results:
Structural SSOT is achievable only when a language provides definition-time hooks and runtime introspection. Macros/codegen (before definition) and reflection (after definition) are insufficient. These requirements are derived, not chosen: because structural facts are fixed at definition, derivation must occur at definition time and be introspectable to verify DOF = 1.
Would appreciate review, critique, or independent checking of the Lean scripts.
Comments URL: https://news.ycombinator.com/item?id=46537459
Points: 4
# Comments: 0