There is a lot of algorithms written in formal languages, but I have never seen any formal system which target is to explain or give a rationale behind an algorithm. It seems that when constructing examples, authors have to create both interesting, somewhat random, and small samples. I think this task could be formalized to some degree.
I wonder if there is such theory or maybe attempts to formalize explanations?
Edit: I was looking for a theory that describes how to teach other people an algorithm. As mentioned by jmite, it is possible to create a self-explaining algorithm using dependent types to solve this problem.