-
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.
-
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
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
Lo que Concrete empeora
Las restricciones de Concrete tienen costos reales. La limpieza lineal es verbosa, las closures con capturas ocultas no existen y el ecosistema todavía está verde. Esto es lo que el lenguaje realmente hace más difícil.
-
Concrete
Cuando el compilador es el oráculo
Corrí un loop al estilo autoresearch sobre un programa en Concrete. El compilador le dijo a un agente dónde se podían mejorar la autoridad, la asignación de memoria y la superficie de prueba, y le confirmó cuándo esas propiedades cambiaban. Sin profiler, sin ruido de benchmarks. Tu compilador puede responder preguntas en vez de decir pasa/no pasa.
-
Concrete
Diseñar un lenguaje de programación para la era de la IA
Edgar Luque tiene razón en que la IA crea una nueva barrera para los lenguajes de programación. Se equivoca en que la barrera sea universal. Los lenguajes diseñados para la generación y la verificación por máquinas invierten el problema por completo.
-
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.