Formal methods: Just good engineering practice?

Original Article ↗ Hacker News Discussion ↗

Engineering, economics, and risk

  • Engineering is framed as making good tradeoffs under constraints (money, time, safety, performance), not pursuing perfection.
  • Formal methods are seen as justified when failure is catastrophic or very costly (deep space probes, large-scale distributed systems, medical/nuclear/aviation-like domains).
  • For early-stage startups or short-lived prototypes, many argue the cost of formal methods is irrational compared to time‑to‑market; technical debt is treated as an economic bet.
  • Several comments stress that finance and incentives (including the ability to externalize failure costs) largely determine how much rigor is applied.

Where formal methods help (and where they don’t)

  • Widely agreed: they matter most for concurrency, distributed protocols, and tricky low-level behavior where intuition and tests often fail.
  • They’re also useful to precisely explore requirements and failure modes, and to prove or disprove algorithmic properties (deadlock freedom, message loss, protocol safety).
  • Some argue formal methods are essential to make software engineering more like traditional engineering; others counter that most non-software engineering only uses heavy formality in narrow, optimized or safety-critical slices.

Tools and approaches mentioned

  • Positive experiences reported with TLA+, Alloy, bounded model checking (CBMC, Kani, JBMC, Klee, Frama‑C), and Rust-based verifiers (Prusti).
  • Other tools referenced: SPARK, Dafny, F*, abstract state machines, P, Viper, RAISE.
  • Some use these tools to model protocols/hardware buses and then mirror the model closely in code, yielding very few logic bugs.

Verification gap and integration with code

  • A major concern: “verification gap” between a specification in a separate language (e.g., TLA+) and the production implementation (C, Rust, etc.).
  • Desired directions:
    • Proofs embedded in the language via stronger type systems, contracts, or dependent types.
    • Tooling that runs in CI, generates tests/stubs, or checks real source (not just abstract models).
  • Async, threading, and complex frameworks are often poorly supported by current tools, limiting adoption.

Testing vs proofs and cost debate

  • Long back‑and‑forth on whether exhaustive testing or high coverage can ever substitute for formal proofs; many say no, others claim exhaustive testing can be practically sufficient in some domains.
  • Formal proofs are described as powerful but expensive; estimates range from modest overhead to 5–10x more effort, and only clearly worthwhile where correctness is highly valuable.