Solo Haskell: lo mejor es lo funcional

Agda es un lenguaje de programación funcional con tipado dependiente. Donde los tipos pueden depender de valores, lo que permite expresar invariantes directamente en el sistema de tipos. Es una extensión de la teoría de tipos de Martin-Löf y representa el desarrollo más reciente de lenguajes creados en el grupo de lógica de programación de Chalmers. "Gracias a su fuerte tipado y a los tipos dependientes, Agda puede utilizarse como asistente de demostración, lo que permite probar teoremas matemáticos (en un entorno constructivo) y ejecutar dichas pruebas como algoritmos". Además de programar, puedes demostrar teoremas y verificar que tu código cumple propiedades matemáticas. Se usa principalmente con Emacs, que ofrece asistencia paso a paso para escribir programas y pruebas. La similitud con Haskell coniste en compartir la orientación funcional, pero Agda va más allá al integrar la lógica formal en el lenguaje. Comparativa con Haskell Obse...