3 ms·
Theorem provers using constructive logic have the nice property that proofs are programs; if you have a proof that A implies B, and you have an A, you can produ
by logicchains 6y ago
Theorem provers using constructive logic have the nice property that proofs are programs; if you have a proof that A implies B, and you have an A, you can produce a B. Classical mathematics is usually based on set theory plus the axiom of choice (implying law of excluded middle), which allows non-constructive proofs (which don't compute). If the computer knows "not not X" implies "X" due to the law of the excluded middle, it can't necessarily produce an "X" from an "not not X".
The most popular theorem provers (at least among computer scientists) are based on some form of Martin-Löf type theory. In these theories, some very helpful proof techniques (often used in classical mathematics) like function extensionality and quotients don't compute. While they can be added as axioms, this breaks the computational property of the proof. What HOTT brings is a type theory with an improved notion of equality in which such things do compute, based on the notion of transport along equivalences.
If have two types
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
Inductive natural_number : Set :=
| Zero : natural_number
| Successor : natural_number -> natural_number.
And I have proved something about nat, HOTT allows me to automatically convert that proof into a proof about natural_number (after showing nat is isomorphic to natural_number).
- pgustafs 6y agoYep, and you could even prove "nat" is isomorphic to the type of binary numbers "Bin := List (0 | 1)" and transport proofs there too.
- momentoftop 6y ago> The most popular theorem provers (at least among computer scientists) are based on some form of Martin-Löf type theory. Are they? Judging by posts on HN, I 100% agree. But judging by the number of users and the amount of verified mathematics and code, I'm not so sure. Maybe things have changed recently, but I believe that systems based on simple type theory (HOL and Isabelle) and systems based on set theory (Mizar, Metamath) have much larger repositories of verified mathematics and verified programs than those based on dependent type theories.
- logicchains 6y agoI don't have hard numbers to prove it. But I think it's significant that https://deepspec.org/main https://deepspec.org/main, the largest recent formal verification project (at least in the US) chose to use Coq, which is based on type theory. There's also Coq-verified code in Chrome (http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP1...), a claim that can't be made for any other theorem provers (as far as I'm aware).
- The_rationalist 6y agoHow do you prove isomorphism between those two types?