-
Demostración de teoremas
Programar un mini-Lean en el sistema de tipos de Julia
Guillermo Angeris arma un demostrador de teoremas que funciona en 61 líneas de Julia. Un kernel de confianza chiquito, seis axiomas, y el compilador hace el resto. Esta es la construcción.
-
Concrete
El debate sobre efectos en Rust y el argumento de Concrete a favor de un lenguaje más chico
Wuyts tiene razón sobre los efectos y el ownership. Los escépticos de Hacker News tienen razón sobre la complejidad. Concrete acepta las dos cosas y les dice que no a los tipos refinados.
-
Ensayo
La guía de Fede sobre sistemas de tipos: de generics a tipos dependientes
Una guía práctica de sistemas de tipos, desde los generics de todos los días hasta los tipos dependientes que prueban corrección, con ejemplos en Rust, Scala e Idris
-
Concrete
Por qué existe Concrete
Concrete es un lenguaje de sistemas diseñado para que el compilador pueda razonar sobre lo que hace el código: autoridad, asignación de memoria, lifetimes de recursos y superficie de prueba.