coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Abandoned proof engineering efforts

From: Talia Ringer <tringer AT cs.washington.edu>
To: Coq-Club <coq-club AT inria.fr>, isabelle-users <isabelle-users AT cl.cam.ac.uk>
Subject: [Coq-Club] Abandoned proof engineering efforts
Date: Sat, 15 Feb 2020 17:27:23 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-il1-f178.google.com
Ironport-phdr: 9a23:fujscBAkeusaJVUtbydxUyQJP3N1i/DPJgcQr6AfoPdwSPvyosbcNUDSrc9gkEXOFd2Cra4d16yJ6Ou7ByQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vIxi6twfcu8cZjYZsK6s61wfErGZPd+lKymxkIk6ekQzh7cmq5p5j9CpQu/Ml98FeVKjxYro1Q79FAjk4Km45/MLkuwXNQguJ/XscT34ZkgFUDAjf7RH1RYn+vy3nvedgwiaaPMn2TbcpWTS+6qpgVRHlhDsbOzM/7WrajNF7gqBGrxK7vxFwzI7abo+WOvRjYK3SYcgXSnBdUstLTSFNHp+wYokJAuEcPehYtY79p14WoBWgHwasAOLvxSVVjXHq3K061eshHh/c3Ac9GN8OrG7UrNTzNKcdT++11rLFwinYb/9M1zby8pPIchAgofGKUrJwbc3RyU81Gwzbk1qQtJXoMjWI3eoOq2iW9/RsWf6rhmI9qAx8oiKjytoth4TInI4Z11LJ+CZ/zY0oP9O3UlR7bsShEJZItyGVKY92QsQ6TmFtoik6y7kGtYe6fCgO1Zgr3hDfZ+GFfoWL+B7jW+GRITB3hHJhZr2znQq98U+lyuHkV8m01khFrjZdn9XSqnwA0wbf58uHR/dn40us2DeC2xrO5uxGIk04ja/bJIQgwr40mJoTq0PDHirulUXqlq+Wd0Mk+ue25OT9ebjpuoScO5V6iw7kKaQums2/AeI3MggSWGib//6w26P+8k3kWLlKlOE5krHFsJDGIsQWvrK2AwhM0oo69xm/Cyqm388DkHkcLFNFfQqHgJLzN1HPJvD4F/a/jE62nDdl3fCVdoHmV77KNz3olKrrNeJ27FcZww4ux/he4YhVA/cPOqS3Ek7qvdbVChs0dhGvzvz8QIF8zYoUVGaLD+qEK67IqneD4qQkKuzKbYRTpTWreNY/4Pu7sXY9mFZVR6iv0pYNICSkBPVgLEiDSXH3xMgICmcLuAUiS+qshVGfB20AL02uVr4xs2loQLmtCp3OE9j03O6xmRyjF5gTXVhoT0iWGC65JY6fHegFcyKTJMB9lTpCWLS8Gdd4hEOe8TTiwr8iFdL6vygRtJbtzt9wvryBngp06jVvD8Wb3H2KSSd5kn5aHmZrjpA6mlR0zxK46YY9g/FcEoYNtfZAUwN/NJqFiuIjVIC0VQXGcdOEDl2hR4f+DA==

Hi all,

I'm curious if any of you have ever started to verify a system, but then abandoned that system due to the difficulty of evolving and maintaining your proofs. If so, I would love for you to share those proof efforts with me, especially if the code is public.

Thanks!

Talia

[Coq-Club] Abandoned proof engineering efforts, Talia Ringer, 02/16/2020
- Re: [Coq-Club] Abandoned proof engineering efforts, Talia Ringer, 02/16/2020
  - Re: [Coq-Club] [isabelle] Abandoned proof engineering efforts, Christoph Sprenger, 02/18/2020
- Re: [Coq-Club] Abandoned proof engineering efforts, Jason Gross, 02/16/2020
  - Re: [Coq-Club] Abandoned proof engineering efforts, Jason Gross, 02/16/2020
- Re: [Coq-Club] [isabelle] Abandoned proof engineering efforts, Denis Nikiforov, 02/18/2020
- RE: [Coq-Club] [isabelle] Abandoned proof engineering efforts, Fernandez, Matthew, 02/18/2020
  - Re: [Coq-Club] [isabelle] Abandoned proof engineering efforts, Stephan Merz, 02/18/2020
    - RE: [Coq-Club] [isabelle] Abandoned proof engineering efforts, Fernandez, Matthew, 02/18/2020
  - Re: [Coq-Club] Abandoned proof engineering efforts, Jan Bessai, 02/18/2020