This episode features Hillel Wayne, a formal methods consultant and author of Logic for Programmers, discussing formal verification, the Crossover Project (comparing software engineering to traditional engineering), TLA+ and other formal methods tools, property-based testing, and AI’s impact on software engineering.
The Crossover Project: Are software engineers real engineers?
Hillel interviewed ~15-20 engineers across 6-7 traditional engineering fields (civil, electrical, chemical, mining, industrial) to compare practices with software engineering.
Core similarity: Every engineering discipline hates waterfall; the fundamental tension is between cost of mistakes and iteration speed — faster iteration means less upfront planning, higher cost means more planning.
Iteration speed varies: Civil engineering plans heavily (can’t rebuild bridges); electrical engineering iterates faster (test circuits, send to fab); mining engineering had an “agile revolution” in 1960 with the Viennese tunneling method.
Software’s advantages: Iteration is fastest (press F11 to test); behavior is perfectly consistent across environments (same code runs identically everywhere); open source and practitioner conferences are unique to software; version control is vastly more sophisticated than change management in other fields.
Traditional engineering’s advantages: Better at upfront planning (software gets away with less); better at compiling deep reference knowledge (e.g., 500-page “Snap Fit Handbook” for plastic clips — software lacks equivalents like a comprehensive guide to API versioning).
Conclusion: Hillel moved from “software isn’t engineering” to “software probably is engineering” — the practices are fundamentally similar, though LLMs may change the calculus.
Formal methods: making implicit knowledge explicit
Core idea: Take the implicit understanding of what code should do (e.g., “max returns the largest element”) and write it as an explicit, unambiguous specification (e.g., “an element in the list such that all others are ≤ it”).
Verification: Show the implementation satisfies the spec — via tests (spot checks), types (structural guarantees), or mathematical proof (all possible inputs).
Proof automation: Theorem provers and model checkers automate the mechanical transformation steps; the engineer guides the tool with lemmas until it can close the proof.
Why not everywhere? Real-world domain problems (file systems, permissions, symlinks, encoding) require massive context; writing the spec becomes a nightmare; imperative code that works 99% of the time is usually “good enough.”
Abstract modeling (Hillel’s niche): Build a simplified model of the system (databases, distributed systems), verify the model, then implement — catches design bugs before they hit code.
Trade-off: Only worth it when bugs are extremely costly and iteration is slow/expensive; otherwise, testing + iteration wins.
TLA+: temporal logic of actions (demo)
Created by Leslie Lamport (1994); models system as state machine (all states + transitions); uses brute-force model checking to explore state space and verify invariants/liveness.
Demo: Trading platform with items, owners, offers (propose/accept/reject). Invariant: “if ownership changes, it’s because the new owner accepted an offer from the old owner.”
Bug found: Alice offers stick to Bob (Bob away), then offers to Carol (Carol accepts → Carol owns it). Bob returns, accepts stale offer → stick moves Carol→Bob without Carol’s offer. Model checker found 35-step trace in 53 states.
Learning curve: Mathematical syntax (∀, ∃, □, ◇) is a barrier; newer languages (Quint, P) offer more programmer-friendly syntax.
TLA+ at Amazon Web Services
2014 paper: “Use of Formal Methods at Amazon Web Services” — engineers learned TLA+ and PlusCal, applied to DynamoDB and S3 replication logic.
Found complex bugs that could lose data; shortest error trace was 35 high-level steps (too deep for human reasoning).
Time-of-check to time-of-use (TOCTOU): Check a condition (e.g., “account has $10”), then act — but state changes in between (another withdrawal empties account). Appears everywhere.
Exactly-once delivery: Hard; most systems build at-least-once + idempotency instead.
Formal methods value: Not just theory — the tight feedback loop (model → instant counterexample → fix → recheck) gives engineers practice seeing concurrency bugs, building intuition faster than production debugging (months between discovery and verification).
Alloy: declarative modeling for static structures
MIT (Daniel Jackson); analyzes static configurations/data models (not temporal behavior).
Demo: Access control with resources, users, parent-child hierarchy. Property: “if you can read a resource, you can read its children.”
Bug found: User reads parent → can read child; but child’s grandchild not readable because “readable_by” isn’t transitive. Visualizer shows counterexample instantly.
SAT-based: Translates model to boolean satisfiability; checks in milliseconds vs. TLA+‘s overnight brute force for large state spaces.
Fix options: Make lookup transitive (may be impractical for SQL), or adjust data model — tool doesn’t prescribe fix, just verifies candidates.
Other formal methods tools
P (Microsoft/Amazon): Actor-style state machines, more accessible than TLA+.
Quint: TLA+-inspired language with programmer-friendly syntax; popular in banking/crypto.
PRISM: Probabilistic model checker — quantifies bug likelihood (e.g., “10% chance of failure”).
Event-B: Used in Paris Metro; mCRL2 (Dutch); NuSMV (NASA); Hybrid systems (robotics).
Property-based testing: the practical middle ground
Idea: Write the spec as executable properties (e.g., “max is in list ∧ ∀x ∈ list, x ≤ max”), then generate thousands of random inputs to falsify.
Demo (Hypothesis/Python): Good max passes; buggy max_first_three fails on [0,0,0,0,1] (returns 0, actual max 1); shrinks to minimal failing case automatically.
Trade-off: Less thorough than proof (random sampling, not exhaustive), but far easier to apply to real code; works with existing test infrastructure.
Hillel’s view: Property-based testing is useful for most engineers; full formal methods remain niche.
Reality (as of March 2025): AI is bad at inventing properties — generates tautologies (P ∨ ¬P) or trivial invariants; struggles with liveness (temporal) properties.
Where AI helps: Fixing syntax errors, explaining error traces (35-step → 2 paragraphs), boilerplate edits, translating precise English into spec.
Where AI fails: Fixing broken specs, generating properties from vague intent, reasoning about system evolution over time.
Successful users: Expert specifiers using AI as force multiplier (faster spec writing, not replacement).
Adoption: Growing from ~0.1% to ~0.3% of engineers — real but not mainstream.
Logic for Programmers: why formal logic matters
Core argument: Booleans are as fundamental to software as integers; logic teaches systematic manipulation of boolean expressions (just as arithmetic teaches integer manipulation).
Not taught in school: Most engineers learn logic informally; formal grounding pays off repeatedly in conditionals, assertions, specs, and reasoning about invariants.
Empirical: Hillel keeps finding new applications where logic background makes the difference.
Hardening distributed systems: where to start
First read: Engineering a Safer World (Nancy Leveson) — systems thinking, accident analysis (Therac-25, Columbia), why complex systems fail.
Then experiment: Property-based testing (Hypothesis, jqwik, fast-check) — low barrier, high payoff.
If needed: TLA+/Quint/P for protocol-level design bugs; Alloy for data model bugs.
Don’t overreach: Use heavy tools only when bug cost justifies planning investment.
Hillel’s 2025 predictions on AI’s impact (revisited)
Vibe coders won’t match experienced engineers — still true; basics needed to direct/verify AI.
LLMs significantly augment senior engineers — true; deep knowledge + tool control = huge leverage.
LLMs will cause job losses — unclear; US market recovering; hard to separate AI from post-ZIRP correction.
LLMs will create new software jobs — true; one-dev products become viable.
New jobs will be lower-paid, less prestigious — biggest fear; software’s “magic” (high pay, autonomy, travel, bargaining power) may normalize to standard white-collar work.
High-end roles remain but become rarer, more competitive, less developer-friendly — already visible (trader analogy).
Tension: AI democratizes creation (doctors building shift schedulers) — net good for society, but threatens the privileged niche software engineers occupy.
Book recommendations
Engineering a Safer World (Nancy Leveson) — systems safety, accident analysis; free online.
Data and Reality (Bill Kent, 2nd ed.) — philosophical deep dive into what data is, identity, representation; “data is our view of reality for a useful purpose.”
Debugging: The 9 Indispensable Rules (David Agans) — war stories + principles; the only book treating debugging as a discipline; $10 used.
