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: 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:13:28 +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=0h57D6z2b6/bHbnwwlui5hlYCrHZwZm2y0KGuCk+PqA=; b=klsJY0ndQNNlyhDR4YEgUcIsCaFZzS1H9syFOZ4B1K3hA7YIdI0n0OTBLXbyb3OToOdTTRAWwjZAC/QLoTgOstWMsBNLuZbWxGN0pQWUggzfpeTyMm+/jvGwoDkrRfWrXR6pAYUKPwtxwCjKUhlcrdsaoTkYogkMBJAu5lR2WrHDQtaupq2wcdXZVQt6FTCR16RENePXNZOaPijsvLMEGWN3DQxB/8gg5w0qE43PgXIWcplpe9jZ7Ky3Ny2u7p1NnVetwDv8HCuObLsoAeMnzzWFD7ltCmqeEMQfGwCFlkpGaDvNm2n1wOd9L4TdJZYmHEbh74sjx5y35JKe+J4M6w==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=Nn3EjTZCy18fBMe+K3B39U1efkAR0aOv6T+IjnZzhGsaVrbnnlvFV58KtYwji463Rb1IIgS5rug1+3xlCpbT59srMLNIwLzWqV5Hb52ee6O0VlJWr/DZ+0UuT9n5QXI9MX5rQjDRItYvJIlNk+bER/cpNQx/NXcI49CgydfhgsXMIQVD0c21l4PI2kskQESK1UhbtSI5Mafu5YJqHdvFwyDAicagzRTHPno9nu4yr2m8d03FvWRtDmGJcEFvNB/c9LYGBL4adMsWKwFLlOYFgMenVfeDPa/ivbTqN257HWshpQIWH3uEj6x1xQ+CS6sRC4M8lKNStzrXcnApUkyYFw==
  • Authentication-results: mail3-smtp-sop.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 mga17.intel.com
  • Dlp-product: dlpe-windows
  • Dlp-reaction: no-action
  • Dlp-version: 11.2.0.6
  • Ironport-phdr: 9a23:ugYZbRGKbnJ57ooxH9OyOJ1GYnF86YWxBRYc798ds5kLTJ76p82ybnLW6fgltlLVR4KTs6sC17OK9f+wEj1Qqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi5oAnLtMQbgoRuJ6IyxxDUvnZGZuNayH9nKl6Ugxvy/Nq78oR58yRXtfIh9spAXrv/cq8lU7FWDykoPn4s6sHzuhbNUQWA5n0HUmULiRVIGBTK7Av7XpjqrCT3sPd21TSAMs33SbA0Ximi77tuRRT1hioLKyI1/WfKgcFrkqlVvAyuqAB+w47MYYGaKvx+fr/GfdgHQWZNR9tdWzBdDo+5aYYEEugPMvtCr4Tlp1UAswawBRWiCu3sxD9HhH720rE13esuCgzGwBcvE84SvHjIsNn4NqEfWv21wqnSyjXDautb1Tn95ofWaBAhp+uDXbRtfsXPyEgjDx7OgFKKpoz5IzOV1voCsmaV4+F9Uu+vjnQoqx1tojiv2MgthJPFhowLxVDe8yV22oA1KsCmR096etOkEZ1Qtz2EOItyWM8tX2ZouCMjx7AApJW1ci8KyJE9yB7ebfyKa4eI4hP/VOaRPDd3n2hpd664hxa390Wr1+7yVtGs3VpXqidJjMPAu3AN2hDJ6sWLVOFx8lqh1DqSzwzf9+9JLE8umabGJZMszaQ8mocdvEnCBCP6hlj6ga+OekUq5Oel6Pjrb7Djq5CBLIB5hQTzP6YylcG/A+k1NwwDUHaF9umz0bDs41f2TbdMg/YriKfWqoraKt4epqOhAw9azIIj6xGnAjej39QXh2QLIVBfdBKGiYjpJ0/BIPTiAfijhFSslS9nx/HAPrL/HpXANmXPnbP/cbpn60NRyBA/wNBB655OF70MIO//Vlf0tNPCDx85NwK0w/zgCNV4zo4eXHiAArOFMKPSr1CJ6PgjI+eSa48PvjbyMf4l6OPwgn44glIdfK+p3YcJZ3C8BPhpP0KZYX/0jtcbDWgKphY+TPDtiFCaTTFTYG+yU7sg6TE/FYKpFpzORputgbyExCe0BIdaZmFAClCWEHfnbZ+IW/kWaHHaHsg0rjUAVLHpcY4n2hy0/Fvm0bthIefO0iYD843qz9h04eLPkhd0+DBpWYDV+GaUCkpwg2lAEzQxxeV0pVF34laFy6lxxfJCQ5gb5uhAWAo+MZOZ0vd3Ecu6DgPad92ETFKrB8i9DCsqZtk1hdQHZgB0EJO/jUaQ8TCtBupfubGRApUy/q/OmzDULtphy3vZnuF1ilA6XstCKiuoi7R5/g7fCpzhkkOFmqLsfqMZin2evFyfxHaD6RkLGDV7Vr/ICDVGPhOP/IbJo3jaRrrrMowJdw5IyMqMMKxPM4S7jFNaSfOlM9PbMTvoxzWAQC2Qz7bJV7LEPn0H1XyEWkkCjw0Xu32BMFpmX3rzkyflFDVrUGnXTQbs/O158SzpS0A9ll7Mbkt92r7z8RkQ16SR
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