Да не. Так-то, сделать удобства типа того же хаскелевого IO, библиотеки, и уже вполне можно было бы "промышленно" программировать на Coq. Но мне больше нравится Agda. Но в Coq с доказательствами лучше. Хоть мне и не нравится способ, которым они сделали улучшения.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2009-06-20 02:28 pm (UTC)Так-то, сделать удобства типа
того же хаскелевого IO, библиотеки,
и уже вполне можно было бы
"промышленно" программировать на Coq.
Но мне больше нравится Agda.
Но в Coq с доказательствами лучше.
Хоть мне и не нравится способ,
которым они сделали улучшения.