Type-driven Development with Idris
Edwin Brady
- Editorial
- Manning
- Año
- 2017
- Páginas
- ~480
- Nivel
- Intermedio
De qué trata
Tratado revolucionario escrito por Edwin Brady (creador del lenguaje Idris) y publicado por Manning en 2017. Introduce el desarrollo guiado por tipos (Type-Driven Development) y los tipos dependientes en la programación práctica.
Explica cómo los tipos dependientes permiten que los tipos dependan de valores, posibilitando verificar matemáticamente en tiempo de compilación que los programas cumplen con sus especificaciones exactas (por ejemplo, que una función de ordenamiento devuelve una lista con la misma longitud y elementos ordenados).
El autor enseña a utilizar el comprobador de tipos como un asistente interactivo que escribe código junto al programador, diseñando máquinas de estado seguras y protocolos de red verificados. Una de las obras más inspiradoras de la ciencia de la computación moderna.
- Idris
- Tipos Dependientes
- Type-Driven Development
- Edwin Brady
- Verificación Formal
- Máquinas de Estado
- Manning
¿Cómo enseña?
Teoría + práctica
- ✓ Incluye ejercicios
- ✓ Incluye proyectos
Proyectos
Máquina de Estados de Protocolo de Red Verificada Formalmente
Modelado de un protocolo interactivo en Idris donde el compilador garantiza que es imposible enviar datos en un estado de desconexión.
