The Coq mailing list

[BEGAY Pierre-leo <pbegay AT ens-cachan.fr>]

Talia Ringer <tringer AT cs.washington.edu> a écrit :

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

You might want to take a look at logipedia and Dedukti. I am no expert on this (I only saw a talk about it given by Gilles Dowek, who I assume is the leader on both projets), but as far as I understand, the former is an encyclopedia of proofs across different languages built upon the latter. The point of this seems to be the analysis of the need for theory-specific axioms in different proofs, to see if they could be translated to assistants built around weaker theories. I'm not sure how operational this whole thing is though.

Pierre-Léo

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