Concrete
Concrete es un lenguaje de sistemas hecho para que el compilador pueda decir algo más que compila o no compila. Tipos lineales, capabilities (capacidades) explícitas, limpieza visible, contratos en el código fuente y evidencia de prueba verificada en Lean convierten el comportamiento oculto de un programa en hechos que el compilador puede exponer.
Sobre la imagen La represa Hoover se coló de a un bloque acotado por vez, cada encofrado dimensionado para que los ingenieros pudieran saber cómo iba a fraguar y a soportar carga cada sección. Concrete, el lenguaje, encara el código de la misma manera: unidades chicas y explícitas cuyo comportamiento el compilador puede enunciar. Colado de hormigón en un bloque de la sección central de la represa Hoover, Black Canyon, Nevada-Arizona, julio de 1933. Foto: fotógrafo desconocido del U.S. Bureau of Reclamation, dominio público, vía Wikimedia Commons (National Archives 293921).
Traducción automática del original en inglés, todavía sin revisar. Leer el original.
Los lenguajes de sistemas mainstream se volvieron enormes, pero el compilador sigue diciendo casi siempre una de dos cosas: compila o no compila. Los caminos de asignación de memoria (allocation), la autoridad, la limpieza (cleanup), los lifetimes, las fronteras de confianza (trust boundaries): la mayor parte de lo que el programa realmente hace queda justo afuera de lo que el compilador tiene permitido decirte.
Concrete está construido al revés. Un lenguaje de superficie más chico. Tipos lineales. Borrowing acotado por regiones. Capabilities (capacidades) explícitas. Limpieza visible. Contratos en el código fuente (source contracts) y evidencia verificada en Lean. Cada restricción está ahí para hacer visible algo, de modo que el compilador pueda responder preguntas que otros compiladores suelen dejarle a la revisión de código.
La serie es el argumento a favor de esa apuesta. Ocho ensayos, cada uno encarándola desde un ángulo distinto:
- Por qué existe Concrete. Qué les falta a los lenguajes que ya tenemos, y por qué hacer uno más chico es la jugada.
- La gran visión de Rust, la respuesta de Concrete. En qué acierta el debate sobre efectos en Rust, y dónde un lenguaje más chico termina con respuestas más limpias.
- La trampa de los datos de entrenamiento de la IA. Por qué los ecosistemas de lenguajes están quedando atrapados por los datos que dejan atrás, y cómo Concrete está diseñado para escapar de eso.
- Probar programas de Concrete en Lean. La entrada original de la hoja de ruta de pruebas, ahora actualizada con lo que se concretó: contratos en el código fuente, estado de prueba, detección de pruebas desactualizadas (stale) y ejemplos verificados en Lean.
- Cuando el compilador es el oráculo. La demostración más directa de la serie: un compilador que responde preguntas semánticas, no solo sintácticas.
- Lo que Concrete empeora. La lista honesta de concesiones (trade-offs). Los lenguajes más chicos cuestan algo.
- Un compilador que produce hechos. Hacia dónde va esto: compiladores que emiten hechos legibles por máquina sobre autoridad, evidencia de prueba, confianza y riesgo en tiempo de ejecución, no solo binarios.
- Etiquetas nutricionales para la confianza. Vitalik Buterin quiere que el software venga con una lista de sus dependencias de confianza; así es como un compilador que produce hechos ya arma la mitad de esa etiqueta que corresponde a la máquina y a la matemática.
Si querés la tesis, empezá por el uno. Si querés ver la apuesta en concreto, saltá al cinco y después volvé: el ensayo del compilador como oráculo es donde todo se vuelve legible de una sola vez.
El problema
Los lenguajes de sistemas pueden garantizar seguridad y aun así ocultar demasiado de lo que el código realmente hace. La asignación de memoria (allocation), la autoridad, la limpieza (cleanup) y las fronteras de confianza (trust boundaries) suelen quedar desparramadas entre detalles de implementación, convenciones y herramientas.
Por qué fallan los enfoques existentes
Los lenguajes mainstream suelen resolver esto agregando más maquinaria o apoyándose en las normas del ecosistema. Eso ayuda en algunas dimensiones y perjudica en otras: más comportamiento oculto, más interacción entre features y menos estructura legible para el compilador.
Nuestro enfoque
Concrete toma el camino opuesto: un lenguaje más chico con capabilities explícitas, ownership lineal, limpieza visible y un compilador diseñado para exponer hechos semánticos de forma lo bastante directa como para servir a la auditoría, a la prueba y a la mejora automatizada.
Referencia
Panorama vivo del lenguaje y referencia de diseño de Concrete.
Episodios
-
Episodio 1: 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.
-
Episodio 2: 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.
-
Episodio 3: 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.
-
Episodio 4: ¿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.
-
Episodio 5: 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.
-
Episodio 6: 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.
-
Episodio 7: 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.
-
Episodio 8: 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.
Esta serie está en curso. Vienen más episodios.