Taver's comment is particularly illustrative. His invocation of Gödel's Incompleteness is particularly interesting. Gödel suggests that any fixed formal system

Taver's comment is particularly illustrative. His invocation of Gödel's Incompleteness is particularly interesting. Gödel suggests that any fixed formal system must be true for all compatible models and thus, supposing we built the formal system to capture properties of some model we care about, is going to be overly restrictive to capture what we really want. Fortunately, typed programming languages (taken as the formal proof systems they are) are extensible. Indeed, that's half of what programming is: adding new types (formally or in documentation alone) to help us capture the reasoning for why our program should work. So, programmers need not fear Gödel so much. Instead, if you embrace the type system then it will help to calculate (up to the current limitations of the logic you've designed and your willingness to wait) the consequences of the logic you've currently designed. And, should the type checker help you to determine that your current system does not capture the behavior you're interested in... Well, you just introduce a new type and your formal system grows.