Logic for Programmers by Hillel Wayne

transcript

I want to start this actual talk by introducing a couple of people. The first is Will. Everybody please say hi Will. Hi Will.

Great. Will is a very close friend of mine and he just got married last Saturday. Everybody please say congrats Will. Unfortunately he got married in Portland, Oregon which is 4,000 miles and three time zones away from Boston and that is why my body currently thinks it is 7 a.m.

Everybody please say why Will? Okay that's person one. Person two is also Will. This is William of Occam, mostly known for Occam's razor.

Do not multiply elements beyond necessity. He is somewhat less known for this claim. Now the possibility of destructive proposition is it is sufficiently that neither it's possible but for destructive proposition to be impossible it would require that both parts be impossible. A little bit less well known for a good reason.

Now this is a statement in logic which is the study of human claims and whether they are true or false. For a long time this was a topic in philosophy which is why you have really long-winded statements like this. In the past 300 years or so it has also become a study of mathematics thinking about booleans and how we can manipulate them and how we can form them to larger expressions which is why this is not aimed after him but after the person who came up with this formulation. Not A or B equals not A and not B.

Much easier to work with I think. Logic and mathematics logic have really deep connections with software engineering. This has been a fast decision of mine for a long time so in 2021 I started thinking about a book that could talk about these connections in more detail for people. In 2024 I made the first public release of an alpha of this book online and as of Monday July 27, 2026 it is now complete, in print and available on Amazon.

And for that reason I now have to make a talk about this book. But there's a lot of topics in the book it's a very very dense book and I only have 47 minutes and 38 seconds now so I decided to focus this talk on one topicPreview. When can new replace old? More specifically when can a new version of something fit into the old version without causing anything relying onEMP version to break?

As a more practical example let's imagine that we maintain an API for finding the location of devices. You pass in a location and you get back to location. Now it's impossible to always get back to the exact location of a device so instead give some sort of estimate. We say it is in some area and we guarantee that wherever we output is going to at least contain the device.

There's many ways we can change the API. For example we could refactor it in a way that changes no observable behavior. That is probably going to work with everybody. Nobody's going to be bothered by that.

But we can also make changes to the observable behavior that are safe. Like if we are more precise everyone is probably going to be happy with us. That's replacing an old version of the code with a new version with different behavior. We can also make changes that people are not going to be happy about.

We could say we're not going to give you the location of the device. We're going to give you a very narrow area that's outside the area of the device. Now the question is what about something like this? Instead of returning a circle we return this weird squiggly area.

Is this safe? This is a harder question. The reason it's a harder question is because we fundamentally don't know how people are using our API. There's some expected common use cases like they don't know where their device is or they know where their device is but they don't know where they are.

But you can also think of more exotic use cases like they might be taking two devices finding the locations and figuring out the distance between them based on their estimated locations. They could be using the device to trigger an automation when it comes to a certain area. They might be doing something more exotic. We don't know what they're doing and if we didn't know what they were doing we don't necessarily know the proportionate that they are doing.

What's the most common use case and what's the rare ones? All we really know is that they have some workflow that has an upstream, a corridor system and a downstream and if we replace the old version with a new version they have the same system with a new version. Ideally this will not break when we replace old with new. So intuitively new can replace old when any workflow that uses old doesn't break with new.

The rest of this talk is going to be formalizing this statement. To start we need a lot of math. This is the part that's probably dense to the talk so if you're tweeting pictures of cats right now now is the time to focus. So everybody has some experience with Boolean logic purely through working as a developer.

Now something like this is formalized was this. TV off or TV on and TV not working. This should be feeling everybody right. All make sense.

And yes I know you can replace TV off with TV on with a single Boolean variable but this is just demonstration so don't think you're hard about it. Now that works. That's obvious. This is a little trick here.

This is still a claim that is either true or false but it's not as obvious from purely programmer experience how to formalize it. To do so we need three concepts. Sets, predicates and quantifiers. A little bit later we'll also be talking about a fourth concept implication but that's an advanced topic.

So back to the claim. Everyone in this room is bald. Here is a logical formulation of that statement. For all P in room bald P is true.

This as a whole is a expression. This is true or false. On the right side we have a predicate bald P. For the purpose of this talk I'll just say a predicate is any function that returns a Boolean true or false value.

Room is a set. A set is a collection of unordered unique elements. Every person in this room is a set. One comma two comma three is a set.

Every integer is a set. Every integer that is a hash of a Python program written by somebody in this room is a set. Not everything can be represented with a naive set but a huge amount of interesting things can. Finally this all P in room is a quantifier.

