[vezzy-fnord]

Mathematically perfect provided the proposition you're verifying is actually relevant and consistent with the one you're applying in the real world. Given the finicky nature and constraints of the environments that most software runs on, this could prove difficult. Moreover, the proofs must be maintained along with the software.

As for type systems, mission-critical software has generally made good practice with them (Ada, proof checkers, etc.) More so than consumer and enterprise circles. Yet a ton of catastrophic bugs have been the result of errors outside the scope of type checking, and as a counterpoint, our telephony is pretty robust with dynamically typed Erlang switches. It seems that mechanisms for building self-healing and concurrent systems are often put aside and equivocated solely with strong type systems. From what I recall, Erlang's signature feature of hot code loading actually conflicts with static typing.