The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

No comments on particular styles (different Coq communities have radically different styles, but I do agree with guides within projects). But in QED at Large, I talk about existing style guides for proof assistants, which you may find interesting:  https://arxiv.org/abs/2003.06458

On Wed, Dec 1, 2021, 3:58 PM Timothy Carstens <intoverflow AT gmail.com> wrote:

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

I'm currently working on assembling a style guide for Coq projects. The goal is to provide clear recommendations that are informed by experience and guided by relevant use cases. I've included a brief FAQ at the bottom with more information.

The project is still in its infancy. I want the output to be relevant to you so I am reaching out to ask:

* Are you interested in joining this effort? It would be great to put together a small group of people who can help set the goals & manage the execution of this project.

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

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

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.