@rysiek The really sad part, and an indictment of the entire discipline, is that "all software has bugs" and "all mathematical proofs are incorrect" are technically equivalent statements.
Usually inaccurate specifications of expected behaviour are considered "software bugs", because writing the specification is part of designing the software. In that model, these two statements are not equivalent.
