> However, this is impossible as per Rice's theorem. You moved a _little_ too quickly. There exist program-pairs which can be proven equal, and those for whom

> However, this is impossible as per Rice's theorem. You moved a _little_ too quickly. There exist program-pairs which can be proven equal, and those for whom no proof exists. You can organize the production of new programs into finite steps and organize the act of creating a proof-of-equivalence between the input and output into finite steps, then execute one step of creating a new program candidate followed by one step of finding the equivalence proof for each of the (finite number of) candidate programs created so far. In this way you are guaranteed to find an output program and its equivalence proof whenever such an (input-program, output-program, equivalence-proof) tuple exists. Finding the equivalence proof is recursive enumeration—the same as creating the program candidates—but in some machine verifiable proofing language. Speeding this up by leaving out syntactically incorrect programs and equivalent programs, as well as defining the proofing language and implementing the checker are left as an exercise to the reader.