Types because they can be checked mechanically, simply enough that a programmer can understand the checking process and why it fails or succeeds, but are expressive enough (given some relatively cautious/widespread advances - HKT and some level of dependent typing) for every invariant I've ever needed.