This is the age old problem with proving correctness. You can (sometimes) prove that two programs have identical behaviour. One of the programs can be slightly

This is the age old problem with proving correctness. You can (sometimes) prove that two programs have identical behaviour. One of the programs can be slightly simpler in that it is only concerned with what the correct result of a given operation is, not how to get there. But this doesn't fundamentally change that the complete specification is almost as complicated as the program itself.