3 ms·

For those who want to understand what Homotopy Type Theory is, here is the "standard text" free to download or online: https://ncatlab.org/nlab/show/Homotopy+T

For those who want to understand what Homotopy Type Theory is, here is the "standard text" free to download or online: https://ncatlab.org/nlab/show/Homotopy+Type+Theory+--+Univalent+Foundations+of+Mathematics https://ncatlab.org/nlab/show/Homotopy+Type+Theory+--+Unival...

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 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 ago
    But 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 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.
nudpiedo 7y ago
Thanks for sharing. So it is basically a research programming language implementing some modern mathematical theories?
- alimw 7y ago
  While Homotopy Theory is just one strand in modern mathematics, it is believed that a type theory based on it can serve as a foundation for the whole of mathematics.

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 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 ago
  But 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 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.

nudpiedo 7y ago

Thanks for sharing. So it is basically a research programming language implementing some modern mathematical theories?

alimw 7y ago
While Homotopy Theory is just one strand in modern mathematics, it is believed that a type theory based on it can serve as a foundation for the whole of mathematics.