Programación funcional verificada en Agda

Opiniones de los lectores

Las reseñas del libro destacan su accesibilidad y su enfoque práctico de los tipos dependientes utilizando Agda, subrayando su idoneidad para principiantes a pesar de algunas deficiencias en claridad y organización. Aunque muchos lectores lo encuentran excelente para aprender Agda y la demostración de teoremas, hay críticas sobre su estructura, claridad y presentación, particularmente en la versión Kindle.

⬤ Introducción accesible a los tipos dependientes en entornos prácticos utilizando Agda.
⬤ Prepara a los lectores para material más avanzado sobre teoría de tipos y demostración de teoremas.
⬤ Contiene un buen número de demostraciones sencillas y ejemplos prácticos.
⬤ Adecuado para lectores sin conocimientos previos de lógica o teoría de tipos, aumentando el alcance de su audiencia.

⬤ Carece de cobertura teórica de tipos dependientes.
⬤ Algunas secciones no enfatizan los conceptos generales antes de entrar en detalles.
⬤ Problemas de claridad en las explicaciones y organización de los capítulos; algunos puntos se repiten demasiado mientras que otros no se explican adecuadamente.
⬤ La versión Kindle tiene un diseño deficiente, con una sangría de párrafo inadecuada y problemas de alineación con el código fuente.

(basado en 4 opiniones de lectores)

Título original:

Verified Functional Programming in Agda

Contenido del libro:

Agda es un lenguaje de programación avanzado basado en la Teoría de Tipos. El sistema de tipos de Agda es lo suficientemente expresivo como para soportar la verificación funcional completa de programas, en dos estilos.

En la verificación externa, escribimos programas funcionales puros y luego escribimos pruebas de propiedades sobre ellos. Las pruebas son artefactos externos separados, típicamente usando inducción estructural. En la verificación interna, especificamos las propiedades de los programas a través de tipos ricos para los propios programas.

Esto a menudo requiere incluir pruebas dentro del código, para mostrar al verificador de tipos que las propiedades especificadas se mantienen. El poder de probar las propiedades de los programas en estos dos estilos es una profunda adición a la práctica de la programación, dando a los programadores el poder de garantizar la ausencia de errores, y por lo tanto mejorar la calidad del software más de lo posible anteriormente. Verified Functional Programming in Agda es el primer libro que proporciona una exposición sistemática de la verificación externa e interna en Agda, adecuada para estudiantes universitarios de Informática.

No se presupone ninguna familiaridad con la programación funcional ni con las pruebas verificadas por ordenador. El libro comienza con una introducción a la programación funcional a través de ejemplos familiares como booleanos, números naturales y listas, y técnicas para la verificación externa. La verificación interna se considera a través de ejemplos de vectores, árboles de búsqueda binarios y árboles de Braun.

También se incluye material más avanzado sobre computación a nivel de tipo, razonamiento explícito sobre terminación y normalización por evaluación. El libro también incluye un caso práctico de tamaño medio sobre la codificación y descodificación Huffman.