The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Talia,

  You maybe know about it already, the recent book on mathematical components goes a lot into proof methods and the framework behind the library, and is meant to be accessible to the newcomer:

  https://math-comp.github.io/mcb

  Apart from that, stackoverflow contains some folk knowledge, as does this very mailing list. Of course CPDT also advocates its so-called Chlipala-style, based on dependent types and automation. And Software Foundations kind of gets a style across as well, but more suited to education than maintainance I believe. There might be other projects with a formulated "style"-guideline addressing proof engineering issues. The HoTT library has a set of guidelines for example: 

  https://github.com/HoTT/HoTT/blob/master/STYLE.md

  Just of the top of my head, TLC by Arthur Charguéraud also has a style guideline. For less "standard" libraries, the relational algebra library by D. Pous employ a mixed typeclass - canonical structure approach that has proved very effective:

  https://perso.ens-lyon.fr/damien.pous/ra

  I'm very happy to learn that you are looking into this subject, which from my viewpoint always looked rather scary and ginormous, but I didn't have your tool to even start thinking of tackling the problem! If you look at the Coq contributions for example, you'll see that each one uses a different style (apart from the few following, e.g. mathcomp's or Chlipala's style). There is work on proof refactoring that Hugo Herbelin and Bruno Barras developed for the 7 -> 8 transition that implemented a beautifier allowing to do systematic translations of term syntax and proof scripts, that is still part of Coq, I guess you might be interested in looking at this as well.

  Isabelle does have at least one style guide, I guess you should ask on the Isabelle list for their take on proof engineering:

  http://proofcraft.org/blog/isabelle-style.html

Best (of luck!),

-- Matthieu

On Wed, Jan 17, 2018 at 3:49 AM Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

Nice idea. I don't have specifics to offer. Just a vague intuition that concepts of architecture and of design patterns might be worth thinking about. Kevin

On Jan 16, 2018 18:46, "Talia Ringer" <tringer AT cs.washington.edu> wrote:

Hi all,

I am writing a survey paper on proof engineering, and one of the topics is about design principles and frameworks (which often go hand-in-hand).

I'm already aware of a lot of work in this area (planning for changes, writing good automation that is resilient to changes, deep specifications, and principles and frameworks that address problems within certain domains like mechanized metatheory). However, I'm curious if anyone has any useful pointers, especially for folk knowledge -- the kind of thing I might not find looking through old papers, but that everyone who writes proofs about real systems knows and applies in practice.

Of course, if you have papers you'd like to point me to, that's also welcome, since it helps to know if I've missed anything obvious. This doesn't have to be specific to Coq; please feel free to send me something related to other proof assistants like Isabelle. It is particularly interesting to see what exists within one proof assistant but not within another, and whether that is fundamental or simple due to a lack of tooling.

Thanks for all of your help,

Talia Ringer

University of Washington
http://tlringer.github.io/