Predicate Logic For Programmers

May is finally, finally over. This was one of the roughest months both jobwise and lifewise in recent memory. But now all my deadlines are over, I'm fully vaxxed, and I finally have time to start writing again. It might take me a while to get things back on track again, but at the very least I'll be back to sending newsletters (at least) weekly.

So I've got a big project for June:

Predicate Logic For Programmers

This is something I've wanted to write for a while.

People often ask me what's the best math to learn for formal methods, and my answer is always "predicate logic", aka FOL.¹ It's super useful to specifying properties, understanding requirements, and just modeling things in general. Then they ask me how to learn FOL and I falter. I could find three classes of resources on learning logic:

• Philosophy: mostly concerned with the nature of argument and reasoning, completely different focus.
• Mathematics: mostly about logic as a research topic.
• Programming: all about logic programming. Don't get me wrong, logic programming is cool, but most of us don't do it.

None of them focus on using logic as a tool for other stuff. As far as I can tell everybody picks it up through osmosis.

The best analogy I can think of for practical logic is arithmetic: just as arithmetic is the basics of manipulating numbers, logic is the basics of manipulating boolean expressions. Most programmers are familiar with the basic kind, propositional logic, via conditionals. If I see if(!(cond1 && !cond2)), logic tells me I can rewrite that as if(cond2 || !cond1).² FOL adds in boolean functions (predicates) and ways of manipulating "quantities" of expressions, where we say whether something is true of all values or some values. "All dogs are cute" and "at least one day of the year is sunny" and stuff like that. There's many other branches of mathematical logic, but FOL by itself is perhaps the most widely useful.

Most mathematicians know the basics of predicate logic, even if they don't formally study logic. This is because FOL is a useful tool. It's a great way to formalize English statements in a rigorous, manipulable way. Take JavaScript's Array.indexOf(x), which returns -1 if the element isn't in the array. Here's how I'd formalize the properties of the method using predicates:

// (a <=< b) =  {x: Int | a <= x < b}
let l.indexOf(x) = o

o = -1  => all i: 0 <=< len(l) | l[i] != x
o != -1 => 
     0 <= o < len(l) 
  && l[o] = x

If we're property testing, we can translate this to a directly to a programming predicate and test the total specification of our function. If we're writing example tests, we can use this to guide the examples we write. And if we're implementing, we can use this to eliminate ambiguity: have we captured our understanding in a precise way, or are we missing something?

Like, for example, if our spec allows multiple different implementations that don't do what we actually want. Like "return a valid index of x, but pick it at random". The intended behavior for indexOf is that you return the first element:

o != -1 => all i: 0 <=< o | l[o] != x

Being able to eliminate ambiguity is really helpful when working on high-level requirements. If I have the requirement "Show the tour to any user who doesn't have at least one of these credentials", there are at least two ways of formalizing that:

// doesn't {have at least one}
all u: User | 
  !(some c: Cred | u.has(c)) => ShowTour(p)
//------------1-------------

// doesn't have {at least one}
all u: User | 
  (some c: Cred | !u.has(c)) => ShowTour(p)
//------------2-------------

There are plenty of cases where (2) is true but not (1)… and a case where (1) is true but not (2)! Writing it down as a predicate makes the ambiguity really obvious, and then you can go to the client and ask which one they actually want.

Knowing logic is very useful for understanding the properties of functions, systems, and requirements, which is why I think every programmer should learn it, which is why I'm disappointed there are no pragmatic introductions, which is why I decided to write one. Go figure.

Book Plans

I want the book to be as easy and as immediately useful as possible. With that in mind it's gonna be less a book and more a pamphlet — I'm estimating rn that it will be under 50 pages. First ten pages on introducing the notation and properties, the rest on applications, techniques, and examples. I also plan on including exercises with solutions, too. I found a sphinx plugin that allows for cross-referencing problems and solutions. Man I love Sphinx.

I'm focusing on the ideas of using and manipulating logical expressions, not how its presented. While mathematicians write ∀ to mean "for all", most programmers won't recognize that or be able to grep it. So I'm writing all x instead. Similarly && instead of ⋀, ! instead of ¬, etc. Haven't settled on all of the syntax yet. As you can tell from the <=< thingy, I also really like messing around with different ways of presenting information. Like another possible way to present the indexOf properties could be

if o = -1 then all i: 0 <=< len(l) | l[i] != x
else 
 1. 0 <= o < len(l) 
 2. l[o] = x
 3. all i: 0 <=< o | l[o] != x

Numbered lists of conditions!

Between "covering a topic new to most programmers" and "keeping things as tightly written as possible" and "messing around with different presentations and layouts", this is going to take some iteration. So I expect to make the book purchasable early-access as soon as I have something worth presenting, which should be the end of June.³ This is probably not going to take up all my time: there's a bunch of work I want to do for the TLA+ community, and I really want to start writing essays for the blog again. But I'll let you know as soon as I have something interesting to present. I think you'll enjoy it!

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.