invariants

Making impossible states impossible

I used to treat assertions as debugging tools. Something you sprinkle in while hunting a bug, then take out before shipping. That was backwards.

An assertion is a contract. When code reaches a state it should never reach, panicking beats carrying on and being quietly wrong. Most of the bugs I could never reproduce in development turned out to be bugs an assertion would have caught the first time they happened. This is the point that an analysis of assertions makes better than I can: they catch correctness violations that types cannot. Combined with CI, your assumptions stop being assumptions.

The three I use:

• precondition: what must be true just before a block of code runs
• postcondition: what must be true just after it runs
• invariant: what does not change across a set of transformations

Preconditions

Here is a payment processor I can only enable when it is disabled, and disable when it is enabled:

@dataclass
class StateManager:
    state: bool = False
    
    def enable(self) -> None:
        assert self.state == False, "Cannot enable: state must be False"
        self.state = True
    
    def disable(self) -> None:
        assert self.state == True, "Cannot disable: state must be True"
        self.state = False

Four lines and my tree of states collapsed to the valid ones. Coverage went up because there were fewer combinations left to cover. I could fuzz and simulate without generating garbage inputs. Race conditions surfaced at the assertion instead of three deploys later.

Why assertions over types

Types catch some errors at some cost. Assertions catch the impossible, and for me they work like rails: they keep me on the track rather than describing the track.

I use types for business rules and assertions for correctness. The broader version of the same instinct is in error handling: make the bad state unreachable rather than catching it afterwards.

Assertions work in every language I have used. Type systems do not. I want both.

Invariants

Invariants hold throughout execution, which is why I reach for them in algorithms and data structures, especially against system constraints:

• static allocation: no malloc, everything pre-allocated
• algorithm bounds: all values positive, checked each iteration, so overflow cannot hide
• logical implications: if-then relationships that must hold

Postconditions

Preconditions are half a contract. The half I kept forgetting is what you promise on the way out:

processed := process(numbers)
assert len(processed) > 0 # postcondition

def process(numbers):
  assert len(numbers) > 0 # precondition

TigerBeetle calls this it takes two to contract. Both halves catch bugs the other one misses, and looking at real bugs most of them need a specific set of conditions before they appear at all.

Postconditions and invariants took me much longer than preconditions. They ask you to understand the domain, the algorithm and the constraints. That is also why I think they are worth the trouble: concurrency, race conditions and distributed systems do not care how well I meant.