Escribir código dependiente que lleve pruebas es generalmente más fácil en Agda, porque tiene buenas instalaciones para el análisis de casos dependientes y usa Axiom K internamente, por lo que la igualdad heterogénea no es algo con lo que tenga que luchar en un nivel bajo (es decir, cuando el tipo de dos cosas es igual “hasta algunas reescrituras triviales”).
Coq es bueno cuando usa tácticas para automatizar grandes pruebas mecánicas, como el análisis semántico, donde a menudo se deben descargar numerosos objetivos secundarios que no son interesantes para la pregunta en cuestión, en forma de ramas en el árbol de sintaxis.
Dicho esto, uso Coq para muchas cosas y Agda para ninguna, por lo que también puede depender del proyecto que tenga en mente, qué teorema demuestra que usan sus colegas y quién será su audiencia final.
- ¿Qué es un número ruso de Doll Prime?
- ¿Cuál es la gráfica de | z + (1 / z) | = 2?
- ¿Cómo se puede explicar la propiedad de agrupación de la multiplicación?
- ¿Son los árboles B y B + un truco?
- ¿Cómo es la especialización en ACME en BYU?
Nota: La biblioteca recientemente actualizada [Coq-Equations] (mattam82 / Coq-Equations) hace que el código de estilo Agda sea posible escribir convenientemente en Coq. Lo he estado usando en algunos proyectos ahora, y hace que la programación de tipo dependiente de ese tipo sea mucho más natural.
