|
|
|
|
|
|
by Footpost
2502 days ago
|
|
|
They 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. |
|
|