coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [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: Re: [Coq-Club] Abandoned proof engineering efforts
Date: Sun, 16 Feb 2020 11:18:41 -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-f176.google.com
Ironport-phdr: 9a23:xshwBB2Q/wUrrzH/smDT+DRfVm0co7zxezQtwd8ZseIWKPad9pjvdHbS+e9qxAeQG9mCt7Qb16GP6fqocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLx/IA+0oAjeucUanJVuJrgswRbVv3VEfPhbymxvKV+PhRj3+92+/IRk8yReuvIh89BPXKDndKkmTrJWESorPXkt6MLkqRfMQw2P5mABUmoNiRpHHxLF7BDhUZjvtCbxq/dw1zObPc3ySrA0RCii4qJ2QxLmlCsLKzg0+3zRh8dtjqxUvQihqgRwzI7aYo6bNPRwcKDAc90EWWVMRdxeWzBbD46mc4cDE+gMMOBFpIf9vVsOqh6+CBGyCuz1zj9Ih2X51rAm3eQgFwHG0xIvH8gTu3nTsNX1LqYSUea6zKbW1zXOdO9Z2Szn5InGaB8huvGMXbN2ccre1UkvEAXFgk+OpoP4IjOYz+IAuHWY4ep4Te+jlXIrpgVrrjWsxsogkJTFi4MUx1ze6Cl0woc4KNulQ0Bhe9GkCoFftySCOot2XMwiR2ZotT4/yrIcuJ67eDEGyJUjxxLCcvCHfZWE7xDiWeqLLjd4g3VleL27hxms60Sv1ur8Vsys3FZLqCpKjMXMu2gT2xDP7sWLUPhw80e71TqS1g3e6/tILV02mKfaM5Ihx6Q/lpsXsUTNBC/2n0D2gbeKdkU+++io7evnbav8ppKHK4B0kRvyM6o0lcykAeQ4Mw4OX2eH+eS70r3v51P2T6hXjvEuiKnWrIjaJdgHpq6+GwJazoEj6w+mAzi61NQYgGIIIUleeBOHiojpI0vBLOr5Dfe5mVSskS1ky+rIPr37Ud3xKS3ol66kVrJg4QYIww0qiNtb+ph8C7cbIfu1VFWn8JTZFRYzPgiwzqP6E9hnzctKWHmGCKKdNK6XrESF/PkHKO3Kb4YQ/j/2beUmsa3Al3g8zGMUeaiglaEWbn+1BLwyP1+YZ3XhmP8KCiEVtxE+TerllFqEFzNfeiDhDOoH+jgnBdf+Xs/4TYe3jenZhXbpLthtfmlDT2u0PzLtfoSAVe0LbXvDcMR61CMNTrigTYA90hfouQPnmeM+c7jkvxYAvJem7+Bbou3ekRZoq25xBsWZlmCJFiR6xzxWATAx2697rAp2zVLRifEk0cwdLsRa4rZyail/LYTVlr0oAMu0RQvaftaPR0qhRJOrDSxjFt8=

To clarify: any size project in any proof assistant is fine. I'd actually really love examples of projects of different sizes in different proof assistants. The more examples, the better.

On Sat, Feb 15, 2020, 5:27 PM Talia Ringer <tringer AT cs.washington.edu> wrote:

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