Hillel Wayne's Logic for Programmers reached 1.0 in 2026 after five years and fifteen public alphas. It is a survey: one chapter of logic basics, then eleven chapters applying them, four of which hand you a tool you probably do not have.

This note is not a review. It is the tools comparison the book implies but does not tabulate, with two things the book cannot give you — what each tool costs to get running on a real machine, and a failure mode they share that only shows up once you try to automate them.

Companion to Alloy Specification Language, which goes deeper on Alloy specifically and compares it against TLA+ and Lean 4. This one is wider and shallower: nine tools, one axis.

Working repository: jwalsh/logic-for-programmers.

Wayne names it in §2.6 and returns to it in §11.4 and appendix C: the ability-guarantee tradeoff. The more a formalism can express, the less it can promise about answering. Every tool in the book sits somewhere on it, and the book's structure is a walk from one end to the other.

The left column always answers. The middle answers within a scope — Alloy's check is bounded, TLC explores a finite state space, a property test samples. The right column is the honest end: SMT can return unknown, Dafny needs invariants you supply, Prolog can diverge.

Nothing on the right is "better". Wayne's field observation is the useful one: SMT solvers get used for satisfaction problems in software engineering, while the constraint solvers get used for optimization problems in business. Which end of the axis you live on is a fact about your industry.

Measured, not estimated. Every row was installed on one macOS arm64 machine and run against both a minimal example and one of the book's own samples.

The real barrier in this book is not conceptual difficulty. It is that chapters 9 and 10 need JVM jars with no package-manager story, and chapter 6 needs a .NET toolchain. Everything else is one brew install away. A reader who bounces off the second half usually bounced off an install, not off temporal logic.

Two version traps worth stating:

• Alloy must be 6 or later. Temporal modeling landed in 2021; most Alloy material online — including the canonical book — predates it and emulates time with a signature-based encoding. §9.3 uses the modern operators.
• MiniZinc bundles Gecode and a CBC-class ILP backend, so §11.2's comparison between solver classes runs without further installs. Running the same model against both backends turns §11.4's table into an experiment.

This is the part that does not appear in the book, because it only bites when you try to put these tools behind a gate.

Three of five signal their most valuable answer through a failure channel. A harness written on the ordinary assumption — nonzero means broken — inverts the meaning of the thing it is checking.

Concretely, in a dependency gate over the book's own samples:

• set -o pipefail with tool | grep returns the tool's exit status rather than the match. Dafny correctly rejecting a bad proof and TLC correctly finding an overdraft were both scored as failures. The gate was red because the book was right.
• The book's basic_invariants.sql ends with three INSERTs whose own comments read "Will fail saying …". The constraint violations are the demonstration; a clean run would mean the invariants were not being enforced.

Alloy deserves separate mention because the inversion is inside the tool:

Same token, opposite verdicts, decided by a keyword elsewhere in the file. Any automation that greps for SAT without knowing which command produced it is guessing.

Independent of tooling. Wayne's §5.4 generalizes Liskov and Wing's behavioral subtyping into replacement, and then reuses it twice — §7.5 for database schemas, §10.5 for specification refinement. He says so outright on p. 65: there is no common term across all the cases, so subtyping, backwards compatibility, the Liskov substitution principle and refinement get one umbrella word.

The operational form is a shortcut worth having (p. 63):

newtype is compatible with oldtype if it passes all property tests written for oldtype.

That is executable as stated. Running Rectangle's property suite against candidate types decides the classic Square case, and the pattern of failures recovers the formal two-clause rule without anyone writing it down: Square passes the invariant property (every Square is a valid Rectangle — clause 2 holds) and fails both behavioral properties (clause 1 does not). A candidate with a strengthened precondition fails in the opposite direction.

It also works on things that are not types at all. An API whose listing endpoint silently stops sorting fails the same harness, and Wayne notes that this case — data schema replacement — is the one that never got a name.

• Alloy Specification Language — deeper on Alloy's relational logic and its Kodkod/SAT flow; this note places it against eight neighbours instead.
• CPRR Methodology — conjecture and refutation as tracked artifacts. The matched-pair discipline above is the same instinct: a gate is evidence only once it has been seen to fail.
• Four-boundary spec mapping — decision tables (§8) are the cheapest formal specification in the book and the only one needing no software; completeness and soundness are exactly the boundary questions.

The book is explicitly non-linear: read ch2, then jump. Four honest paths:

Chapters 2 and 10 carry 45% of the book's 56 exercises between them, which is a fair signal about where practice matters.

The one thing not to skip on a first pass through chapter 10: §10.5 is prefaced with the author saying he "won't be too sad" if you skip it, and the liveness and fairness material genuinely is optional — but Refinement is buried in there at p. 147, and it closes a thread that opened on p. 60.