Formal methods: Just good engineering practice?
Formal methods in software engineering—tools and techniques for mathematically proving software behavior—are presented as both essential for high‑risk systems and overkill for fast-moving products. Commenters weigh the economic tradeoffs, arguing that rigorous verification makes sense when failures are catastrophic or hard to externalize (e.g. aircraft, distributed infrastructure) but is hard to justify for early-stage startups or everyday CRUD apps. The conversation also highlights practical hurdles such as the “verification gap” between models and real code, limited tooling, and the need for approaches that integrate more naturally into mainstream languages and development workflows.
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.