- Cognitive dissonance ("this can't possibly always work, can it?")
- Confronting the danger ("what might go wrong?")
- Questioning assumptions ("what am I assuming, and why do I need to assume it?")
- Codifying assumptions as invariants ("P")
- Pushing invariants through the program ("∀x. P(x)")
But the interesting part to me is really the fact that, if you have the discipline to follow it through, it's precisely that queasy feeling that something might go wrong that eventually leads you to discover the program's invariants and ultimately to get the program right.
I mentioned this to Mitch, and he added "it's that recognition of danger (#1) that keeps us honest."