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...