Invariants and Abstractions

The core of computer science is the mix of invariant and abstractions.

We reason about abstractions using the invariants they provide. We build abstractions to enforce convenient invariants.

Invaraints themselves are expressed in terms of other abstractions.

A protocol is an example of an abstraction: it enables new invariants on top of a messy source.

An example puzzle: let’s say you have a biased coin. You can flip it and get a heads or tails. You’d like to use it to make a 50/50 decision. How can you use the coin to get a bit of randomness?

Here the abstraction we’re given (biased coin) doesn’t provide the invariant we want (fair 50/50), so we need to build a new abstraction (protocol) on top of the coin.

One solution to this puzzle is to always throw the coin twice, if it gives HT that’s a head. if it gives TH that s a tails. If it gives HH or TT then keep throwing.

This new abstraction has an invariant that it always gives 50/50 chance at heads and tails. It also comes with a problem where not every coin toss generates a bit. If the coin is very biased towards one side, it might take longer than desired to generate bits because it keeps giving HH.

Here’s another example: I was reading through some networking code at a job that used a socket like API: you could call socket = openSocket() and then writeData(socket, data) and finally closeSocket(socket).

This is the abstraction API. There are some invariants that should be maintained: open a socket before writing it. Close a socket once done. Don’t write to a closed socket.

Then I noticed there was a function that might call closeSocket() twice on the same socket. What are the consequences of this?

I wasn’t sure, because the generic socket abstraction I think with doesn’t have an invariant about this. It depended on the implementation of closeSocket(). So I had to slow down and read through the implementation at a lower abstraction level to confirm the API would check the socket was already closed.

Another great example I found online at https://matklad.github.io/2023/08/06/fantastic-learning-resources.html talking about the use of invariants while writing algorithms writing about invariants in algorithms:

We don’t teach algorithms so that students can code Dijkstra with their eyes closed on the job. They probably won’t have to code any fancy algorithms themselves.

We teach algorithms so that students learn to think about invariants and properties when writing code. Real-life code is usually simple enough that it mostly works if you just throw spaghetti onto the wall. But it doesn’t always work. To write correct, robust code at work, you need to think about invariants.

Algorithms are all about maintaining invariants. When you find the right invariant/abstraction to work with, the rest of the algorithm implementation can feel trivial.