The Case Against Formal Verification, 50 Years Later
Fifty years after a seminal paper argued against formal verification, this article revisits its claims in light of modern software development, especially with the rise of AI coding. It dissects the original arguments and offers counterpoints, largely concluding that the field's utility has been underestimated, particularly now. The Hacker News community engages in a historical and practical debate, weighing the past challenges of formal methods against their growing relevance for complex systems.
The Lowdown
Formal verification, once considered niche or impractical, is experiencing a resurgence, largely driven by the complexities introduced by AI coding agents. This piece re-examines a 1979 paper, "Social Processes and Proofs of Theorems and Programs," which made a "case against formal verification," to see if its arguments still hold true today.
The article systematically addresses each of the 1979 paper's core arguments:
- Programming vs. Mathematics: The original paper argued that program proofs shouldn't mimic mathematical proofs, which are part of a social process. The author largely agrees but notes this critique targets a specific motivation, not the fundamentals.
- Specification Problems: The 1979 paper highlighted the difficulty of translating informal requirements into formal specifications and maintaining specification independence. The author counters that modern specification languages and interactive tools make mistakes easier to spot, and AI agents necessitate human oversight of specifications.
- Automatic Verification Limitations: The original paper claimed fully automatic verifiers were out of reach. The author points to significant progress, especially with LLM-powered tools, which are rapidly closing this gap.
- Detrimental Effects of Automatic Verification: The 1979 paper suggested verifiers would reduce understanding and disincentivize other defense layers. The author dismisses this as based on pessimistic assumptions.
- Messy Real-World Systems: The paper asserted that real-world systems are too complex to specify formally. While acknowledging not all systems need full verification, the author notes that increasing stakes in critical software and the need to precisely define intent for AI agents push for more specification.
- Reliability Beyond Verification: The 1979 paper stressed that software reliability encompasses more than just verification. The author fully agrees, emphasizing that formal verification is one valuable tool among many for achieving overall correctness.
The author concludes that while the 1979 paper rightly pointed out that formal verification is not a panacea, its focus on 'full verification' led it to wrongly dismiss the broader utility of formal methods. With AI agents writing code, the need for precise specification and verification becomes even more critical, aiding both human understanding and the agents' ability to close the correctness loop.
The Gossip
Decades of Debugging: Formal Verification's Journey
Commenters with historical context reflected on the evolution of formal verification, noting its slow adoption due to perceived complexity and cumbersome notation. They discussed early attempts with SAT solvers and AI provers, constrained by limited computing power. The consensus is that modern advancements, particularly in AI and increased computational capability, are making formal verification more practical and necessary, especially for validating AI-generated code.
The Specification Scrutiny
A core debate revolved around the inherent challenges of creating accurate and independent formal specifications. While some commenters echoed the original paper's concern that specifications are often the 'weakest link' and can be unattractive, others argued that verifying the implementation inherently reduces the overall attack surface. They also pointed out that modern tools, interactive environments, and developing the skill of specification writing can significantly improve their quality, although specifying GUIs remains particularly daunting.
Untangling the Real-World Complexity Knot
The discussion intensely debated whether large, 'messy' real-world systems, like Facebook, can truly be formally verified. Skeptics questioned what such systems 'compute' and argued that their shortest description is often the code itself. Proponents countered that verification doesn't have to be 'all or nothing'; critical subsystems, specific properties (e.g., permissions, data consistency), or smaller, crucial components can be formally verified. This targeted application can yield significant value, prevent outages, and help ensure regulatory compliance.