coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] That time we proved False in Coq

From: public <aa755 AT pm.me>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] That time we proved False in Coq
Date: Tue, 28 Dec 2021 20:34:22 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=aa755 AT pm.me; spf=Pass smtp.mailfrom=aa755 AT pm.me; spf=Pass smtp.helo=postmaster AT mail-40133.protonmail.ch
Ironport-data: A9a23:vpuu5KANDtvUYhVW/3Diw5YqxClBgxIJ4g17XOLfBAS5gjsmhTYCxmpKX2mCaKqPYWb2ctoiO9639UlQv5Skm99gGjLY11k9FiMQ8ZKt6fexdxqrYXvKdqUvdK/WhiknQoGowPscEzmM9n9BDpC79SMljPvSFuKnYAL5EnkZqTFMGH9JZS1LwLZRbr5A2bBVMivV0T/Ai5W31GyNh1aYBlkpB5er83uDihhdVAQw5TTSbdgT1LPXeuJ84Jg3fcldJFOgKmVY83LTegrN8F251juxExYFD9qklvOnKhRRGfjKJw+SjXxTUqmmxBNCzsAw+v9rabxDMQEL03PQxIsZJNZl7fRcTS8gN/KRxcwFVl9dHkmSOIUfoeGaeSPh2SCU5xaeIia9k6UG4FsNFYYf46N8BXxE3ecJLSgEKBGFneO/hryhItSALOw3dJywet4L4yQ4i2nNV6N+B8qeHfvevooAmmok2ZVnA9D1Yuw1aR5OZTL8eTtbYw9CUtZkiI9EnVH6ejxc7Q7N/PFspXDJyxB21r3kMd6TcdzieCmcpW7AzkquwogzKkhy2B2jJTu5HraEg+bOmWanANtJT/ug7Pl2h1uWz20XThYWPbd+iefskVawArqzNGRNkhfCb4BrnKBocjU5dwW95nuJ1vLZc8QFCPU0sWlh1YKNizt0xQE4ovppcNlgscJeqfkCvrOWt4uBOAGDe4F5hZ5QGnl4YN9y1eUowbc+WBI5
Ironport-hdrordr: A9a23:ikllbKNHP9pIgcBcTsyjsMiBIKoaSvp037BN7TEVdfU1SL37qyjN9M5w6faaslYssR0b9OxoW5PvfZq0z/ccirX5W43CYOCMggeVxe9ZgrfK8nnLEyr38+RQ9aoISdkcNOHN
Ironport-phdr: A9a23:ILkOthaKswLiJxc1Z0miy7X/LTEr0IqcDmcuAnoPtbtCf+yZ8oj4OwSHvLMx1gaPBNyKoKsf2qL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNfglEniexba52IRm5sAncuM0bipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2ThLjlSUJOCMj8GzPhMJ+kqJVoAi8qRJ8wYHUbo6aO+ZxcK7GYdMaXHBMUtpNWyBdAI6xaZYEAeobPeZfqonwv0MOrQalCgmoBePg1iJDi3js0qIg0eksEQHL0Rc4H9ILqnjUqcv6Ob4UXOuow6bG0S/NYOlK2Tfh9ofIaBYhrOmCUL9ybMbczVcjGQPKg1mNrYHrMC+Z2vgDvWab8+duWv+jhm4ppQxsoDWhycQhhpTGiI8bxV7J9jh0zYc1K9GkTkNwfNCqEJxVty6ANot2RNsvQ25puCYmyr0GpIW0cDIWx5Qgwh7SbeGMfYuQ4h/7SeqcIjd1iGhndb6jnRq//lSsxvfhWsS63ltHqDdOnMPWuXAXzRPT79CKSvtj8Uel3jaCzwXT5ftFIUAwjKbWJIItzqM+m5cdq0jDBjX2mELqjK+RcEUk//Kn6+XjYrn8upCcN5d4igD4MqswhsyyGfk0PwsOUmSB++mwyKfv8ELlTLlQk/E7nKfUvIjfJcsBp665BwFV0pwk6xa6Fzqpys4XkHsHIV9FYx+Hl43pN0vLIP/mFfu/mUijkC93x/DaOb3sGonCLn/akLv4Ybl971NcxxEowNBE55NUD6kBL+jpVk/wstzYFB45PBauz+bpEtUunr8ZDGmIG+qSNL7YmV6O/OMmZeeWN7UYoDLsF/9w/+PkiX4y0QsUdPb0gLMPbTa9E6I1DV+eZC/0n90FEGxC6gM3E7G3oEWHFzteMSXhF5kg7y02Xdr1RbzIQZqg1eTpNMaTG5RXYiUaUgnXSjHwbYKYXPEJYSOWZMRhwGVsvVeJU4pn0Bz87WcSLpJ/K6zR939A3a8=

I wrote a wiki article about the last such incident I remember.
https://github.com/coq/coq/wiki/CoqTerminationDiscussion
(others have since contributed to the article)

Regards,
Abhishek Anand

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐

On Tuesday, December 28th, 2021 at 3:19 PM, Marco Servetto
<marco.servetto AT gmail.com> wrote:

> Hi,
>
> I'm writing a little document talking about soundness/unsoundesses in
>
> verification systems.
>
> I remember that there was a time we managed to prove False in Coq, and
>
> the community came together effectively and promptly to fix it, and
>
> all major proofs were unaffected by the fix. I also remember members
>
> from other communities (Agda?) coming to give a hand.
>
> While I'm not a Coq genius, seeing the honesty and the clear polite
>
> and direct action made by this community filled me up with hope for
>
> the
>
> future.
>
> Do I remember correctly? Can someone help me to summarise the event
>
> and provide some references? Do you have references to other important
>
> tools that have been proved unsound and any discussions about the
>
> response of their community?
>
> Marco.

[Coq-Club] That time we proved False in Coq, Marco Servetto, 12/28/2021
- Re: [Coq-Club] That time we proved False in Coq, public, 12/28/2021
  - Re: [Coq-Club] That time we proved False in Coq, Mario Carneiro, 12/29/2021
    - Re: [Coq-Club] That time we proved False in Coq, Abhishek Anand, 12/29/2021
      - Re: [Coq-Club] That time we proved False in Coq, Jason Gross, 12/29/2021
        
        Re: [Coq-Club] That time we proved False in Coq, Mario Carneiro, 12/29/2021
        
        Re: [Coq-Club] That time we proved False in Coq, roux cody, 12/29/2021
        
        Re: [Coq-Club] That time we proved False in Coq, Jason Gross, 12/29/2021
        
        Re: [Coq-Club] That time we proved False in Coq, Yannick Forster, 12/30/2021
        
        Re: [Coq-Club] That time we proved False in Coq, Pierre-Marie Pédrot, 12/31/2021