The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Let me just add my brief advice to, before any introduction of explicit 
dependent typing anywhere in a Coq development, pretend like you need to 
submit a pile of permission forms to a bureaucracy and wait six months 
for a lengthy review process.  It usually is a net negative for the 
project.  Length-indexed lists are on the "promising" side of the 
spectrum, but still they're often a bad idea.  At least, that's my 
aggregated instinct after ~20 years of experience working on Coq 
projects with collaborators all along the spectrum of experience with 
the tool.