4
$\begingroup$

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.

Improve this question
$\endgroup$
1
  • 5
    $\begingroup$ 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"? $\endgroup$
    – Neal Young
    Aug 10, 2020 at 14:49

1 Answer 1

Reset to default
4
$\begingroup$

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:

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.