One of the (many) reasons people feel that proving code is unacceptable
is that every change requires a proof check. This is certainly the case.
Of course, code that implements known mathematical functions would
have far fewer changes as the specifications would not change.
But, then, every change to a code base SHOULD require a code review.
Part of that review would be to check that the change is 'sane' (e.g.