coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Frédéric Blanqui <frederic.blanqui AT inria.fr>
Cc: <coq-club AT inria.fr>, <homotopytypetheory AT googlegroups.com>, <agda AT lists.chalmers.se>
Subject: Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq
Date: Tue, 07 Jan 2014 14:33:12 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; q=dns; s=mandrill; d=mailbagger.com; b=L+Feptb3OU7OHZjfqkgWz52i8tOEjhEf0CFkGShnON9AfUDT+vnLO3hIe7MURFhwdazlOB9RFNl3 TNX8SWxku1wGFTRq0AiXba8OM+oK4UmLW09EnDQUAynluGVafhkftX01hc2kRdxcgZ1m44fx1fqx /NP+74k57mlyFuUeNw8=;

On Jan 7, 2014, at 5:01 AM, Frédéric Blanqui
<frederic.blanqui AT inria.fr>
wrote:

> This of course may raise
> problems for making sure that such definitions are consistent, but it is
> another (interesting) problem.
>

Do not forget that proof assistants are there precisely because we need
proofs which we know are correct. So a proof assistant which certifies
incorrect proofs is useless except for experimental purposes.

For those of us who want to *use* proof assistants not to develop proof
assistants the consistency issue is crucial.

Vladimir.

Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, (continued)