HN Debrief

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

  • Programming
  • Developer Tools
  • Infrastructure
  • AI

The post argues that formal methods fail to spread for practical reasons, not because engineers are irrational. Different tools solve different problems, specifications are hard to write, proof effort often lands best on small components or designs rather than whole products, and most software does not justify the cost. That framing held up. The strongest comments pushed the same core point harder: the hard part is usually not proving code against a spec, it is writing a spec that actually captures what you mean. The classic sorting example kept resurfacing because it shows how easy it is to prove the wrong thing. "Returns a sorted list" allows an empty list. Even adding length checks still misses duplicates. You do not escape ambiguity. You relocate it into the spec.

Treat formal methods as a targeted design and risk tool, not an all-or-nothing purity test. If you own infrastructure, concurrency, or safety-critical code, start with the narrowest high-value properties and the lightest tools your team can actually sustain, often stronger typing, model checking, or specs around critical algorithms.

Discussion mood

Interested but unsentimental. People liked the article’s realism and saw formal methods as genuinely useful for infrastructure, concurrency, and safety-critical systems, but most were convinced the real blocker is specification cost, tool fragmentation, and poor fit with fast-changing product code.

Key insights

  1. 01

    Equivalence proofs found real Postgres bugs

    By checking that Rust and C implementations of Postgres functions behave identically, one commenter verified more than 1000 small functions and found four upstream bugs. The important part is not just that bugs were found. It is that the bugs came from platform-dependent C behavior like signedness, overflow, and parsing differences, which is exactly the kind of edge case that routine tests rarely cover but bounded model checking with Kani can surface quickly on small self-contained code.

    If you are rewriting mature systems code, use equivalence checking on narrow components before chasing full proofs. It is a practical way to de-risk migrations and flush out latent edge-case bugs in the incumbent implementation.

      Attribution:
    • malisper #1 #2 #3
  2. 02

    Most proof failures start in the spec

    The sorting example landed because it exposed how easy it is to prove a useless property. A function that returns an empty list satisfies "output is sorted." A function that drops duplicates can still satisfy a naive stronger condition. The right post-condition needs ordering plus multiset preservation. That shifts the story from "proofs are hard" to "requirements are more slippery than teams admit," and explains why formal methods often feel expensive even before the solver runs.

    Before introducing any proof tool, force critical functions into precise post-conditions and invariants. Even property-based testing can pay off here because it trains the team to state what must hold, not what they hope the code does.

      Attribution:
    • teiferer #1 #2
    • Jtsummers #1 #2
  3. 03

    The modeling work is often the payoff

    Several comments made the same practical point from different angles. Writing the spec is not a clerical step you hand to a specialist. The engineer designing the system learns from the act of modeling. Microsoft’s reported TLA+ experience was cited as evidence that the value shows up during design, not just in later verification. People using TLA+ with Claude said it takes longer up front but cuts rework because bad assumptions surface early.

    Use formal specs on designs that are hard to reason about, especially distributed or concurrent ones, even if you never prove the final code. Budget the work as design validation, not just verification overhead.

      Attribution:
    • kilobaud #1
    • baq #1
    • the__alchemist #1
  4. 04

    Type systems are the mainstream on-ramp

    A strong framing was that software already uses formal methods constantly, just at a level people do not label that way. Type systems are the piece of formal verification the industry made cheap enough to run on every edit. That perspective is useful because it turns the question from "should we use formal methods" into "how much more domain knowledge can we push into the checker." It also explains why stronger types, linters, and narrower analyzers get adopted while full theorem proving does not.

    Look first for invariants you can encode in the compiler or CI pipeline. Teams are far more likely to adopt stronger typing or lightweight static analysis than a separate proof workflow.

      Attribution:
    • ndriscoll #1
    • yoshuaw #1
    • sethhochberg #1
    • mrkeen #1
  5. 05

    Risk profile decides whether the cost is rational

    The best business framing was blunt. Most software does not need this level of rigor, so it does not get it. But systems that sell guarantees or can create outsized damage when wrong, databases, message queues, aircraft software, cryptography, financial infrastructure, do have a real case. The gap is often not ignorance. It is that product teams optimize for shipping and cheap recovery, while infrastructure and safety teams optimize for preventing classes of failure.

    Match proof effort to blast radius. Reserve serious formal work for code that holds money, data integrity, availability, or human safety, and avoid imposing the same bar on ordinary app features.

      Attribution:
    • another_twist #1
    • asxndu #1
    • akshayshah #1
    • SCdF #1

Against the grain

  1. 01

    Specs can be much simpler than code

    Against the dominant claim that specifications approach implementation complexity, one commenter argued that many important properties are still far easier to state than to realize. You can specify non-crashing behavior or mathematical correctness independently of implementation details, and those properties compose better than production code does. That is a useful correction because it shows why formal methods can be disproportionately effective on the right class of problem rather than merely duplicating the work in another language.

    Do not assume a spec will always be code-sized. For algorithmic kernels and safety properties, try expressing the property first. You may find the statement is short enough to make proof worthwhile.

      Attribution:
    • phafu #1
  2. 02

    Formal methods apply beyond source code

    One commenter pushed the scope wider than program proofs and argued that formal reasoning is underused in operational design. The Telstra NTP outage was offered as an example where basic Failure Mode and Effects Analysis could have exposed organizational and architectural single points of failure before they caused a large outage. That broadens the value proposition from proving modules correct to systematically managing system risk.

    If code proofs are too heavy, apply formal risk analysis to architecture and operations instead. You can still get large reliability gains by modeling failure modes, dependencies, and single points of failure.

      Attribution:
    • angry_octet #1
  3. 03

    LLMs can still help after the proof

    Some people saw feeding a TLA+ design into Claude as defeating the purpose, but the response drew a cleaner boundary. TLA+ is often about validating an algorithm at a high level, not generating deployable code with all runtime decisions attached. In that workflow, an LLM can accelerate translation into ordinary code as long as the human still audits the result, because the hardest part was pinning down the algorithmic behavior in the first place.

    Do not wait for perfect verified code generation to get value from specs. You can use formal methods to lock down the hard logic, then treat LLM-generated implementation like any other generated code that still needs review and tests.

      Attribution:
    • tombert #1 #2 #3

In plain english

bounded model checking ↩
A form of model checking that searches for counterexamples up to a chosen depth or size bound.
formal methods ↩
Mathematical techniques for specifying and checking software or system behavior more rigorously than ordinary testing.
Kani ↩
An open source model checker for Rust that can prove properties about code by exploring many possible executions.
model checking ↩
A verification technique that systematically explores possible states of a system to check whether a property always holds.
NTP ↩
Network Time Protocol, a system for synchronizing clocks across computers and networks.
post-condition ↩
A property that must be true after a function or operation finishes.
spec ↩
Short for specification, a precise description of what a program or system is supposed to do.
TLA+ ↩
Temporal Logic of Actions Plus, a language and toolset for modeling and checking the behavior of concurrent and distributed systems.

Reference links

Formal methods in practice

Postgres rewrite and bug context

Learning resources and tools