Hmm. An interesting observation, but is mutation really the problem here? I'm not sure it is... we are able to transform any program with mutation into an equivalent program where each variable is assigned once upon allocation. (If you don't already know what it is, this transformation is called static single assignment.)
Anyway, it's really hard (undecidable in the general case) to compare two programs and determine whether they do the same thing. Is that what you're proposing?
And even if you could compare programs like that reliably, it seems impractical to apply it to the giant body of today's source code, but maybe you have an idea for doing that?
In Haskell I frequently find myself searching libraries for functions (algorithms) based on the input and output type. The list is often short. Also there is some literature on deriving algorithms simply by specifying such types.
If we had a standard algebra for programs, written in some relative of Haskell or an EDSL thereof, then searching for algorithms that mapped between certain types could be made easier. True, the case of proving two versions equal would be undecidable sometimes, but not always. In that case it could time out.
I don't believe this would work for imperative languages because the semantics of side effects are often not available, but I could be wrong, or they could be restricted enough so that an SSA specification could do what you say. Bottom line: types would help, purity or the equivalent would help.
Until then please excuse me while I reinvent the wheel...
Anyway, it's really hard (undecidable in the general case) to compare two programs and determine whether they do the same thing. Is that what you're proposing?
And even if you could compare programs like that reliably, it seems impractical to apply it to the giant body of today's source code, but maybe you have an idea for doing that?