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?
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).