This is saying that the right hand side of the expression bald P needs to be true for every element of the set. You can see we use P as a binding of a temporary variable like a list comprehension in most languages. So this is as a whole like the statement. Now is it true or false for this thing?

Is it true or false? Raise your hand if you think it's false. Okay. Now why is it false?

Somebody point to somebody who's at fault for making this false. A lot of arrows going in a lot of random directions. Okay. So this is not true that everybody in the room is bald.

And as you all go, show it by pointing around you can find a specific counter example to this. You can find someone in this room who is not bald. Some is another quantifier. Some are often written as a backwards E.

The all quantifiers written as an upside down A by mathematicians. And it is true if at least one element of the set satisfies the right hand side. I want to point out this connection between all and some. All X P of X is an equivalent statement to not some X not P of X.

If something is true for everything in a set, it is false that it is not true for one element of the set. We call this duality and let's just sort of transform all into sums in the same way D Morgan's law. Let's just transform and into Ours. Now this isn't true for everybody in the room.

But I can imagine we can find some sort of subset of the room where this is true. For example, maybe it's true that all everyone in this room named hill L is bald. How do you represent this statement? Well, there's a IMAGES.

The first is we canhered the set of room for people who satisfied the predicate hill L creating a new set called hill L's. Then we just have all P and hill L's bald P which is true unless somebody, anyone named hill raise your hand. No, excellent. Great.

We can also do something a little more clever. Take the sentence all P and room not hill L or bald. Either you are not named hill L or you're bald. So let's look at somebody like Marina right over there.

She's not named hill L so the left hand side is true. Therefore it doesn't matter the right hand side is false, that she's not bald, that's true for her. Then we look at Dominic. Dominic is bald and not named hill L so that's true and we're good.

Finally look at me. I'm named hill L so the left hand side is false so I have to check the right hand side. Right hand side says that it's bald. I'm bald.

Yeah, so that's true. Essentially what this does is it filters the predicate, it conditions the predicate to only check the bald predicate on people who are named hill L. This process of using not P or Q to filter on P is so common we have a special symbol for it. We say all P and room hill L P implies bald P to say that if you're named hill L then you're bald.

Only check bald on people named hill L. This is called implication and the operator is called implies. Can I get some water actually? No.

Great. Thank you. Oh, it's right under here. Wow.

Can I get a friend? Anyway, so that's actually all the operators we need. Before I continue though I want to point out some interesting relationships between them. First of all, we now essentially have three sets.

We have the set of everybody in this room, the set of people in this room who are bald and the set of people in this room who are named hill L. Bald is a subset of room. That means every element of bald is also an element of room. Hill L is a subset of balls.

Every element in hill L is also an element of balls. I can say that if we filter the set of people in the room on hill L, that is a subset of filtering the set on people who are bald. Similarly, because hill L represents everybody who passes the hill L predicate, I can say that for everybody in the room filtered on people named hill L, they're bald. Furthermore, I can say that all people in the room, if they're named hill L, they're bald.

These are all the same statement. These are all either all true or all false at the same time. This lets us convert between all of these forms, which is very, very handy for doing manipulation. Similarly, both of these are transitive.

If hill L is a subset of balls and balls is a subset of room, hill L is a subset of room. Similarly, if hill P implies bald P and bald P implies room P, then hill L P implies room P. Finally, I do want to address an edge case. What if I had a mohawk?

Well, then it would not be true that everybody in the room, hill L implies bald. It would also be true that there's at least one person who was both named hill and not bald. Can we show these are the same thing? And the answer is yes.

The manipulation rules I briefly touched on allow us to transform via duality this top thing, into the second statement. And then, using the definition of implication, we can transform the second one into this. And then, de-borgans law brings us from there to there. So these are the same statement and we can show it mathematically.

So, in short, sets, unordered unique collections, predicates, boolean functions, quantifiers, checking all in sum on predicates on sets, and implications is really weird operation that a lot of properties really like. You can go back to not paying attention now. We're done. We're past the hard part.

So, this is the math we're going to use to try to make a formalization of this. New can replace old when workflows using old don't break with new. So, what does it mean for a workflow to rely, depend on old? It means that they're using it in a correct way and whatever we're giving back, they know some things about it that are guaranteed, that are safe.

To start, what do we know about usage of it? We know that they're always passing in devices and they're always getting back location estimates, right? In other words, we've got a type system. Get location has the type, device to location, meaning everybody always calls it with devices and always gets back locations.

Now, type theory is a deep, deep topic that is way beyond the scope of this talk, but for the purpose of this talk, I'm going to highly over simplify it to sets. Device is the set of all devices or the domain of the function. Location is the set of all possible locations that could be returned. The type, device location is the set of all functions that map devices to locations.

