The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Aaron wrote:
> As a prerequisite for such improvement, it seems critical to develop
> an official, written, agreed-upon style guide that is as thorough and
> detailed as possible (*).  The library code should (obviously) follow
> the style guide and be a perfect model for how users should write
> their own code.
>
> (*) The style guide should cover the parts of the Coq code that can be
> seen when looking through a library's coqdocs, i.e., the Gallina and
> generic tactic definitions.  A style guide for proof scripts would be
> a whole other can of worms and seems much less urgent.
>

While I agree that such a style guide is crucial, I think that, at the
moment, no one can tell whether, e.g., a partial function should
return an option, or a default value. Moreover, writing the guide
lines on how to write perfect code can take an infinite amount of
time. Thus, I think there should be a compromise between the amount of
guidelines that are set up before starting the project, and the
necessity to start the projet to see what kind of guidelines are
required. Maybe I am wrong, but I do not think people are planning to
write guidelines at the moment. However, kickstarting a repo of open
contributions may spark the writing of such guidelines.

Frederic wrote:
> But I don't think we need to worry too much about backward compatibilities 
> with old contributions or the current standard lib, because we can simply 
> use new name spaces.

Indeed, a good way to ensure backward compatibility would be to tag
stable releases of the current ext-lib (or to resort to module to tame
the name-spaces).

Thomas