Logic for Programmers

A book about math, software, and using one to fix the other.

Written for the working programmer. No math background required.

Buy Print Buy EbookBuy Ebook Sample ChapterSample

227 pages. Ebook includes PDF and EPUB, DRM-free.

What’s this book?

This is a book about designing, verifying, and reasoning about software better. And it’s about how learning a little bit of logic, the mathematics of Booleans, unlocks all sorts of cool techniques in our field.

If you want to get a feel for what it’s like, try reading a sample chapter!

Is this mostly theoretical or does it have practical applications, too?

Everything in the book is meant to be practical. Early chapters are on topics like “simplifying conditionals” and “ensuring an API change won’t break clients”. Later chapters are on slightly more esoteric subjects, like “finding race conditions in hypothetical software designs” and “minimizing the wall clock time of a distributed task”. Not everything will be useful to everyone, but I hope everyone finds something useful!

Do I need to know math?

Nope! You don’t need to know math besides the Boolean AND, OR, and NOT that programmers pick up through daily experience. The book covers the rest of the math you need.

That said, you do need to know some programming! This book is meant for intermediate-to-advanced programmers and I assume the reader knows universal topics like loops, version control, testing, etc. Some chapters expect more specific knowledge like SQL or API design. Chapters are independent, though, so if something doesn’t fit your needs, go ahead and skip it.

What’s with the weird A and E in the title?

Logicians use the symbols ∀ and ∃ to mean “for all” and “there exists”, respectively. For example, we could write the sentence “everybody has a favorite color” as ∀p ∈ Person: ∃c ∈ Color: IsFavoriteColor(p, c).

To make learning the topics (and searching the book) easier, I use English words instead of math symbols. So the same expression would be all p in People: (some c in Color: IsFavoriteColor(p, c)).

How can I get it?

If you want to read the book on your phone or computer, you can get it as a PDF or EPUB. Here’s the PDF:

The print version is identical except with black-and-white printing and wider page margins. You can buy it on Amazon.

What’s in the book?

Here’s a table of contents and corresponding techniques:

1. A Crash Course in Logic • predicates, booleans, sets, and quantifiers

2. Refactoring Code • rewrite rules

3. Writing Better Tests • property testing

4. Composing Code Correctly • contracts, subtyping

5. Proving Code Correct • formal verification, Dafny

6. Working with Data • database theory

7. Decoding Decisions • decision tables

8. Modeling Domains • formal specification, Alloy

9. Designing Systems • temporal logic, TLA+

10. Solving Math Problems • constraint and SMT solving

11. Logic Programming • Prolog and answer set programming

Plus some appendices on math notation, useful rewrite rules, and advanced topics in logic. All code samples are available on GitHub, along with a bunch of extra samples on the same topics that are not used in the book.

How long is the book?

It’s just about 50,000 words and a bit over 200 pages. The extra credits add another 4,000 words or so.

“Extra credits”?

There’s a lot of interesting topics that I wanted to cover but couldn’t because they weren’t useful or focused enough to be in the book. So I put them in an extra credit repository with links in the book. This covers stuff like how to calculate the size of a state space, the theory of partial orders, and a few other small things.

How come in Python all([]) == True? That always bugged me.

Python’s all function is equivalent to this:

all(l) = l[0] && l[1] && l[2] ...

This has a particular property: given any two lists xs and ys, we know:

all(xs . ys) == all(xs) && all(ys)

But that’s for any two lists, and that includes empty lists! What happens if we pick ys = []? Then xs . [] == xs, meaning:

all(xs) && all([]) == all(xs . [])
all(xs) && all([]) == all(xs)

If all([]) = True, then this equation becomes all(xs) && True == all(xs), aka all(xs) == all(xs). If all([]) = False, then this becomes all(xs) && False == all(xs), which means all(xs) == False no matter what xs is. So it makes more sense for all(xs) = True, to preserve the property.

We say that True is the identity of &&: p && True == p regardless of what p is. The same argument, incidentally, also explains why the sum of an empty list is 0 and the any of an empty list is False.

Who’s the author?

I’m a software engineer specializing in formal methods, distributed systems, and software history. Some of my past works include Practical TLA+ and The Crossover Project. I’ve done formal verification and training for clients like NASA, Meta, Giesecke+Devrient, McKinsey & Company, Siemens AG, and Western Digital. I usually bring homemade chocolate when I speak at conferences.

I also have a blog and a weekly newsletter.

Ready to read?

Buy Print Buy Ebook Sample