In this context, it's pretty easy to transform the type signature into a quantifier expression. For every device in the set of devices, calling get location on that device returns a value in the set of locations. This is always true and people can always rely on this guarantee. In fact, a person can say this and say, well, get location requires that the device comes from the set of devices and I can be assured that the return value is in the set of locations.

That's how they have to use it and what they can rely on in order for those to endure correctly. We often call this requires thing, something that must be true for a function to work correctly, a precondition, which I'll write as pre underscore get location or get locks precondition or pre of get lock depending on how I'm feeling at the time saying it. This ensures is a post condition, something that is guaranteed as long as you satisfy the preconditions. Post conditions are a little bit easier to talk about formally, so let's start there.

Specifically, the post condition that the locate output is in the set of locations is a very weak post condition. I can give you a million functions that satisfy this post condition. Even something like takes a device and just returns some random location on Earth counts as a function that satisfies this post condition. We want something a bit stronger and something that possibly relates the input to the output, right?

So I'm going to say the post condition isn't just that the output is in the set of locations, but that the device actually is really in the output estimate. And this now requires us to actually be accurate in our response. Even this though is not really enough for us. And the reason why is because I can also give you a very easy function to implement that satisfies this.

You call get location on your device and you get back Earth. It's always going to be on Earth somewhere. So we're going to ask one more thing. We're going to make this more precise.

We're going to say that there is some guaranteed boundedness on how big the area is. So I'm going to say the area of location is less than one deci acre. And for you metric people out there, a deci acre is approximately two meters by one for long. So now our guarantee changes from for all the device, the output is in the set of locations to this.

For all the device, the post condition of get location is true. And this gives us all we really need to give a contract to our users. They know that I know now that I can call get location on my device and get where I am. And I can call get location on Andrew Kelly's phone and figure out where he is.

And I can call it on your ons phone and know where your on is. And I can call it with the popes phone and know where the popes is. Oh hey, he's singing out with Andrew. Didn't know they were friends.

So in the real world, people value privacy and we kind of want to help them keep privacy. So we only want to allow them to call this on a device they own. This acts as a further precondition in order to use the function correctly and get an output that guarantees their device location actually contains their device. They need to own the device they have.

So I'm going to amend the precondition to not just say that these and the set of devices, but that you own D. There's a bit of a difference though between representing the precondition and the post condition. And that is that there's no clear place to put it in the guarantee. I can't change all the device because that has to be a set and precondition is a predicate.

So we need to first think about how this can actually be fit into our guarantee. And to do that, let's go back to thinking about predicates as sets. This is the set of all devices in the universe in the domain of discourse. This is the set of all devices satisfying the precondition.

It's going to be a subset of those devices. So if this is so basically instead of saying all D and device, the post condition is true, we can say for all D in the set of devices filtered on the precondition, the post condition is true. Does that make sense to everybody? Great.

Now we can do something tricky. Remember this? Remember how implication lets us convert set filters into just straight upsets and predicates? We can do that here too.

Instead of saying all D and D and device, the precondition is true, I can say for all D and device, if the precondition is true, that implies the post condition is true. And this gives us the contract form of a specification. For all functions s to t, the specification of f, the guarantees we make and the requirements we put on it for customers is that for��s, the precondition is true, implies the post condition is true. For brevity, I'm going to sometimes in this talk simplify to this, saying pre of f implies post of f.

The types, the quantifiers are going to be implicit here. This can lead you down a dark path if you're not careful, but not in anything we're goingHong to do in this B. The precondition is that B is not equal to zero and the post condition is that the output times B gives you back the input, gives you back A. So we have two specifications that pre of old implies post of old and that pre of new implies post of new.

We have two versions of the system that our user has. The old workflow, we're upstream calls old and old passive value back used by the downstream, where old requires the old precondition and uses the old post condition and the new version, which is the exact same except we require the new precondition and ensure the new post condition. Without knowing anything else about old and new, can we find some sort of relationship that tells us if new will be a safe replacement? We can by relying on one key usually safe assumption.

And that assumption is that the old system that the customer has works, that it works correctly, that it does what they need. Because old isn't the only thing with the specification. Upstream and downstream have specs too. The upstream ensures some post condition of the upstream and the downstream requires some precondition of the downstream.

And given the assumption that our system does not break when they put it in theirs, whatever they assumed as, whatever they basically ensured as a post condition of their upstream was at least enough to ensure old preconditions, it's not passing in something that is invalid for us. Then our specification says that is true. And then whatever we ensured from the post condition is enough to satisfy downstream's preconditions. Once we establish all these things, that again means their system works, we can apply the transitivity of implication to get that the post conditions of the upstream imply the preconditions of the downstream.

