Ethereum thread on making client hard forks prove things, while politely admitting proofs don't replace tests or judgment.

Revisits a 1979 anti-formal-verification paper in light of Lean, model checking, and LLM coding, so the old arguments get their annual ch...