Impossible to write

Think of it when a mistake could be caught by the shape of the data, such as two ids that are easy to swap or a case nobody handled.

In everyday life

Like a diesel pump nozzle that is too wide for a petrol car’s tank. The wrong match is stopped by its shape, before anyone has to remember which pump is which.

One case

A bank app refunds wrong fees with move(from, to, amount): from the bank’s fee account to the customer’s account. Both ids are plain text. A developer swaps the two in one place, and every test still passes. Over 300 refunds, the bank takes the money from the customer instead of paying it back: a $50 refund costs the customer $50.

Every refund moved the money the wrong way
The case, cell by cell1 cell = 1 refund
Customer balance, intended
+50+20+35+80+15+60
Customer balance, actual
-50-20-35-80-15-60
Refunds paid the wrong way
300
Tests that failed
0
With one type for the bank’s accounts and another for customers’ accounts, the swap is an error before the code runs.

Every case

A test checks only the cases someone thought to write. A type checkerA program that reads the code, without running it, and reports any value used as the wrong kind. checks every line on every run, usually in seconds. Give each kind of value its own type, and whole classes of mistakes cannot be written: a customer’s account where the bank’s own account belongs, a payment that is both settled and cancelled, a status nobody handled. The editor marks the mistake while you type, which is the cheapest moment to find it. An agent gets the same red mark and can fix it before anyone reads the code.

The word

Engineers call this

typesLabels in the code that say what kind of value each thing is, such as a number, a date or an account id. A checker reads them and refuses wrong code before it runs.

Shape the types so the wrong code cannot be written. Turn a mistake you found once into an error the checker finds every time.

Where this idea leads

Skills that encode it

  • principle-type-system-discipline pstackBrand semantic primitives: two arguments with the same primitive type but different meanings each get their own type.
  • correct pstackFix a repeated mistake with types, so the bad state cannot be written, before you reach for docs or rules.