Lógica para Programadores: Diseña, Verifica y Razona Mejor sobre tu Código
Logic for Programmers
Escribí este libro para que los programadores intermedios y avanzados mejoren el diseño y la verificación de software usando lógica booleana. No necesitas conocimientos matemáticos previos, solo experiencia práctica con loops y testing. Explico cómo aplicar técnicas como property testing, contratos y verificación formal con herramientas como Dafny, Alloy y TLA+ para resolver problemas reales desde simplificar condicionales hasta encontrar race conditions.
Si all([]) fuera False, entonces all(xs) sería False sin importar qué sea xs, por lo que tiene más sentido que sea True para preservar la propiedad de identidad.
- rmunn
Cuando estaba en la universidad, tomé algunas clases de filosofía solo por diversión. Descubrí que cuando cursé Lógica Simbólica, mientras todos los demás luchaban con la clase, yo la encontraba bastante fácil, porque encadenar una demostración en lógica simbólica se sentía exactamente como programar. Eran los mismos pasos mentales: tienes las condiciones iniciales, hay un punto final al que quieres llegar, y necesitas encadenar estas operaciones fundamentales para llegar allí. (Y a veces necesitabas ver cómo descomponerlas: si necesitas demostrar P Y Q, entonces demostrar P por separado y demostrar Q por separado solían ser pasos más fáciles, y una vez que has demostrado P y has demostrado Q, entonces has demostrado P Y Q. Lo cual se sentía mucho como refactorizar una función grande que hacía dos cosas en dos funciones separadas y más pequeñas que hacen una cosa cada una).
Al revisar el capítulo de muestra, me recuerda a mi experiencia con la clase de lógica simbólica. Parece que será exactamente lo mismo, pero dado la vuelta: en lugar de saber programar y usar ese conocimiento para hacer la lógica simbólica más fácil, esto parece que será sobre saber lógica simbólica y usar ese conocimiento para hacer la programación más fácil. Parece bastante útil; le daré una lectura más profunda a los capítulos de muestra pronto.
- js8
Parece un buen libro, pero.. siento que ningún trabajo serio con esta ambición hoy en día debería omitir (quizás esté presente, no estoy seguro por el índice) la isomorfismo de Curry-Howard, proposiciones-como-tipos, y de ahí la analogía entre lógicas y cálculos lambda.
Realmente me gusta esto: https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard....
Creo que todo programador debería entender las consecuencias del CHI para la disciplina, que son profundas. Significa que no hay necesidad de una lógica clásica como metalenguaje separado, las propiedades de los programas también podrían expresarse en el lenguaje de programación de tu elección. Además, muestra que "ejecutar el programa" y "razonar sobre el programa" son en última instancia los mismos procesos, lo cual plantea algunas buenas preguntas filosóficas sobre las pruebas, por ejemplo. Pero también sobre cómo podemos abordar el diseño del programa, quizás podamos simplemente "calcularlo" a partir de las restricciones. También nos abre a cosas como la supercompilación.
Creo que la disciplina necesita avanzar hacia una comprensión formal de cómo diferentes lenguajes de programación y lógicas expresan ideas similares, porque es una herramienta realmente poderosa de comprensión mutua.
(También, personalmente encuentro la notación de LC tipada, especialmente con verificación de tipos e inferencia, más fácil que la notación de lógica clásica. Podría ser la razón por la que la lógica se considera demasiado complicada.)
- mirrorlake
Espero con ansias leer esto, soy una de las personas que lo preordenó. A menudo he escuchado a personas con títulos decir que lamentan no haber sido mejores con el material de este libro, así que para muchas personas esto será una oportunidad para practicar estas habilidades de una manera que sus títulos en CS/matemáticas/física/ingeniería realmente no habilitaron.
Además, Hillel (el autor) tiene un blog que absolutamente vale la pena revisar, así como algunas excelentes charlas en conferencias que están en YouTube, está en la lista corta de ponentes a quienes automáticamente veo cualquier charla que den.
- Merkur
Leí la parte gratuita. Parece interesante, pero el legado matemático es dominante como se prometió.
Parece favorecer el tipo de código compacto y eficiente que es frágil en manos de un desarrollador junior moderadamente competente, o un senior con multitarea pesada.
Me gusta el código inteligente, en proyectos divertidos, pero en el trabajo prefiero código rápido de leer y de razonar. No intentes ser sofisticado.
Así que supongo que es un libro para desafiar mis suposiciones. Me gusta eso. Gracias.
- mjaniczek
¡Felicidades a Hillel por terminar el libro!