The Coq mailing list

[Erik Martin-Dorel <e.mdorel AT gmail.com>]

Hello,

Le mer. 1 déc. 2021 à 22:58, Timothy Carstens <intoverflow AT gmail.com> a écrit :

Do you have an opinion on how to style Coq code/projects?

[…]

* Do you know of any other good Coq style guides or similar resources?

I'd say a must-read is Mathematical-Components' style guide; AFAIK the corresponding reference URL is this one:

https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md

* Do you have any other relevant thoughts/comments/suggestions that you'd like to share?

Generally speaking the naming convention (for functions and lemmas) seems paramount for proof-assistant developments,

so I guess it should always be a key component of any proof-assistant style guide.

I can mention some articles on this very issue, focusing on automatically learning and suggesting lemma names:

- Deep Generation of Coq Lemma Names Using Elaborated Terms

  [Nie, Palmskog, Li, Gligoric: IJCAR 2020], https://doi.org/10.1007/978-3-030-51054-1_6

And an earlier article, focusing on HOL Light developments:

- What’s in a Theorem Name?

  [Aspinall, Kaliszyk: ITP 2016], https://doi.org/10.1007/978-3-319-43144-4_28 & http://cl-informatik.uibk.ac.at/workspace/publications/ITP16-DACK.pdf

Best regards,

Erik

Kindly yours,

-t

Why adopt a style guide?

Everyone who interacts with code is impacted by code style. This clearly includes the project’s contributors, but it also includes other interested parties such as users and upstream maintainers. In other words, style is relevant to many different roles and personas engaged in many different use cases.

A style is “good” if it has a net-positive impact on those use cases.

Good style does not arise by accident; rather, it is engineered by carefully considering how different idioms & practices impact different use cases.

This is a lot of work to get right. Therefore, many projects adopt a style guide - either in full, or as a starting point for their own style.

What does a good style guide look like?

* The Google C++ Style Guide: https://google.github.io/styleguide/cppguide.html

* Awesome Guidelines: https://github.com/Kristories/awesome-guidelines

How does this relate to Requirements on the Use of Coq in the Context of Common Criteria Evaluations?

Requirements on the Use of Coq in the Context of Common Criteria Evaluations is a requirements document published by ANSSI and INRIA. While most projects are unlikely to be used in a Common Criteria Evaluation, the guidance offered by this document is valuable in other contexts as well.

With respect to coding style, the document says:

    There is no well-established coding style for Coq development. The present document does not attempt to fill this gap, but rather to identify and discourage known bad practices.

This style guide aims to fill this gap.

--

Érik Martin-Dorel

http://erik.martin-dorel.org/