Por qué existe Concrete

Traducción automática del original en inglés, todavía sin revisar. Leer el original.

Esta es la pieza fundacional de la serie sobre Concrete. Si primero querés la demostración más práctica, empezá por Cuando el compilador es el oráculo. Si querés la referencia viva del lenguaje, usá la Especificación de Concrete.

La programación de sistemas tiene un problema recurrente. Queremos escribir código cerca de la máquina, pero también queremos poder afirmar cosas fuertes sobre lo que hace ese código. ¿Asigna memoria? ¿Toca la red? ¿Pierde recursos? ¿Se puede auditar sin rastrear veinte funciones auxiliares y tres capas de convenciones de bibliotecas?

La mayoría de los lenguajes responden esas preguntas de forma indirecta. Leés la implementación. Hacés profiling. Inferís a partir del estilo. Confiás en los bloques unsafe, en la documentación y en la disciplina de revisión. Incluso en lenguajes fuertes, mucho de lo que importa de un programa vive fuera del sistema de tipos.

Concrete existe porque creo que ese es el lugar equivocado para detenerse.

Concrete es un lenguaje de sistemas construido alrededor de un único principio organizador: toda propiedad importante que el compilador pueda saber sobre un programa debería ser lo bastante explícita como para que humanos y máquinas puedan actuar directamente sobre ella.

#El problema

La concesión (trade-off) habitual de los lenguajes de sistemas se plantea como rendimiento contra seguridad. Es real, pero no es la única tensión que importa.

Hay otra:

• los lenguajes pueden ser lo bastante expresivos como para construir software serio
• o pueden ser lo bastante simples como para que el compilador explique qué está haciendo el software

Cuando un lenguaje se vuelve más implícito, más inferencial y más cargado de features, la brecha entre “lo que hace el código” y “lo que el compilador puede decir claramente” se agranda. Los destructores corren de forma invisible. La asignación de memoria (allocation) se esconde dentro de patrones de conveniencia. El comportamiento con efectos es ambiental. Las fronteras de confianza (trust boundaries) colapsan en un único balde amplio de unsafe. El código sigue siendo escribible, pero se vuelve más difícil de auditar, más difícil de probar y más difícil de optimizar a partir de hechos semánticos en lugar de ruido de benchmarks.

Concrete es un intento de empujar en la dirección opuesta: un lenguaje más acotado que resigna conveniencia para que el compilador pueda exponer más verdad.

#Las apuestas centrales

Concrete hace cinco apuestas.

1. Los efectos van en las firmas de las funciones. Si una función lee un archivo, asigna memoria, consulta el reloj o llama a la red, eso debería ser visible en su tipo mediante capabilities (capacidades) como with(File) o with(Alloc). Nada de autoridad ambiental, nada de adivinar a partir de detalles de implementación.

2. El ownership debería ser lineal por defecto. El ownership afín de Rust evita el use-after-free, pero todavía te deja olvidarte de un valor y dejar que Drop limpie a tus espaldas. Concrete es más estricto. Los valores con dueño se tienen que consumir exactamente una vez. La limpieza (cleanup) es explícita, con destroy y defer. Es más ceremonioso, pero significa que los lifetimes de los recursos son parte del programa visible y no una acción oculta del compilador.

3. El comportamiento oculto es el enemigo. Nada de destructores implícitos, nada de asignación oculta, nada de sobrecarga de operadores, nada de closures con capturas invisibles, nada de excepciones desenrollando la pila a través de código que no podés ver. Cuando leés una función, el objetivo es que estés mirando lo que realmente se ejecuta.

4. Más chico le gana a más ingenioso. No quiero un lenguaje que siga absorbiendo más maquinaria a cambio de garantías más fuertes. Quiero un solo modelo de efectos, un solo modelo de ownership, una gramática chica y un lenguaje núcleo que todavía entre en una cabeza humana.

5. El compilador debería producir conocimiento estructurado, no solo aprobado/rechazado. Si el lenguaje es lo bastante explícito, el compilador puede reportar cosas como el uso de capabilities, las fronteras de confianza, los sitios de asignación, la superficie de la interfaz pública y los subconjuntos elegibles para prueba. Eso cambia cómo los humanos revisan código y cómo los agentes automatizados lo mejoran.

#Cómo se ve eso en la práctica

Este diseño lleva a un tipo específico de lenguaje.

Una función pura es pura porque no declara capabilities y el compilador prueba esa afirmación a través del grafo de llamadas.

Una función que asigna memoria dice with(Alloc).

Una función que puede leer archivos dice with(File).

Una función que cruza una frontera foránea o semánticamente peligrosa dice with(Unsafe).

Una función que administra un recurso muestra su limpieza en el código fuente con defer destroy(x).

Un pedazo de truco de implementación de bajo nivel se puede marcar como trusted, separando la falta de seguridad interna a nivel de punteros de la autoridad semántica visible desde afuera.

