LMF2017: Lógica y programación
En la primera parte de la clase de hoy del curso Lógica matemática y fundamentos se han comentado algunas relaciones entre la lógica y la programación.
En primer lugar, a partir del artículo The Curry-Howard correspondence between programs and proofs se han comentado cómo los tipos se corresponden con las fórmulas y la existencia de funciones de un tipo dado se corresponde con la veracidad de su fórmula.
Como lectura complementario se ha recomendado el artículo El isomorfismo de Curry-Howard y una introducción a Coq.
Para analizar la distancia del lenguaje matemático a los de programación, se ha comentado el artículo From math to machine: translating a function to machine code que partiendo de la definición matemática del factorial expica su representación en un lenguaje funcional (Haskell), en uno imperativo (C), en ensamblador y en código máquina.