6
$\begingroup$

Major proof assistants like Lean and Coq are fundamentally based on the Curry-Howard correspondence: propositions are encoded as types, quantified propositions are encoded as dependent types, proofs are instances of those types, and so on.

On the other hand, I read that Isabelle (another major proof assistant) is not based on the CH correspondence.

My question is: what are the advantages (and disadvantages) of basing a proof assistant on this correspondence?

$\endgroup$
3
  • 1
    $\begingroup$ langdev.stackexchange.com is riddled with "pro and con" questions, and when someone fails to list some cons in their anwer, they get told off and downvoted. I do hope we're not adopting their customs. $\endgroup$ Sep 19, 2023 at 12:52
  • $\begingroup$ BTW, I don't know how tags are managed on SE, but I'm surprised I couldn't find any "Curry-Howard" related tag here. $\endgroup$
    – Weier
    Sep 19, 2023 at 12:54
  • $\begingroup$ Strange, I added the tag, let's see what the moderators will do. $\endgroup$ Sep 19, 2023 at 13:06

1 Answer 1

3
$\begingroup$

Let us separate two things here: having dependent types, and using them to express logic a la propositions-as-types.

As far as formalization of mathematics is concerned, there are no disadvantages to having dependent types. Mathematics is naturally expressed using dependence and any attempt to remove it results in awkwardness that is then remedied in one way or another.

Regarding the second point, neither Lean nor Coq use propositions-as-types. They both have a notion of impredicative propositions, through which logic is expressed in a standard form.

However, there is something to be said about pure propositions-as-types and pure logic. They are both inadequate for formalization:

  • In pure propositions-as-types a la Martin-Löf type theory we cannot express abstract existence, i.e., that something exists without having access to a specific witness, as we must always use $\Sigma$, which automatically exposes the existential witness. Thus for example there is no reasonable definition of surjection in Martin-Löf type theory. One has to do acrobatics known as "setoids".

  • In pure logic we cannot express explicit existence, i.e., that we have actually constructed a specific thing, as we must always use $\exists$, which automatically hides the existential witness. One consequence of this is that mathematicians are unable to speak precisely. They write "there exists $X$ such that ..." instead of "we construct $X$ such that ..." because someone told them in logic class that $\exists$ is the only formal notion of existence.

Mathematics needs both kinds of existence. Lean has it, Coq has it, Homotopy type theory has it. Agda does not (without postulates) and HOL does not either because it is a logic (although it compenstates by having an expressive term language and meta-theoretic devices, such as definitions).

$\endgroup$
14
  • 1
    $\begingroup$ I think some talk about the Curry Howard isomorphism in a looser sense (for pedagogical purposes) as explaining why Lean (or Coq) uses the same language for term proofs and definitions. Of course those proofs take place in Prop so it isn’t full CH isomorphism. (I think you could find it used this way in TPIL which is maybe where the OP is getting this idea.) $\endgroup$
    – Jason Rute
    Sep 19, 2023 at 13:09
  • 1
    $\begingroup$ Well, it is not a good idea to dilute the Curry Howard correspondence by making it more non-specific and historically inaccurate. For pedagogical purposes, perhaps it would be better to remind the students (and apparently their teachers) that Russell's and Church's type theories had types of logical truth values, and so one was free to mix "logic" and "other types". The Curry-Howard correspondence came a lot later, and was and is traditionally tied to the idea that "all types" can serve as propositions. $\endgroup$ Sep 19, 2023 at 13:13
  • 1
    $\begingroup$ “there are no disadvantages to having dependent types”. I think to be fair to the Isabelle/HOL folks, they would say DTT has some disadvantages like a larger kernel, a more complicated logic that is further from standard set theory foundations, etc. $\endgroup$
    – Jason Rute
    Sep 19, 2023 at 13:14
  • 1
    $\begingroup$ The Isabelle/HOL folks are more than welcome to explain their point of view in a separate answer. See my comment below the question. Also, I specifically qualified my statement with "as far as formalization of mathematics is concerned" (so not "as far as meta-theory is concerned" or "as far as implementation is concerned"). $\endgroup$ Sep 19, 2023 at 13:15
  • 2
    $\begingroup$ Being further from standard set theory foundation is an advantage in many respects. $\endgroup$ Sep 19, 2023 at 13:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.