I can't begin to explain how excited I am to delve into this! Thank you for the lead.
You can have a look at Richard Bird's book _Pearls of Functional Algorithm Design_. It's much more accessible than his earlier influential book _Algebra of Programming_.
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.
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....