-
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.
-
Demostración de teoremas
Construyendo un pequeño demostrador de teoremas en Python
Un pequeño demostrador de teoremas es apenas un lenguaje de términos, un checker y un kernel chico de confianza. Construimos uno en Python puro para dejar la arquitectura a la vista.
-
Demostración de teoremas
Las proposiciones son tipos, las demostraciones son programas
La correspondencia de Curry-Howard dice que los tipos y las proposiciones lógicas son lo mismo. Entender por qué cambia cómo pensás tanto la programación como la matemática.
-
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
Etiquetas nutricionales para la confianza
Vitalik Buterin quiere etiquetas nutricionales de confianza para el software. Concrete muestra cómo se ve la mitad de máquina y matemática cuando la produce el compilador en lugar de un proveedor que escribe prosa.
-
Concrete
Un compilador que produce hechos
Concrete ya sabe mucho sobre aquello de lo que depende un programa: autoridad, asignación de memoria, recursión, confianza, obligaciones de seguridad y evidencia de prueba. El próximo paso es hacer que esos hechos sean fáciles de usar para agentes, CI y revisores.
-
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.