Correctness, explanation and intention (Q2179349)

This interesting paper is centered around the notion that good solutions and proofs have to be explanatory and provides appropriate reasoning and examples from computer science. Among other things, the author emphasizes that, while a correct solution may consist of an enumeration of the results, such extensional solutions are ``at best impractical and at worse (sic!) impossible''. Obviously, they are not explanatory. The author discusses nice explanatory solutions based on well-known Hoare-style correctness proofs [\textit{C. A. R. Hoare}, Commun. ACM 12, 576--580 (1969; Zbl 0179.23105)] and remarks, in particular, that ``mathematicians seek new proofs of known theorems because the new proofs throw more light on matters -- they provide better explanations of the result''. One can only agree with the author's observation that ``establishing and explaining why a program meets its specification is part of the activity of programming''. More technically, he also properly notes that in Hoare-style proofs the correctness of the whole is compositionally constructed in a way that follows the structure of the program. Finally, when characterizing a physical computation, the author -- again, properly -- states that it is not the physical device that determines whether the specification is true because ``the aim is to show that an artefact satisfies its abstract specification''. Ideas similar to those discussed in the paper under review have been presented earlier by other authors not quoted in this paper, notably, by \textit{E. W. Dijkstra} [``Some meditations on advanced programming'', in: C. M. Popplewell (ed.), Information processing 1962. Proceedings of IFIP congress 62. Organized by the International Federation for Information Processing, Munich 27 August -- 1 September 1962. Amsterdam: North-Holland Publishing Company. 535--538 (1963)] (who also mentioned physical correctness, for example, in [\textit{E. W. Dijkstra}, On the role of scientific thought. EWD 447 (1974), \url{https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/EWD447.html}], and always stressed the needs to separate concerns and to be explicit about program design considerations and design process), by \textit{Yu. I. Manin}, who famously observed that ``a good proof is one that makes us wiser'' [A course in mathematical logic for mathematicians. 2nd ed. Berlin: Springer (2010; Zbl 1180.03002)], and by others who also noted, for example, that not only proofs and programs, but also specifications may and ought to be convincing [\textit{H. Kilov} and \textit{A. Ash}, ``On the structure of convincing specifications'', in: Behavioral specifications of businesses and systems. Dordrecht: Kluwer Academic Publishers. 141--160 (1999)]. For the entire collection see [Zbl 1428.68037].