coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] license: derivative status of proofs

From: Tej Chajed <tchajed AT mit.edu>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] license: derivative status of proofs
Date: Tue, 14 Jul 2020 20:24:31 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT mit.edu; spf=None smtp.helo=postmaster AT outgoing.mit.edu
Ironport-phdr: 9a23:riOowx/WalT+t/9uRHKM819IXTAuvvDOBiVQ1KB41O4cTK2v8tzYMVDF4r011RmVBNudsKsP17aempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgRFiCCzbL9vIxm7ogrcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh/27XhM5/gqJVrhyiuhJx3ZLbbZqPO/ZiZK7QZ88WSXZDU8tXSidPApm8b4wKD+cZI+hXsYv9rEYQoBu+HwasBv3gxSJVjXLxwa01z+QhHhvE3AM+At0Dq3HUrNTpNKsIT++60bTIwCzFYvhL1jjz9JLGfQo9ofGQQ71wa8zRxFEhGQ7Kkliepo3oMTyJ2ukOvGaW7eVtWPyuhmMjtgx8vyWjy8cvh4TUmI8Z1FPJ+Dl4zYs0OdC1Vkx2bNGgHZZfsSyRKoh4Qts6Tm11uys20LkLtYSlcCUJ0pgr2gPTZ+SZf4SU5h/vTuWcLDdiiH57Zr6zmQy+/VWix+D4UMS/zUxEoTBfktbWs3AAzxzT5daDSvt65kqh3iuP1xzc6uFDIEA0k6XbJ4Qkwr4xipofq1rMETLrmEnuja+WcFsr+vSw5uj6YbjqvJuRO5Vqhgz9KKgih9GzDfw9MgcUXmib/eq81Kfk/U38WLhKkuE5kqnDv5DYO8sUu7W0AwpU0oY/8RqwESqp0MkAkXkdMF1FYA6Hj5TuO1zWPP/4Cu6/j02wnzdv2vDJJabsAo7NL3jGiLfuZ6xx609ayAopzNBQ/YhYCr8bIKG7Zkikv9vBSxQ9Lgb8l+3gEZB20p4UcWOJGK6Qdq3I5wym/OUqdtWBZsc+uD//JvRts+LljXY7lFM1eKi1m5YbdSbrTbxdP0yFbC+00Z86GmAQs19mFb24uBi5STdWIk2Kcec57zA/BpihCNaRQ4GxxrGNwXXiR8AEViV9ElmJVEzQWcCEVvMLMXLAJdJ9nTsFU7fnTo49kxyiqV2ikuY1Hq/v4iQd8Knb+p1t/eSCxxQz6Xp5A9nPi2w=

> On Tue, Jul 14, 2020 at 8:05 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

> Highly automated proofs often do not contain the representation of the code. The Ltac proof scripts are often just algorithms that find the concrete proof, when applied to the concrete Coq AST representation of the C code, the latter need not be distributed with the Ltac proof scripts.

I don't understand this point. The specification for the correctness proof must have a model of the C code, even if you elide proof scripts and the proof itself. This model need not be a full representation (it only needs to capture the execution semantics, so it can certainly elide things like comments and the exact syntax used), but it needs to show up in the theorem statement.

[Coq-Club] license: derivative status of proofs, Abhishek Anand, 07/15/2020
- Re: [Coq-Club] license: derivative status of proofs, Kevin Sullivan, 07/15/2020
  - Re: [Coq-Club] license: derivative status of proofs, Marco Servetto, 07/15/2020
    - Re: [Coq-Club] license: derivative status of proofs, Abhishek Anand, 07/15/2020
      - Re: [Coq-Club] license: derivative status of proofs, Tej Chajed, 07/15/2020
        
        Re: [Coq-Club] license: derivative status of proofs, Abhishek Anand, 07/15/2020
        
        Re: [Coq-Club] license: derivative status of proofs, Jim Fehrle, 07/15/2020
        
        Re: [Coq-Club] license: derivative status of proofs, Kevin Sullivan, 07/15/2020
        Re: [Coq-Club] license: derivative status of proofs, Izzy Hasson, 07/15/2020
        Re: [Coq-Club] license: derivative status of proofs, Jim Fehrle, 07/15/2020
        Re: [Coq-Club] license: derivative status of proofs, Abhishek Anand, 07/16/2020
        Re: [Coq-Club] license: derivative status of proofs, jonikelee AT gmail.com, 07/16/2020
        Re: [Coq-Club] license: derivative status of proofs, Jim Fehrle, 07/16/2020
        
        Re: [Coq-Club] license: derivative status of proofs, Stefan Monnier, 07/16/2020
        Re: [Coq-Club] license: derivative status of proofs, jonikelee AT gmail.com, 07/16/2020