Formal Methods: Just Good Engineering Practice? (2024)
Formal methods—mathematical techniques for specifying and verifying software behavior—are praised here as powerful tools for catching subtle bugs, especially in concurrent, distributed, or safety‑critical systems. Many engineers, however, argue that their cost, required expertise, and dependence on stable, well‑understood requirements make them impractical for most fast‑moving, product‑driven work, where tests, strong type systems, and static analysis often suffice. Several contributors advocate “lightweight” approaches such as TLA+, Alloy, property‑based testing, and richer type systems as a pragmatic middle ground, emphasizing that the real value lies in forcing clearer thinking about system invariants rather than in full formal proofs.
Meta / Prior Discussion
- Thread notes an earlier HN discussion of the same article and related AWS work.
- Reposts are generally seen as fine if prior threads are linked for context.
Where Formal Methods Fit (and Don’t)
- Widely agreed: high-value / safety- or security‑critical systems benefit most (aerospace, high‑assurance security, critical distributed infrastructure).
- Many argue most business software doesn’t justify pushing correctness from “good enough” to “near perfect”; cost and time outweigh benefits.
- Several note that formal methods require some degree of stable, formalizable requirements; “we don’t yet know what we want” agile environments are a poor fit.
- Others counter that you can specify and verify only key components (e.g., state machines, allocators, deployment workflows) and evolve specs alongside code.
Costs, Benefits, and Adoption
- Strong sense that full formal verification remains expensive in expertise, time, and tooling; learning curves are steep.
- Some see lack of broad industry uptake after decades as implicit evidence the ROI is marginal outside niches.
- Others argue costs have dropped (e.g., TLA+, Alloy, model checkers) and that even partial modelling finds subtle bugs and clarifies thinking.
Types, Tests, and “Lightweight” Methods
- Static type checking is framed as a widely used, limited formal method.
- Tests are described as formal specifications of specific behaviors; property‑based testing sits between tests and model checking.
- Debate over whether property‑based testing and randomized testing count as “formal methods” or just informed testing.
- Trace checking with temporal logic and linearizability checkers are mentioned as practical, non‑exhaustive but powerful techniques.
Tools, Syntax, and Learning
- TLA+, Alloy, Lean, SPARK Ada, dependent types, Verus, Quint, FizzBee, and P are cited.
- Opinions diverge: some say tools like TLA+ can be taught in a week; others report needing 100+ hours before they’re useful beyond toy examples.
- Mathematical syntax (e.g., TLA+, Lean) is a major barrier for many engineers who “only think in code”; more code‑like notations (Quint, FizzBee) aim to reduce this.
Specs vs Code; Intrinsic vs Extrinsic
- Some argue “the code is the spec,” and external specs often end up tautological or drift from implementation.
- Others emphasize that simple, high‑level properties (invariants, universal quantifications) are much clearer than code and catch deep design errors.
- Distinction raised between extrinsic methods (separate models and proofs) and intrinsic methods (types, dependent types, inline proofs) that tie correctness more tightly to code and compilation.