Да не.
Так-то, сделать удобства типа
того же хаскелевого IO, библиотеки,
и уже вполне можно было бы
"промышленно" программировать на Coq.
Но мне больше нравится Agda.
Но в Coq с доказательствами лучше.
Хоть мне и не нравится способ,
которым они сделали улучшения.