Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] [isabelle] Abandoned proof engineering efforts

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] [isabelle] Abandoned proof engineering efforts


Chronological Thread 
  • From: "Fernandez, Matthew" <matthew.fernandez AT intel.com>
  • To: Stephan Merz <stephan.merz AT loria.fr>
  • Cc: Talia Ringer <tringer AT cs.washington.edu>, Coq-Club <coq-club AT inria.fr>, isabelle-users <isabelle-users AT cl.cam.ac.uk>
  • Subject: RE: [Coq-Club] [isabelle] Abandoned proof engineering efforts
  • Date: Tue, 18 Feb 2020 17:24:20 +0000
  • Accept-language: en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=intel.com; dmarc=pass action=none header.from=intel.com; dkim=pass header.d=intel.com; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=OEYL5eO4Hw6967dsSMhwfrEp3xYPdWrDApYmKhZwRV8=; b=kwj+/lMIRUtavnbdWIr9zsqkuBG0cvq2BesZCQM0oCL51dF4xifY/GAmsvEjvBQy4GgMGYZCd+k8d4NBThdcIzKM87rfNYAYaSwPwSB7DcTzXo46ezKxMhjryWqdNn38WIJtCCejpQrUOKEwqiccB6JGEVdtTcOeVbmydPdj2rPxibaO9rfZLy/y+Ucy3Sosmo3Jt4kor/7pCEE4PWnp7L2gsgwJbQyjthzDof8qifyBEBjsruSWqIPpDydmwaxFnDaIikNaLgpK53H9wIbOIVp9h8dm1M/cqH8F7wQM5SJWCTxYoyhSLlKIJdJz3o188zPLa4RxFgfTEvaJl4BNkw==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=Pn/IY1kjz4OXN+1B+ra13wjsL0tzT3VY9H8zXktvrgUl6p9pWBLuS5MbVJnd/6cQjX3+Kq8/4d7A+tSlvau9FHgamejFx4UH1z5oc8+b6f2xpqB84EoiD7rBoYnqahIq9SCHMnqzjnH+1sfgFRUYHNEVbDlhCArj1YAbJLwO9CKF79m/ziPqr/Oz6wjVpbMIZ1UGcfsWjFuBfg1HRCSjcWVufiIIOHjKaxg5M4wYpcML7+8fire4v//tgoF7OvyyBA08GsEqbbgz5s1HitSRD+vF8wK/6L1yQCshbzMMciMXS348vWb3A4ba70eLdIQtSnKQEcRXupBKUYdSTPdZkw==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=matthew.fernandez AT intel.com; spf=Pass smtp.mailfrom=matthew.fernandez AT intel.com; spf=None smtp.helo=postmaster AT mga06.intel.com
  • Dlp-product: dlpe-windows
  • Dlp-reaction: no-action
  • Dlp-version: 11.2.0.6
  • Ironport-phdr: 9a23:6whu5xfOiarBg+LtYw+d1+A0lGMj4u6mDksu8pMizoh2WeGdxcW+YR7h7PlgxGXEQZ/co6odzbaP7+a/CSdZuc7JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sArcutMUjIZhJao91wfFrmdVcOlK2G1kIk6ekBn76sqs5pBo7j5eu+gm985OUKX6e7o3QLlFBzk4MG47+dPmuwDbQQSA+nUTXGMWkgFVAwfe9xH1Qo3xsirhueVj3iSRIND7Qqo1WTSm6KdrVQPohSIaPDM37G3blsp9h79ArRm/uxJw3ZLbYICNNPp/YKzde88aRXFcVcpVTiBNH5+wY5cKA+cHIO1WrZTyp0EWoBW+GweiGf/vxDFLiH/436I60vguHw7J0wE7A9IOqWjYoMnpOKsOT+y4yrTDwzXZb/NR3Dfw8IbEfBA/rvGWW7J/a8zRxlQxGALEllmbtIvrMCmJ1uQRs2iU8eRhWeyygGMgrgF+uCSvxtssiobXiIMZ0F7E+jtjwIYzP9K4TlN0bsClEZZLtiGaMZd2Td0mQ21ypCk6zbgGtIe9cSMXxponwBvfZOaGc4iO+h/jW+eRISt4hHJ4Y72znQq98U+lyuD6S8K6005KozJYntTCuX0BzQHf58aIR/dn40us1zeC2xrd5+1ZOUw4iKTWJpE7zrItmJcevl7PEjL4lUj3lqOaaFgo9+iw5+TpfLrrpYOQOopxhw7jKasjlcmyDOYkPQUOXWWW/OCx26P98kD2RbhFkOc5n6vfvZvHP8oUvLS5DBVQ0os76xawETOm0NMAkHkCI1JKYg6LgonzN1HPJvD4Eemwg1C2nDh3wPDGO6XtApTLLnfdjLfsZatx5kBTxQYp0NxS6Z1ZBqscLP/9W0L9rtLVAgIhPwyx2ennCdF91o0EWWKIB6+UKKbSvkWU5uIzI+mDeoEUtCzzK/c7/f7ui2U2mVkAcqa33Joac3G4HvJ6I0qHZXrgmMsOEWAPvgYmVuzllEWCUSJPZ3a1R68z+jY7CJu/AYjfQoCtnaeO0TygHpxWY2BGEkqDHW3pd4WCQfcMaTidLtVvkjweBvCdTNoayRy2tAb8g59qNPicrjYEuIrj3d4z4uDJhzk28iZ1BoKTyTfeYXtzmzZCaTIs2ql5rUFvjh+m2LRkg/FHX5QH4vpVTgc3KtjSwvZ8Atb+VxDpf9GVRVLgSdKjV2JiBuktysMDNh4uU+6piQrOim/zW+dMy+67Qacs+6eZ5EDfYt5nwi+fhqgnk1QiBMBIMD/+3/8tx03oH4fM1n6hueOvfKUY0jTK8T7an2uIoExcFgV3VPecBC1NVg7ttd38o3j6YfquBLAga1QTzMGLcvUMa9v1gFEAT/DmaozT
