[nilknarf]

The answer is surprisingly yes!

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

[kjeetgill]

I can't begin to explain how excited I am to delve into this! Thank you for the lead.

[yangzx]

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.

[kjeetgill]

Thanks!