Broken proofs and broken provers

My impression is that the LCF style systems, including the HOL family as well as Isabelle, have an excellent record for soundness, confirming Robin Milner’s conception from half a century ago – and with no countervailing penalty.

It's galling to read this after a listing of kernel bugs in a multitude of LCF-style systems. Meanwhile, Metamath's kernel has been independently implemented like five times and you (yes, you the reader!) could implement a more-or-less working kernel in a week. In Metamath databases, it's possible to have buggy or incorrect axioms, or to have proofs which incorrectly substitute metasyntax, but kernel correctness has already been figured out. Indeed, we invert the responsibility somewhat: your Metamath kernel is not correct if it thinks that set.mm or iset.mm have any invalid proofs.

This is an interesting look at "bit rot" in a field (formal verification) that many outsiders assume is immune to it. Paulson’s point about proofs breaking due to changes in underlying libraries really highlights that "complexity is the enemy," even when that complexity is mathematically sound.

It makes me wonder if the formal methods community could benefit from a more "suckless" inspired approach to library design. If the goal is long-term stability, we often find in systems programming that the best way to keep a project buildable ten years later is to aggressively minimize dependencies. It seems like formal proofs are currently sitting on a very deep, moving stack that makes that kind of longevity nearly impossible right now.