It's usually called equational reasoning or Bird–Meertens formalism.
Transforming an insertion sort into merge sort is covered in Section 5 of "FUNCTIONAL PEARLS The Third Homomorphism Theorem":
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45....
In this book, many well-known algorithms, e.g. KMP pattern matching, are derived from naive implementations by step-by-step applications of algebraic rules of (functional) programs.
For example, can a program decide, given a sorting function implemented in language X, and an algorithm Y, whether or not the sorting function is an implementation of algorithm Y? Part of the question is how to represent algorithms (is "formal" pseudo-code the best way?)
Also, can you decide whether or not two functions written in different programming languages are implementations of the same algorithm?
Assuming the usual things (e.g. that an algorithm Y can be specified in some useful, say, very high level language) then this problem is Halting-hard (e.g. at least as hard as the halting problem), because it would be showing the equivalence of two programs. A similar case applies to your latter question.
I'm not sure there's a good way of specifying abstract algorithms without running into this problem, but I'd be interested in defining a bit further what you might be thinking about.
I should have been clearer, but I'm mostly interested in structure (traversal) algorithms, most of which could be coded in a language with bounded loops.
An easier question is the one of determining the complexity of an algorithm. I think there's a ton of work in this area, for example in techniques that use typing systems (types may for example specify how many times a parameter is used, thus allowing the program to infer the complexity).
(easier because the equivalence relation of "implementing the same algorithm" is strictly finer than "having the same complexity")
Bubble sort and Quicksort only resemble each other in so much as the result is sorted. All of the other steps are completely different, meaning the abstract shapes of the intermediate computations are very different.
Take an ugly equation like: x^2 + 3x+y+2+(−x)^2 = 3+(−x)^2 . It can be transformed to either (x+1)(x+2)-3 = y or y=−x^2−3x+1 fairly cleanly and usefully with just a few algebraic theorems. I remove redundancy among other things.
Can I take "bubble sort" work my way in steps to produce a "quick sort" or a "merge sort"? Sure you could prove they produce identical results but it doesn't feel like you're bridging that gap. Maybe this is too vague a question.