Yes, I was not meaning to imply otherwise. Merely that I don't recall the
reason why they moved away from ITP. You can see the Isabelle pieces under
cluster/isabelle in the repository.

> -----Original Message-----
> From: Stephan Merz
> <stephan.merz AT loria.fr>
> Sent: Tuesday, February 18, 2020 09:21
> To: Fernandez, Matthew
> <matthew.fernandez AT intel.com>
> Cc: Talia Ringer
> <tringer AT cs.washington.edu>;
> Coq-Club
> <coq-club AT inria.fr>;
> isabelle-users
> <isabelle-users AT cl.cam.ac.uk>
> Subject: Re: [isabelle] Abandoned proof engineering efforts
>
> A short look at the GitHub repository seems to indicate that they moved to
> model checking. Although an interactive proof system for TLA+ does exist, I
> couldn't see any proofs in their modules.
>
> Stephan
>
> > On 18 Feb 2020, at 18:13, Fernandez, Matthew
> > <matthew.fernandez AT intel.com>
> wrote:
> >
> > Some of the Elasticsearch algorithms have been verified using TLA+ [0]. In
> that repository is also a partial Isabelle formalization of the same. I had
> a
> conversation with David Turner about why they moved away from Isabelle to
> TLA+, but can't recall the exact details and motivation offhand. This might
> be
> an interesting case study for you though, Talia.
> >
> > [0]: https://github.com/elastic/elasticsearch-formal-models
> >
> >> -----Original Message-----
> >> From:
> >> cl-isabelle-users-bounces AT lists.cam.ac.uk
> >> <cl-isabelle-users-
> >> bounces AT lists.cam.ac.uk>
> >> On Behalf Of Talia Ringer
> >> Sent: Saturday, February 15, 2020 17:27
> >> To: Coq-Club
> >> <coq-club AT inria.fr>;
> >> isabelle-users
> >> <isabelle-users AT cl.cam.ac.uk>
> >> Subject: [isabelle] Abandoned proof engineering efforts
> >>
> >> 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


Archive powered by MHonArc 2.6.18.

Top of Page