A program transformation is semantics preserving when the transformed program has the same observable behavior as the original under the chosen language semantics.

If transformation $T$ maps program $p$ to $T(p)$, a correctness statement can be expressed as

$$p\approx T(p),$$

where $\approx$ is an appropriate observational equivalence.

For a pure expression, replacing

$$x+0$$

with $x$ is valid when evaluation of $x$ has the same behavior in both contexts. In a language with effects, transformations must also preserve evaluation order and the number of evaluations. Replacing

f() + f()

by

2 * f()

is not generally valid if f() performs I/O or mutation.

Compiler correctness scales this idea across translation stages. A pass may transform source syntax into an intermediate representation or one IR into another, while a proof or validation argument establishes that every relevant source behavior is preserved by the target.

The exact relation need not always be literal equality: an optimized program may use different internal states or timing while preserving the externally defined observations.

Semantic equivalence therefore provides the specification against which optimizations, refactorings and compiler passes can be judged, separating “the transformed code seems plausible” from a precise notion of correctness.