HNHiroyuki Nakahatainblog.iroha1203.dev·6h ago · 23 min readThe Goddess of Plenty Smiles at the SummitEvery test passes. Every metric looks the same. Is that enough to judge whether a design change is sound? There are pairs of changes that the observations of AAT (Algebraic Architecture Theory) cannot00
HNHiroyuki Nakahatainblog.iroha1203.dev·Aug 16 · 18 min readUncharted Waters: Thirteen Rules for Not Trusting an AI's ProofsTL;DR I want to hand an AI agent a multi-day job and have it run to completion. This post collects the rules for that — thirteen of them. Never let the loop rewrite its own spec. Enumerate up front w41T
HNHiroyuki Nakahatainblog.iroha1203.dev·Aug 11 · 22 min readSemantic Geometry of ArchitectureTL;DR Does software architecture have a denotational semantics? Yes. But it differs from the classical one in three ways. Syntax is generated from observation. The meaning of a whole system does not 10
HNHiroyuki Nakahatainblog.iroha1203.dev·Aug 8 · 24 min readAtlas Theorem: How Far Can You Zoom Out?TL;DR A veteran reviewer does not read every line. They switch reading resolution to match the property they are checking. Is there a guarantee that reading coarsely misses no bugs? This article is t00
HNHiroyuki Nakahatainblog.iroha1203.dev·Aug 2 · 21 min readTaming a 40-Minute Lean CI: Three Rounds, Three Wrong SuspectsOur Lean 4 + mathlib project used to spend 41 minutes in CI on every single PR. Today, the worst case — rebuilding the heaviest files from scratch — takes 12 minutes, and an ordinary PR finishes in a 54LT
