3 ms·
Though note that it is not simple to understand; it will take quite a lot of real work to grok, unless for some reason you already know about univalence.
by Smaug123 7y ago
Though note that it is not simple to understand; it will take quite a lot of real work to grok, unless for some reason you already know about univalence.
- krapht 7y agoThe 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.