Everything works, everything is fine, everything is safe. Now, what does that look like for the new version? Well, we know, given that the old version worked, that the old post condition, that the upstream's post conditions, implied our old preconditions, our new preconditions imply our new post conditions, and our old post conditions imply downstream's preconditions. So if we want to guarantee that our placement is safe, what we need to do is close the links here, get back something where the upstream implies the preconditions of the downstream.

In other words, we need to fix that top zone over there and that bottom gap over there. We need assurances that the old precondition implies the new precondition, and for the bottom, that the new post condition implies the old post condition. That's it, at least for pure functions. New can replace old when the old precondition implies the new precondition and the new post condition implies the old post condition.

Obvious, right? Just totally obvious. Just looking at the mat to get what that means. So let's also put a little bit of a informal spin on this.

Say we have pre-old implies pre-new. Then we have the set of all inputs that satisfy the old precondition. And then based on those subset of super set rules of converting between sets, we have the set of everything that the new precondition accepts. Everything is accepted by the old preconditions accepted by the new.

But there's lots of values that used to be invalid that have become valid. In other words, the new precondition is a looser assumption of the old precondition. So saying that pre-old implies pre-new is the same as saying that we can keep the same preconditions or strictly loosen them. We can make them more accepting.

And then new implies old, the post new implies post old, is that by conversely you can keep or tighten the post conditions. Or if you want to think about this in terms of post law, we can become more liberal in what we accept and more conservative in what we output. If we guarantee those two things, then we are guaranteeing that any system that relied on the old version of our code will still work with the new version of our code. Let's go through some fixed examples.

Old version is you own the device. New version is you own the device and have a premium account. Does pre-old imply premium? No.

In general, A never implies A and B. And that is why, for example, this is also wrong. Because it is you own the device and the device was made in the last year, it is again an A and B thing. So again, it will not be okay.

How about this? Not only can you see your own devices, but anybody in your family can see your old device and you can see anybody in your family's devices too. So the new precondition, pre-lated, is that you or someone in your family owns the device. Does pre-old imply pre-lated?

It does. Now, I want to be clear here, by replacement, I mean that any existing system still works. Not that everybody is happy. Because some people might not be happy that their family members can now see where they are at all times.

But again, by our logic, that's acceptable. We are not caring about morality or use a desire only about preventing breakage. On the same line, pre-ble, where you own the device or have a premium account in which case you can see anyone's device, is also okay. It is horrible, but logically it is okay.

Now on the post-condition side. If we make the area wider, does that mean that our new post condition implies their old post condition? I see people shaking their head, no it does not. One thing I often like to think about is what kind of workflow would break with a weaker post condition.

In this case, I'm imagining somebody who knows they can search the area in like 10 minutes, so they are having a robot search after they get the location back and now the robot runs out of battery before it finds the device. What if we just give, what if we make it more accurate area, but we just give the wrong area? So now the device is outside the area. Again, not okay.

What if it's still in the area, but we give a narrower, narrower like area of where it could be? That's fine. That's not going to break anybody's current workflows. Now I'm going to probably do a bit of an interesting case.

Old version has a resolution of one deci-acre. The new version has a resolution of one centi-acre and for those of you who don't know imperial, that's approximately equal to two meters by one tenth of one for long. Old version looks like this though. Oh wait, is it?

Old version looks like this though. New version looks like this. Is this a safe replacement? It is.

It is totally fine. That is because our old post condition was that it was located in the area and the area had a certain radius. The new one is that it was located in a certain area and it had a certain area. Sorry, not radius before, but like the output location had a certain size.

Again, the new post condition is that the output area has a certain size. This is fine. And yet we can sort of imagine easily a workflow that breaks. Like you have some automation that triggers the devices in range.

If you scooch the device over a bit, it activates. And here if you scooch the device over, it's still like five widths apart. So clearly some user has broken by us changing even though we've satisfied the post conditions. And this gets to something very, very important about replacement any kind of theory like this.

Not all properties are post conditions. Post conditions are only what we guarantee to our users we're going to preserve. A property though can be anything they observe is true for all inputs. So if we and generally the post conditions are a very strict subset of the observable properties.

Like we say it's going to be located in a certain area and the area is going to have a certain size. The properties are going to be that yes, those are all true, but also that the area is a circle and that it's convex, meaning that it's like a regular polygon isn't like spiker have like weird jagged edges or stuff, that it's not disjoint because it could be that we return four areas that are not connected to each other and that's fine. That still satisfies the post conditions and that the response time comes in a certain amount of time. Any of these things can be true and that could be something they rely on.

