4 ms·
The trouble with HoTT is that it has very little to offer in regards to making it easier to prove the correctness of programs expressed in Hoare logic (which is
by krapht 7y ago
The trouble with HoTT is that it has very little to offer in regards to making it easier to prove the correctness of programs expressed in Hoare logic (which is ~99% of all computer programs).
- JadeNB 7y agoBut the trouble with focusing effort on tools that can serve our current programs is that it guarantees that we are locked into our current programming models instead of exploring new design spaces.
- Footpost 7y agoThey are not mutually exclusive: - Use HoTT or any other type theory as a logic / foundation of math. - Use Hoare logic to reason about programs, using your logic / foundation of math to deal with inferences that are not given by the rules of your Hoare logic, i.e. for Hoare's "Rule of Consequence". There are several ways of connecting the two. One is Hoare type theory [1]. Another is using Characteristic Formulae [2, 3]. [1] G. A. Delbianco, A. Nanevski, Hoare-Style Reasoning with (Algebraic) Continuations. [2] L. Aceto, A. Ingolfsdottir, Characteristic Formulae: From Automata to Logic. [3] A. Chargueraud, Formal Software Verification Through Characteristic Formulae.