software

Show HN: Lean4 proof that SSOT requires definition-time hooks and introspection

Published: (January 8, 2026 at 12:15 AM EST)
1 min read
Source: Hacker News

Source: Hacker News

Overview

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 the mechanisms that enable this.
Back to Blog

Related posts

Read more »

Proving Liveness with TLA

Article URL: https://roscidus.com/blog/blog/2026/01/01/tla-liveness/ Comments URL: https://news.ycombinator.com/item?id=46471699 Points: 9 Comments: 0...

When to use getattr in Python

The basic idea Normally, you access attributes like this: python p.name That works only if you know the attribute name at coding time. getattr lets you do the...