This could lead to us thinking that we replace the system and yet breaking real-world use cases. Is this something we should be worried about? Maybe, maybe not. Probably but not always.

Because when I say that any property can be something people rely on and can break their post condition and can basically break if we change our system, I mean anything. Like let's say somebody comes to us and says like hey, when you made your system more accurate, you broke our you broke my workflow. You ruined everything and we're like how? We just made it more accurate.

Now instead of it being like let's be able to one desi acre, it's now less than equal to one centi acre and they're like no. We measured that the area is always exactly one desi acre and because of that I could turn on my light bulb by throwing my phone at the light bulb and causing it to turn on and now that it's more accurate, I have to hit the light bulb dead on to turn it on. In a sense, we've just reinvented Hiram's law. With a sufficient number of users of an API, it doesn't matter what you promised in the contract, all observable behavior of a system will be dependent on by somebody.

And as it turns out, much to our horror, software engineering is as much a social project as a technical one. We guarantee certain things will always hold and as long as our users only depend on those things that we guarantee and the replacement will be safe. If they rely on anything else, all bets are off and we have to make the decision on whether we have to say you're right, that is a reasonable thing to assume. We're going to make sure that we preserve it or roll back what we did or to say that is something that we cannot guarantee is always the same and if you depend on it, you depend on at your own risk.

I actually recently saw online a person talking about how customer complaint they changed the text on their 404 page because they relied on that for one of their workflows. Anything can be dependent on. So as a last topic, I want to address a bit of a problem with this entire formulation which is that the function I gave you, get location, is fundamentally stateless. There's some state in where the device actually is but that function does not change the state of the world.

It does not change the state of the system. It does not do anything internally. And what I presented you with that pre-new implies pre-new, postal implies post-new seems to only really be designed for similarly stateless non-mutating functions. Can we extend this theory of replacement logically to cover state two?

And in here I wrote that I don't have time for this but it looks like I have actually 18 minutes left. Fortunately I cannot write the slides on the fly so I'm just going to give you a very high level argument for why I believe we can extend this logic to cover stateful functions. So in 1987, Barbara Liskov wrote the paper, sorry, future Turing award winner Barbara Liskov wrote the, and so I can test this protocol and venture into future Turing award winner Barbara Liskov invented, wrote the article, data abstraction hierarchy where she was trying to come up with a good definition of a subtype of a type. This was for OOP stuff mostly.

She wrote, if for each object O of type S, there's an object O2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when O1 is substituted for O2, then as is a subtype of T. In other words, if S is a subtype of T, then we can replace S into any system that uses T and depends on T without that system breaking. Essentially, this whole notion of replacement just for types as opposed to only pure functions. And given that a type can have a pure function as a method, this means that her work is a strict superset of the talk I just gave.

In fact, in 1994, she wrote a famous paper called a behavioral notion of subtyping where she came up with the exact rules required to guarantee that S is a subtype of T. And this entire talk, everything I cover today is basically just us talking about sub clause 2B of her rules. Exact same thing. Her rules incidentally also cover stateful types and types that have internal data and the history of types and stuff.

So if you want to try to extend this theory to cover everything, you can just read this paper and it will cover it all. And yes, that means that once again, it's yet another thing that Barbara has invented. So as a quick summary, logic useful. With a simple bit of math, we can develop quite complicated topics, taking sets, predicates, quantifiers, and implications and using it to figure out whether one bit of software can accurately replace another bit of software.

And it's to speaking of which, the actual way that works is that if we keep or loosen the preconditions and keep or tighten the post-conditions, then it is safe to replace one bit of software with another one, assuming they only rely on our stated contracts and not any observable properties we have. And finally, Barbara is the GOT, the greatest of all time. So I do think there are some interesting consequences of this. I want to leave that homework for everybody because I have the time to say this.

If you found it interesting, some ways to test your knowledge. How does this lead us to know that it is safe to change in a function signature, change the parameters going in co-contravarily, meaning we can put super types in, but we can change the output co-barantly, meaning we can return a subtype. That is also covered by this. Think about that.

Another thing to consider, why is it safe to add dictionary keys to an output but not remove dictionary keys? And why is it safe to make a required input optional but not make an optional input required? So all things we're thinking about because these all can be explained in this way, just if you want to learn more, just try to think about that. Now, if you like this, as I mentioned, this book, it all comes from this book, a lot of programmers which is now available online, both at e-book on Amazon.

Specifically, this is section chapter five, section four of this book is covering this notion of replacement. And there's 12 chapters. So a lot more goodies in there if you find this interesting. And if you didn't like this talk, blame will.

Thank you.