-
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
¿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
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
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.