The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On 2011-03-09, Aaron Bohannon wrote:
> I would love to see improvements/extensions to Coq's standard library.
>  As a whole, it seems to be in rough shape.
> 
> 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. 
> <...>

I certainly think that this is a laudable goal. I worry however, that
this sets that bar too high. Certainly, there should be style
guidelines, and the should be ahered to. I think that requiring that the
library be a oerfect model would discourage many potential contributors.
And I think that any definition of perfect is going to vary, over time,
as the features provide by Coq change and improve.

I can't write perfect code, and I don't think I would be qualified to
judge code perfect. I think that a better criterion would be, at least
as good as the standard library, perferably better.

On a differnt tack, I wonder how much potentially generally useful code
is written for one off task or projects, and then is forgotten about. I
think there is value in collecting these snippets, and improving upon
them. The coq-contribs repository does the first part of this,
collecting the code. But to my knowledge, aside from the few
contributions that are still being actively developed by outside groups,
the code is static (barring compatibility updates).

Also, there is the issue of compatibility. There needs to be a balance
between improving the library, and supporting code that worked against
older versions. It wouldn't surprise me if a number of the perceived
deficiencies of the standard library are due to the requirement to be
backwards compatible. I think to a certain extent, both the goals that I
outlined above run counter to maintaining backward compatibility. I
don't think this is an insurmountable challenge, but certainly, at
points it will lead to non-perfect code.

  Tom Prince

P.S. In case it wasn't clear from my rambling, I am in support of some
sort of ExtLib.