The Coq mailing list

[Jan Bessai <jan.bessai AT tu-dortmund.de>]

Talia,

during my PhD I rewrote my proofs at some point. The old implementation
is still online:

https://github.com/combinators/cls-coq/tree/old_version

Reasons were:
- The Coq Module System was too complicated for me to deal with
- My proofs didn't work well with extraction because of sigma-types
- I simplified the type theory these proofs are about
- SSReflect+Mathcomp was a more appealing style to do proofs in

The new system is in the master branch of the same repository. Both are
around 15-20k lines of Coq.

-- Jan

> -----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

-- 
Dr. Jan Bessai
Wissenschaftlicher Mitarbeiter

Technische Universität Dortmund
Fakultät für Informatik - Lehrstuhl 14 Software Engineering
Otto-Hahn Straße 14
D-44227 Dortmund

Tel.: +49 231-755 77 64
Fax: +49 231-755 79 36
jan.bessai AT tu-dortmund.de
www.tu-dortmund.de


Wichtiger Hinweis: Die Information in dieser E-Mail ist vertraulich. Sie
ist ausschließlich für den Adressaten bestimmt. Sollten Sie nicht der
für diese E-Mail bestimmte Adressat sein, unterrichten Sie bitte den
Absender und vernichten Sie diese Mail. Vielen Dank.
Unbeschadet der Korrespondenz per E-Mail, sind unsere Erklärungen
ausschließlich final rechtsverbindlich, wenn sie in herkömmlicher
Schriftform (mit eigenhändiger Unterschrift) oder durch Übermittlung
eines solchen Schriftstücks per Telefax erfolgen.

Important note: The information included in this e-mail is confidential.
It is solely intended for the recipient. If you are not the intended
recipient of this e-mail please contact the sender and delete this
message. Thank you.
Without prejudice of e-mail correspondence, our statements are only
legally binding when they are made in the conventional written form
(with personal signature) or when such documents are sent by fax.