Comment by randysalami
11 hours ago
Turning buggy software A into buggy software B, with all bells and whistles (and bugs included). This is useful for doing large-scale restructuring of codebases. You can verify you aren’t adding (or removing) bugs.
Actually, bugs might surface during such restructuring. If the statement you're proving can be greatly simplified to something reasonable, if we omit this one weird special case, that indicates a bug in the specification.