the undecidability of program equivalence

Suppose you refactor a function and want a tool to certify that the new version behaves identically to the old one on every possible input. Or you want to check that a fast optimized routine computes exactly the same thing as the slow reference. Program equivalence is the question 'do these two machines recognize the same language (compute the same input-output behaviour)?' The bad news: this is undecidable. No algorithm can decide, for all pairs of programs, whether they are behaviourally equivalent.

The formal language is EQ_TM = { (M1, M2) : M1 and M2 recognize the same language }, and a quick reduction shows it is undecidable. Suppose you had a decider for equivalence. Take any machine M and any input w. Build M1 that ignores its input and simulates M on w, accepting if M accepts; and build M2 that simply rejects everything (its language is empty). Then M1 and M2 are equivalent exactly when M does NOT accept w. So an equivalence decider would decide co-A_TM, which is not even recognizable — a contradiction. Equivalence is undecidable, and in fact unrecognizable.

This bites hard in real engineering. There is no perfectly general, always-correct way to confirm that two programs are interchangeable, that a compiler optimization preserved meaning, or that your rewrite introduced no behavioural change. As ever, the practical world copes by restricting the problem: equivalence IS decidable for simpler models like deterministic finite automata, and is approached for real code by testing, by equivalence checking on bounded inputs, or by translation validation that re-checks each compilation. But the universal 'are these two arbitrary programs the same?' button cannot exist.