The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Le 08/01/2020 à 20:00, BEGAY Pierre-leo a écrit :

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

Thanks Pierre-Léo for the ad! ;-) Note that until some time ago Dedukti was not an interactive proof assistant but just a type-checker. We are currently working in turning it into a full proof assistant with tactics and some LSP-based interface (emacs and vscode). See https://github.com/Deducteam/lambdapi for more details. The interesting point of Dedukti and its new version is that functions and predicates can be defined by giving arbitrary rewriting rules. Rehan Malak and Bruno Barras use this feature to develop models of cubical type theory. Best regards, Frédéric Blanqui, coordinator of the development of the new version of Dedukti.

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