Do Two Programs Do the Same Thing?

Every programmer knows the small anxiety of a refactor: you rewrite a function to be cleaner or faster, and you believe it does the same thing — but does it, on every input? That question — do two programs always produce identical outputs? — is program equivalence.

The obvious check is to test: run both on a bunch of inputs and compare. If they ever disagree, they're not equivalent. But if they always agree on your tests... you've proven nothing. There are infinitely many possible inputs, and a difference might hide at exactly the one you didn't try — the value 42, or every input above a million.

And here's the deep result: there is no general procedure that can decide, for arbitrary programs, whether they're equivalent. The problem is undecidable — a direct relative of the halting problem. Not slow: impossible.

Try it. Pick a pair of small programs that look like they might do the same thing. Type an input and compare their outputs, or let the demo auto-test a range. Hunt for a value where they disagree.

<p class="hint">{{hint}}</p>
<select id="pair" class="pair"></select>
<div class="progs">
  <pre class="prog" id="pa"></pre>
  <pre class="prog" id="pb"></pre>
</div>
<div class="row">
  <label>{{label_x}} <input id="x" type="number" value="3" /></label>
  <button id="test" type="button">{{btn_test}}</button>
  <button id="auto" type="button">{{btn_auto}}</button>
</div>
<div id="out" class="out"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .8rem; line-height: 1.45; }
.pair { font: 600 14px system-ui; padding: .4rem .6rem; border: 1px solid #bbb; border-radius: 8px; margin-bottom: .7rem; width: 100%; max-width: 340px; }
.progs { display: grid; grid-template-columns: 1fr 1fr; gap: .6rem; margin-bottom: .8rem; }
.prog { background: #1d2733; color: #e6edf3; border-radius: 8px; padding: .7rem .8rem; font: 600 12.5px ui-monospace, monospace; white-space: pre-wrap; margin: 0; line-height: 1.5; min-height: 84px; }
.row { display: flex; gap: .5rem; align-items: center; flex-wrap: wrap; margin-bottom: .7rem; }
label { font: 600 14px system-ui; color: #1d3557; }
input { font: 700 15px ui-monospace, monospace; width: 6rem; padding: .35rem .5rem; border: 1px solid #bbb; border-radius: 7px; }
button { font: 600 13px system-ui, sans-serif; padding: .5rem .9rem; border: 1px solid #457b9d; background: #457b9d; color: #fff; border-radius: 8px; cursor: pointer; }
.out { font: 600 14px system-ui; line-height: 1.6; min-height: 2.4em; }
.out .ok { color: #0a7d33; } .out .bad { color: #c0392b; font-weight: 800; }
.out code { font-family: ui-monospace, monospace; background: #eef1f4; padding: .05rem .3rem; border-radius: 4px; }

// Code not found

Some pairs really are equivalent; others hide a difference at one sneaky input. When your tests all match, notice the trap: it feels like proof, but it isn't. You'd have to test every input to be sure — and for real programs, that's infinitely many. That gap is the whole point.

Equivalence is undecidable, and the reason is elegant:

• Testing can only disprove. A mismatch shows non-equivalence, but no finite set of passing tests proves equivalence over infinitely many inputs.
• It reduces from halting. If you could decide equivalence, you could decide halting: compare a program against one that trivially halts, and equivalence would tell you whether the first halts. Since halting is undecidable, so is equivalence.
• Rice's theorem seals it. Essentially any non-trivial question about a program's behavior (not its text) is undecidable — and "does it behave like this other program?" is exactly that kind of question.
• Restrict to win. On finite-state or loop-free programs, equivalence becomes decidable — that's why hardware circuits can be checked exactly. The undecidability comes from unbounded loops and memory.
• Practice approximates. Bounded equivalence checking verifies agreement up to some input size or loop depth; SMT solvers and formal methods prove equivalence for specific, well-structured cases (and compilers use this to validate optimizations).

So program equivalence is the verification engineer's version of the halting wall: provably no universal tool, only partial methods that work within limits.

The question "do these behave the same?" is everywhere in software and hardware:

• Compilers: every optimization must preserve behavior — equivalence checking validates that the optimized code matches the original.
• Refactoring tools: automated rewrites that promise to keep behavior identical.
• Hardware verification: checking a chip design matches its specification — decidable for finite circuits, and a billion-dollar industry.
• Formal verification: proving safety-critical software (avionics, medical) meets its spec.
• Security: confirming a patch fixes a bug without changing intended behavior.

Because the general problem is undecidable, all of these live on restricted languages, bounded checks and clever solvers — getting certainty where it's possible and high confidence where it isn't.

Program equivalence is the halting problem wearing a programmer's everyday worry. Each test you run can only ever catch a difference, never certify sameness — and the one input that would expose a bug may be the one you never thought to try. In full generality, no tool can settle it, because the question is fundamentally undecidable.

But the story isn't bleak. Restrict the programs — no unbounded loops, finite state — and equivalence becomes decidable, which is why your CPU's design was verified down to the gate. The lesson echoes the rest of this site: when a problem is provably impossible in general, progress comes from drawing a smaller, well-chosen box where the impossible becomes routine.