coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Abandoned proof engineering efforts

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Abandoned proof engineering efforts
Date: Sun, 16 Feb 2020 17:12:58 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f41.google.com
Ironport-phdr: 9a23:SJZMpxOEJOlxXlfqJqAl6mtUPXoX/o7sNwtQ0KIMzox0Lfr+rarrMEGX3/hxlliBBdydt6sYzbWK+Pm9BiQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vIxi6twfcu8YZjYd/Kqs8yAbCr2dVdehR2W5nKlWfkgrm6Myt5pBj6SNQu/wg985ET6r3erkzQKJbAjo7LW07/dXnuhbfQwSB4HscSXgWnQFTAwfZ9hH6X4z+vTX8u+FgxSSVJ8z2TbQzWTS/86dmTQLjhSkbOzIl9mzcl8p9h79Zrh28vRxy24HbYI+XO/R+cK3Tfs4US3RdUctKTSNNHpmxYpETA+YdP+tVqZT2qVsUrRu5AAmhHOfhxSVThn/x260xzuUvERvB3Aw7BNIFrXPZrNfvO6cJVuC1yqbIzS/Eb/NNwjfw7JPFch8kof6WXLJwddDdxlUoFwPAl1idr5HuMT2S1uQIqWeb7uxgWPqgi24mtwFxoiWvydw2hobVgYIVz1bJ/jh6zoYtPdC0VlJ3bNq+HJZTtyyWLZV6Tt8hTm1ytys217sLsoOhcicQ0pQo3RvfZuSHc4eW5hLjU/6cITJii3JkfLKzngi9/lW9xuHlWMm530tGojBKktnLsXAN2BjT5dadRvRh+Ueh3C6D1wHV6u5aPUA5jbTXJ4Ilz7IqlZcesV7PEjHqlEj1lqObeVgo9vCt6+v9Y7XmopGcN5VzigH7KqkumNawAf8/MggIUGib4+O81Kb4/UD9W7hKgfg2nbPYsJDeP8gUuqm5AwpN3oY59xm/Fyum0MgfnXQfMF1FfwuHg5H1NFHKPfD3Fuyyg0+skTdu3/DJJKftApTLLnjZkbfuZ6xx60BGyFl78dcK7JVNT7oFPfi7DkT2rZnTCgIzGw2y2efuTttngNAwQ2WKV42QK6TU+XCS4fk0a72ObZQSvjnnLOM+ttbhiHY4nRkWeqz/jshfU2yxAvkzexbRWnHrmNpUST5X7Dp7d/TjjRi5aRAWZ3u2WPhhtDQyCYbjAIuaA47x2fqO2yC0GpAQbWdDWAjVQCXYMr6cUvJJUxq8Z8pokzgKT7+kEtZz2hSntQu8wL1ifLONpn8o8Kn73d0w3NX90Ako/GUtXcuY2mCJCWpzmzFQSg==

The fiat-crypto-legacy code also probably counts (https://github.com/mit-plv/fiat-crypto/tree/sp2019latest ), cf https://github.com/coq/coq/pull/11494

On Sun, Feb 16, 2020, 17:09 Jason Gross <jasongross9 AT gmail.com> wrote:

I think fiat-parsers might count https://github.com/mit-plv/fiat/tree/master/src/Parsers

On Sat, Feb 15, 2020, 20:28 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