Formal Methods: Just Good Engineering Practice? (2024)

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.