<p>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.</p>
<p>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.</p>
<p>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.</p>
<p>For intros on this, see:</p>
<ul>
<li><a href="https://cs.ru.nl/%7Ewouters/Publications/ThePowerOfPi.pdf" rel="nofollow noreferrer">https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf</a></li>
<li><a href="http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf" rel="nofollow noreferrer">http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf</a></li>
<li><a href="https://www.manning.com/books/type-driven-development-with-idris" rel="nofollow noreferrer">https://www.manning.com/books/type-driven-development-with-idris</a></li>
<li><a href="https://mitpress.mit.edu/books/little-typer" rel="nofollow noreferrer">https://mitpress.mit.edu/books/little-typer</a></li>
</ul>

CC BY-SA 4.0
2020-08-11T05:28:21.473Z
2020-08-11T05:28:21.473Z
Joey Eremondi
<p>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.</p>
<p>I wonder if there is such theory or maybe attempts to formalize explanations?</p>
<p>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.</p>

CC BY-SA 4.0
2020-08-10T14:49:47.943Z
As the question is posed, I don't agree with the premise.  The two main standard rationales for an algorithm are (i) that it works (is correct) and (ii) that it is efficient enough to be useful.  It is standard practice to formally (mathematically) prove (or disprove as the case may be) that a proposed algorithm has these properties.  Maybe you could explain more clearly what you mean by "rationale" and "formal system"?
Neal Young
<soft-question><advice-request>
Formal theory about explaining algorithms
Artem Kokorin
# Formal theory about explaining algorithms

(Asked by: username_0 on 2020-08-10)

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.

**Tags:** soft-question, advice-request

> **Comments:**
> **username_1**: As the question is posed, I don't agree with the premise.  The two main standard rationales for an algorithm are (i) that it works (is correct) and (ii) that it is efficient enough to be useful.  It is standard practice to formally (mathematically) prove (or disprove as the case may be) that a proposed algorithm has these properties.  Maybe you could explain more clearly what you mean by "rationale" and "formal system"?  

---

## 1 answers

### Answer by username_2 on 2020-08-11. Score: 4 | Accepted answer

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 "why" 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](https://cs.ru.nl/%7Ewouters/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>


---

