If I start a build at 3:05 PM and it takes 12 minutes to complete, when will the build be finished?
To answer this question, we need to know how to manipulate numbers. The mathematics of numbers is called "arithmetic". Arithmetic shows us how to multiply two numbers, use fractions, determine which of two numbers is larger, and more.
If I have the conditional if(sensor_offline || inactive), and I know for sure that sensor_offline is true, does the value of inactive matter?
To answer this question, we need to know how to manipulate booleans. The mathematics of booleans is called "logic". Logic shows us how to simplify a boolean expression, use sets, determine if one statement is stronger than another, and more.
But there is one key difference between arithmetic and logic. We were taught arithmetic in elementary school. Few of us were formally taught logic. Most programmers pick up a little logic by osmosis, but even that rarely exposes people to anything beyond the basics. This makes logic the single most useful topic in math a programmer can learn.
That is the goal of this book. Reading this will teach you the basics of logic and how to apply it to various everyday software problems, like testing code, designing a database, working out customer requirements, and more. Over 50 exercises are provided to help readers master the material. No prior math background required!
------
The book's current status is GAMMA. All of the content is in but I am still in the process of copyediting, formatting, and proofreading. The final 1.0 release will be sometime mid 2026. If you buy the book now, you'll get all future version for free as well as input into how it develops.
New in v0.13:
- All chapters now explain what they will cover in the introduction
- First draft of chapter diagrams
- All chapters rewritten. Some of the notable changes:
- “Crash Course” chapter now foreshadows how the math ties into various techniques, subtyping, expressiveness
- “Writing Better Tests” has more conceptual coverage of partial specs, structural and metamorphic properties
- “Composing Code Correctly” teaches contracts before assertions and generalizes subtyping rules to functions
- “Proofs” has section on inductive proofs, more Dafny coverage
- “Working with Databases” now comes before “Case Analysis”, more on left joins, schema compatibility
- “Case Analysis” now “Decoding Decisions”, pretty much the same aside from reorganization
- “Data modeling” now “domain modeling”, which fits the overall thrust of the chapter better. Rewritten with this in mind
- “Designing Systems” replaces PlusCal section with more in-depth TLA+ and refinement
- “Solvers” has more on SMT solving
- “Logic Programming” covers Answer Set Programming
- Added “Coda” chapter
- Expanded “Useful Rules” appendix
- New logic theme: compatibility, a pattern across LSP, Refinement, and data modeling
- Index page reworked with more detail on book themes
- PDF: code diffs now show removals with strikethrough
- Removed content on
disj term (nothing in the book used it) - Various reader feedback and fixes
- 9 exercises removed, 17 added (+8 total)
----
Table of Contents
1. Acknowledgements
2. Part I: Introduction
1. Early access notes
2. A crash course in logic
3. Part II: Techniques
1. Refactoring code
2. Writing Better Tests (property testing)
3. Composing Code Correctly (contracts, subtyping)
4. Proving Code Correct (formal verification)
5. Working with Data (database theory)
6. Decoding Decisions (decision tables)
7. Modeling Domains (Alloy, formal specification)
8. Designing Systems (TLA+)
9. Solving Math Problems (Constraint/Integer/SMT solving)
10. Logic programming (Prolog, Datalog, ASP)
4. Part III: Appendices
1. Math notation
2. Useful rules
3. Other ideas in logic
4. Answers to Exercises