Formal theory about explaining algorithms 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.
This might not be what you're looking for, but I think this is somewhat covered by the theory of dependent types, specifically intrinsically typed data structures.
The idea is that, instead of having an algorithm along with a proof of correctness, you start with a type that describes the properties of a solution. Then you simply write a program of that type, and you are guaranteed that it is correct.
Does this mean that you get correctness for free? Certainly not. But now the &quot;why&quot; at each stage is clear. The presentation of the algorithm and the explanation are one and the same. The notion of of correctness is formalized, and baked into the language itself.
For intros on this, see:

https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf
http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
https://www.manning.com/books/type-driven-development-with-idris
https://mitpress.mit.edu/books/little-typer