-
Ensayo
Una prueba vale lo que vale su spec
La verificación formal no elimina el riesgo. Lo traslada a la spec, al modelo y a la trusted base. Cinco pruebas ejecutables en Lean 4 que compilan sin errores y aun así esconden bugs reales.
-
Demostración de teoremas
Tus primeras demostraciones en Lean
Los mismos tres teoremas del demostrador en Python, ahora en Lean 4.
-
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
¿Puedo probar programas de Concrete en Lean?
La hoja de ruta original para probar programas de Concrete en Lean, actualizada ahora que parte de ese puente existe: contratos en el código fuente, obligaciones de prueba, evidencia verificada por Lean, detección de pruebas desactualizadas y una base trusted explícita.
-
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.
-
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.