coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Marco Servetto <marco.servetto AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] That time we proved False in Coq
Date: Wed, 29 Dec 2021 09:19:22 +1300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=marco.servetto AT gmail.com; spf=Pass smtp.mailfrom=marco.servetto AT gmail.com; spf=None smtp.helo=postmaster AT mail-lj1-f169.google.com
Ironport-data: A9a23:HdUj8Kmx5IWlsu+JO6vbfWHo5gzpJ0RdPkR7XQ2eYbTBsI5bpzBSnTdNCGyBP6yJYzPyKtp+Oti28kJXuJXVmoBiSVBu3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t512huEtnanYd1eEzvuWGuWn/SkUOZ2gHOKmUbeeYHApHmeIdQ944f5ds75h6mJXqYPha++9kYuaT/z3YDdJ6RYsWo4nw/7rRCdUgRjHkGhwUmrSyhx8lAS2e3E9VPrzLEwqRpfyatE88uWSH44vwFwll1418SvBCvv9+lr6WkgDQ7qXOQrXz3QPBfnkjR9FqSg/lK08MZLwa28N02TPz403ko0d88XuGG/FPYWU8AgZexxRCSp5e7ZL4qHKPWS4mcOWxkzCNXDrxp2CCWlvZNNEpb8oaY1J3aVAdGplggq4r+mx2fewTvRmrt8yKdHieoIZoHBpiz/DZcvK67jXG/CQo4BMhWJowJhaR6OGIZBIOGN7N0GYJUBbZQI+FrYVmcOEhl3eehtksnarpI8jujCGlEgoi6yF3MH9f9WLQYBRnB/dqDuYriL2BRYVMNHZwj2Amk9AT9TnxUvTML/+3pXhnhKrvLGS+oDXIBgfVF/+pfvgz0DnBYMZJEsT9S4j66M18SRHi/GVswKQ+Ba5Utw0ArK80NHWLCmCz6PV50CSAW1sovtpdok9rMFvLdA1/gbhoj4qbACDdJWaTHuc8vGfqjba1e09RYMdTXdscDbpKOUPbG3+Ytwjgzqj/GOIYgXJJAzN
Ironport-hdrordr: A9a23:FZTtqKGJbg3mr++ZpLqE5ceALOsnbusQ8zAXPiFKOHtom6mj/fxG885rtiMc5AxwZJhCo7G90cu7MBHhHPdOiOF7AV7IZniChILHFvAH0WIg+VHd8u/Fm9K1GZ0OT0G2MrPNMWQ=
Ironport-phdr: A9a23:qDiftB1VtsCdq+hXsmDOtwQyDhhOgF0UFjAc5pdvsb9SaKPrp82kYBaGo6w03RSQBtiTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yf2+94fObwlVgDexbq5+IRu2oA7MqsQYnIxuJ7orxBDUuHVIYeNWxW1pJVKXgRnx49q78YBg/SpNpf8v7tZMXqrmcas2S7xYFykmPHsu5ML3rxnDTBCA6WUaX24LjxdHGQnF7BX9Xpfsriv3s/d21SeGMcHqS70/RDKv5LppRhD1kicKLzE2/mHZhMJzkaxVvg6uqgdjw4LIeoyZKOZycr/fcN4cWGFPXtxRVytEAo6kaIUAFfABMvpfr4LgulUBswG+BReyC+Pz1j9IgWL90Ko/0+s7CwHJwAsgE8gVsHvKttX1KrkdUfypzKnP1jjDYPZW1i386IjMaBwuvfaMXbdpfMfX1EIgGB/LgE+Kpoz5IzOayP4Ns26D4ud9W+yjlWEpph9/rzWtwsohiI3Eip8Ux13Y6Cl3wIg7KNO3RUN7fNOpE4ZcuS6GO4drQc4sQ3xktSg4x7MJt5C2ejUBxpc/xxPHdfCLb4yF7gjgWeuROzt0mm5pdbGlixqv8EWtzuvxXdSu3llQtCpKiNzMu2gN1xPN7siHTeNw/kK71jaO0wDf8+VEIUIpmabCJZ4t3789m54JvUTMGS/2n0r2jKuIeUk+5ueo7OHnbq3npp+aKYB0lhnzProylsG7G+g1MQgDU3KF9eig17Dv51D1TbROg/Eul6nWqpHaJcAVpq6jBA9V154u6xOlADe8zNsYmmMLLElbdxKdkYjmJU3OIOz/DfqkjFSslS1kx/HCPrH7HprNKX3DnK/7fblh805c1BYzzddH6p1IDbEBOev/VVP1tNzFFRA0KBe0wubiCNVlzIwSQ2OPAqmDMKPTq1CE/OwvI/PfLLMS7T36Mr0u4+PkpX4/g14UO6ezjrUNb3XtO/18KELRWnf2nNodDWBC6g83VuftzkaPSyBee2q1d6057zA/TomhCNGQFciWnLWd0XLjTdVtbWdcBwXUeZ8NX4qBUvYILimVJ505+tTrfbekQo4lkxqpsV2jo1KGBu/d+yldsZC6kdYsubyVmhY1+jh5Sc+a1jPVJ1w=

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