Why don't people use formal methods? (2019)

Original Article ↗ Hacker News Discussion ↗

Formal methods for proving software correctness remain rare in everyday development, largely because they are hard to learn, expensive to apply, and often seen as unnecessary for low‑stakes applications like CRUD apps or social platforms. Commenters highlight that rigorous techniques are mostly adopted where failures are extremely costly (e.g., hardware design, databases, finance, critical systems), and that lightweight forms such as type systems, linters, and partial verification are the most practical compromise. Several argue that AI tools and better tooling could lower the barrier to entry, but stress that formal proofs still shift the problem to writing accurate specifications, which can be as complex and error-prone as the code itself.

Perceived Value and Business Context

  • Many argue formal methods rarely justify their cost: most software is low‑stakes CRUD, prototypes, or changing business apps where quick iteration beats rigorous proofs.
  • Higher ROI is seen for infrastructure and safety‑critical domains (databases, filesystems, hardware, finance, cryptography, avionics, medical, DeFi), but even there adoption is uneven.
  • Some see underuse as a symptom of poor risk management and “move fast” culture; others frame it more simply as rational ROI optimization.

Difficulty, Education, and Culture

  • A recurring theme: formal methods are hard to learn, intellectually taxing, and poorly explained; many engineers are intimidated or uninterested.
  • There’s confusion over which method to use; people want a “second‑best for everything” rather than a zoo of techniques.
  • Formal methods advocates report resistance inside companies and often “sneak” them into their workflow.

Specs vs Code and Limits

  • Multiple comments stress that specs can be as complex as code; bugs can just move from implementation to specification.
  • Sorting is used to illustrate how subtle a “complete” spec is (must capture ordering, length, permutation, duplicates, ties).
  • Formal methods are seen as a complement to testing, not a replacement; both ultimately rely on human understanding of requirements.

Types, Partial Verification, and Pragmatic Techniques

  • Many note that type systems, linters, and related analyses are already widely used “lightweight formal methods.”
  • There is debate over where “type checking” ends and “formal verification” begins, with some insisting refinement‑style constraints as a minimum.
  • Partial verification (e.g., proving key properties or small pure components) is presented as practical, especially for libraries, codecs, and concurrency algorithms.

Tooling, Examples, and Case Studies

  • Tooling is seen as fragmented and hard to approach; people ask for beginner‑friendly, open‑source, go‑to solutions and non‑toy examples (e.g., text editor, todo app).
  • Hardware and some large software shops reportedly use heavier formal tools; one practitioner rewriting a database engine in Rust used model checking to prove equivalence of 1000+ functions and uncovered subtle upstream bugs.
  • Some large cloud providers reportedly use formal models for design and telemetry validation, but details and extent are contested.

LLMs and Future Directions

  • Several speculate that LLMs could change the equation by:
    • Mass‑generating candidate proofs or specs, which are cheaper to verify than to produce.
    • Making it feasible for non‑experts to experiment with tools like TLA+, Lean, and others.
  • Others warn that feeding formally precise specs into a black‑box model reintroduces another layer that itself must be trusted or checked.