coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Stephan Merz <stephan.merz AT loria.fr>
- 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: [Coq-Club] [isabelle] Abandoned proof engineering efforts
- Date: Tue, 18 Feb 2020 18:21:17 +0100
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
- [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
- Re: [Coq-Club] [isabelle] Abandoned proof engineering efforts, Stephan Merz, 02/18/2020
- Re: [Coq-Club] Abandoned proof engineering efforts, Talia Ringer, 02/16/2020
Archive powered by MHonArc 2.6.18.