Imagining version control for APIs

    Is there a form of static analysis that transforms source code into a normalized representation, such that two semantically identical programs with different source can be proved identical?

No, there isn't. Not in the general case. Solving program equivalence would also provide a solution to the Halting problem.

One way to prove this is as follows:

Given an arbitrary function, f, we choose a number x and define a function f', which on input n returns 1 if n = x, and otherwise calls f(n).

We now statically know that f' halts on at least one input. If functional equivalence were decidable, then deciding whether f is identical to f' decides whether f (which, recall, is an arbitrary function) halts on input x. That would solve the Halting problem. Thus, functional equivalence is undecidable.

You can design normalized forms which will tell you if some classes of programs are functionally equivalent or not (and it's a darn good thing, too, or it would be impossible to do compiler optimizations), but any realizable algorithm for such must always have edge cases where it either gets the answer wrong, or has to output "I don't know".