A usage poll for the Coq proof assistant

Coq developpers recently put together a survey of their tool usage, which will hopefully inform future evolutions. From Matthieu Sozeau's announcement:

On behalf of the Coq developers, I’d like to invite everyone to respond to a survey on their usage of Coq, its programming and proving environment, development model, shortcomings and future directions. This survey aims at gathering important information about Coq's users and uses. The results will be used to better understand users' needs, and help decide in which direction Coq’s development should go. It is really important for us to get as many answers as possible before * January 15th 2014 *. We are also taking this occasion to collaboratively build a bibliography of Coq-related papers. The survey’s results will be synthesized, anonymized and made publicly available in february.

The estimated burden time for this survey is around 30 minutes. The survey is available online at:


This survey was mainly prepared by Thomas Braibant, assisted by Enrico Tassi, thanks to them for giving us all an occasion to take a step back and reflect on Coq’s future.