3 ms·
That "facility" is the Curry-Howard correspondence!
by dronemallone 9y ago
That "facility" is the Curry-Howard correspondence!
- mafribe 9y agoNot necessarily. Isabelle/HOL, an prover not based on CH but on the LCF-architecture, can also do program extraction, see e.g. Program extraction in Isabelle: https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides....
- samth 9y agoExtraction of terms written using Fixpoint isn't really the Curry-Howard correspondence. Instead, the correspondence is between (for example) proofs of correctness and terms in the Calculus of Constructions. [Fixpoint terms are also CIC programs, so there's a sense in which they're related, but it's not really about Curry-Howard.]