[sirseal]

There's certainly limits. Compilation-time type safety can only guarantee the absence of certain errors or presence of certain behaviours. Any question that can be reduced to the halting problem is something that cannot be automatically verified. However, there's lots of interesting and useful stuff that is not reducible to this problem. Such as "is this input really an integer?" (cough cough, dynamic languages)