El resultado va más allá de “C más seguro” o “Rust más estricto”. Es un lenguaje cuya semántica pretende ser lo bastante legible como para que el compilador pueda responder directamente preguntas de más alto nivel.

Por eso los posts siguientes de esta serie se concentran en cosas como:

• por qué el debate sobre efectos en Rust apunta hacia un lenguaje más chico, no a uno más grande
• por qué la explicitud importa para la generación asistida por IA
• por qué un compilador basado en Lean abre una oportunidad para probar código de sistemas real
• por qué los reportes del compilador pueden convertirse en un ciclo práctico de optimización
• qué empeora Concrete a cambio de esas propiedades

#Para qué es Concrete

Concrete no intenta ser el mejor lenguaje para todo.

Apunta a código donde el comportamiento oculto sale caro:

• firmware
• fronteras de seguridad
• software criptográfico
• motores de políticas
• componentes críticos para la seguridad
• código de sistemas que eventualmente puede necesitar verificación formal

Son dominios donde “¿qué puede hacer esta función?” no es una pregunta de estilo sino una pregunta de auditoría, a veces una pregunta de certificación.

Para esos dominios, creo que un lenguaje más chico y más explícito es mejor negocio que uno más ergonómico y más mágico.

#Para qué no es Concrete

Concrete no es un lenguaje que pone la conveniencia primero.

Es peor que Rust o Zig en muchas cosas agradables:

• el código cargado de recursos es más verborrágico porque la limpieza es explícita
• la composición de orden superior es más explícita porque no hay closures con capturas ocultas
• el ecosistema está en sus comienzos
• el conjunto de herramientas todavía está inmaduro comparado con lenguajes establecidos

Ese costo viene del diseño. Un post posterior sobre concesiones lo va a hacer explícito con más detalle.

Creo que vale la pena pagar esos costos en algunos dominios y no en otros. Las ventajas y las desventajas de Concrete vienen de las mismas restricciones.

#Por qué importa Lean

El compilador de Concrete está escrito en Lean 4. Eso empezó como una decisión práctica de implementación, pero tiene consecuencias de arquitectura.

Todo programa de Concrete se convierte en datos nativos de Lean a medida que avanza por el pipeline del compilador. Eso crea un camino, todavía incompleto pero muy real, desde el código de sistemas hasta las herramientas de prueba, sin coser dos ecosistemas que no tienen nada que ver. También empuja hacia una forma de lenguaje que efectivamente se puede formalizar: una semántica núcleo chica, efectos explícitos, ownership explícito, poca maquinaria implícita.

No creo que “escrito en Lean” sea la razón principal para que te importe Concrete. La razón principal es el diseño del lenguaje en sí. Pero Lean hace que la historia de verificación a largo plazo sea más plausible de lo que sería si no.

#Qué existe hoy

Concrete ya no es solo un boceto. El compilador es una base de código real en Lean 4 con un pipeline por etapas, una suite de tests considerable, una biblioteca estándar en crecimiento, contratos en el código fuente, reportes de prueba y modos de reporte orientados a auditoría.

Lo que todavía no existe es igual de importante:

• no hay un kernel verificado de punta a punta conectado al compilador implementado
• no hay un formatter, un package manager ni un LSP maduros
• todavía no hay una historia de adopción amplia

El cambio más grande desde que se escribió por primera vez esta pieza fundacional es que la historia de las pruebas dejó de ser solo una dirección. Algunas funciones ahora llevan vínculos a pruebas en el código fuente. Si la función cambia, la prueba puede quedar desactualizada (stale) en lugar de seguir en verde en silencio. Los reportes distinguen un teorema verificado por Lean de un hecho garantizado por el compilador, un resultado de un solver, una suposición o una prueba faltante. La afirmación honesta sigue sin ser “el compilador está verificado”. Es más acotada y más útil: afirmaciones seleccionadas sobre funciones seleccionadas ahora se pueden probar, reportar, comparar con diff y auditar sin hacer de cuenta que son todas el mismo tipo de garantía.

Así que la forma correcta de leer esta serie no es “anuncio de un lenguaje terminado”. Es “un argumento a favor de una dirección de diseño particular, con algunas partes ya funcionando y otras todavía en construcción”.

#Para dónde seguir

Si querés el resto del argumento, leé la serie más o menos en este orden:

1. Por qué existe Concrete
2. El debate sobre efectos en Rust y el argumento de Concrete a favor de un lenguaje más chico
3. La trampa de los datos de entrenamiento de IA para los lenguajes de programación tiene salida
4. ¿Puedo probar programas de Concrete en Lean?
5. Cuando el compilador es el oráculo
6. Lo que Concrete empeora
7. Un compilador que produce hechos

Si querés los detalles del lenguaje en lugar de la versión ensayo, usá la Especificación de Concrete.

Esa es la apuesta detrás de Concrete: no un lenguaje de sistemas más expresivo, sino uno más legible. Un lenguaje que restringe al programador para que el compilador pueda decir más cosas que realmente sirvan.