The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Last I checked, the plan was to allow for simple, verified extensions to Coq in order to handle computational interpretations of different axioms. Nicolas Tabareau gave a talk about this at ITP.

It remains to be seen whether this is possible in a way that does not have serious drawbacks, as I gather the customizability of Isabelle is one of the biggest pain points, and most users only ever use Isabelle/HOL anyways. Perhaps having different proof assistants for different needs is a perfectly acceptable status quo. That is, after all, true for other programming languages. 

Maybe the right focus in that case is interfacing between proof assistants, so that we can have projects that use bits and pieces of both as applicable. Or automatic reuse of programs, specifications, and proofs across different proof assistants when possible, with some kind of verified guarantee about the layer interfacing the tools.

On Wed, Jan 8, 2020, 12:44 AM Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr> wrote:

Hello,

Le 08/01/2020 à 02:50, jonikelee AT gmail.com a écrit :
> [decloaking from lurker mode to add my $0.02]
>
> Does having LEM built into Lean interfere with the user's ability to exploit the Curry-Howard isomorphism?
>
> If so, that seems like a bad trade off: a small convenience for a
> small group of people (Fields Medal wanabees) that imposes a large
> inconvenience for a large group of people (software engineers).

Actually, I guess that a classical interpretation of "Prop" is
compatible with *many* certified software development in Coq. For
example, consider the CompCert compiler: currently, it is intented to be
used through Coq extraction, and since the current Coq extraction
removes Prop contents, it is consistent with proof-irrelevance and
classical propositions.

Thus, as I understand it, supporting non-classical propositions is
motivated by higher-order mathematics or by programming on propositions
in the proof assistant... Hence, the picture is quite the opposite:
currently, most people using maths (including software engineers) do not
care of constructive propositions, and simply use classical logic,
because it is convenient.

But, this does not mean that proof assistants should only care about the
majority. For example, it would be great to have an enhanced Coq
extraction, able to deal with an univalent version of equality (this
would provide a powerful mechanism of "coercion"). Is there any progress
in this direction ?

Sylvain.