The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

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.