Un compilador que produce hechos

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

Nota de la serie: este artículo es parte de la serie Concrete y responde a Giving LLMs a Formal Reasoning Engine for Code Analysis, de Dmitri Sotnikov. Relacionados: Cuando el compilador es el oráculo y Por qué existe Concrete.

Cuando un agente de IA explora una base de código, normalmente hace grep de nombres, lee algunas coincidencias, busca quién llama a qué, lee eso, y trata de armarse un modelo mental del programa a partir de fragmentos de texto. Funciona más o menos tan bien como te imaginás. El agente está haciendo preguntas estructurales sobre un programa, cosas como “¿puede la entrada del usuario llegar a esta consulta SQL?” o “¿qué cambia si toco esta función?”, pero la única herramienta que tiene es la búsqueda de texto.

Ayer leí el artículo de Dmitri Sotnikov sobre darles a los LLMs un motor de razonamiento simbólico para analizar código. Su herramienta, Chiasmus, parsea código fuente con tree-sitter (un parser sintáctico), convierte definiciones y llamadas en hechos lógicos, y deja que un LLM corra consultas (queries) sobre grafos en lugar de hacer grep por los archivos. Es una interfaz mucho mejor: el agente hace una pregunta estructural y recibe una respuesta estructural.

Leer el post me dio una mejor frase para parte de lo que estamos construyendo con Concrete: un compilador que produce hechos (fact-producing compiler).

Concrete es el lenguaje de programación de sistemas que estamos construyendo para programas que necesitan ser auditables. Compila el código a un ejecutable y a afirmaciones verificadas sobre lo que ese ejecutable puede hacer.

#De la sintaxis a la semántica

Chiasmus funciona recuperando la estructura del código fuente a posteriori: parsea archivos, extrae qué funciones existen y qué llama a qué, y lo convierte en hechos consultables. Para los lenguajes existentes, que nunca se diseñaron para exponer esta información, ese es el enfoque práctico.

Concrete puede ir más lejos porque el compilador ya sabe más que la sintaxis. Tree-sitter puede ver que foo llama a bar, pero el compilador de Concrete además sabe que bar requiere autoridad de Network, que foo lleva esa autoridad en su firma, y que la cadena de llamadas cruza una frontera FFI trusted.

Por autoridad me refiero a lo que el código tiene permitido hacer: asignar memoria, leer archivos, tocar la red, llamar código unsafe, cruzar a código externo. En Concrete, esos permisos son parte del programa que el compilador verifica. No son comentarios y no los recupera después un escáner.

Hoy el compilador expone esto como un reporte para humanos. Un reporte de autoridad sobre nuestro parser de JSON muestra de dónde viene la asignación de memoria (allocation):

capability Alloc (13 functions):
  pub store  <- store -> vec_push
      parse_string  <- parse_string -> store
  pub parse_value  <- parse_value -> parse_string
      parse_array  <- parse_array -> vec_push

Una línea como esta se lee así: parse_value necesita asignación porque llama a parse_string, que en algún momento guarda bytes en un vector.

El compilador sigue las capabilities (capacidades) (File, Network, Alloc, etc.) en las firmas de las funciones, las hace cumplir de forma transitiva, y puede informar el camino que explica por qué una función necesita cierta autoridad. También sigue la forma de la ejecución: recursión directa, ciclos de llamadas mutuas y si los loops son acotados. El perfil predictable es la dirección más estricta: hoy Concrete informa y verifica partes de la ejecución acotada, mientras que el perfil aplicado por completo todavía se está ajustando.

Para las pruebas rige la misma regla. Un reporte puede decir si una afirmación fue simplemente informada por el compilador, aplicada por un chequeo del compilador, probada en Lean (un asistente de pruebas), o aceptada por un supuesto trusted. La evidencia de prueba se adjunta al nombre de la función y a la huella (fingerprint) de su cuerpo, así que el código que cambió no puede conservar en silencio pruebas desactualizadas (stale).

Todo esto empezó como reportes legibles por humanos. Desde entonces, el proyecto se acercó a lo que defiende este artículo: un solo artefacto que las herramientas de revisión, la CI y los agentes pueden leer por igual. Los reportes ahora tienen paquetes de pruebas, obligaciones de los contratos en el código fuente (source contracts), registros de VCs, salida de trazabilidad, resúmenes de auditoría y mejor detección de desvíos. Lo que queda por hacer no es inventar los hechos. Es hacer que toda la superficie sea agradable de consultar.

#Cómo se ve consultar

Pensá en un escenario de rutina. Un revisor abre un PR que sube la versión de una dependencia. La versión nueva lee variables de entorno tres capas adentro, en una función auxiliar. En Rust, nada cambia en las firmas de las funciones y el revisor tiene que hacer diff del código de la dependencia o rezar para que el changelog lo mencione. En Concrete, la función que llama a esa dependencia tiene que haber declarado autoridad de Env o el build se rompe.

Quiero el mismo tipo de interfaz para todos los hechos del compilador, capabilities incluidas. Así es como podría verse. Un agente o una herramienta hace una pregunta, y el compilador devuelve una respuesta verificada:

“¿Puede el núcleo del parser de paquetes tocar la red?”

{
  "reachable": false,
  "from": "main.decode_header",
  "to_capability": "Network",
  "evidence": "compiler-checked call graph and capability facts"
}

“¿Por qué main no es predecible?”

{
  "violations": [
    {
      "gate": "no_blocking",
      "capability": "File",
      "path": ["main.main", "std.fs.read_to_string"]
    }
  ]
}

“¿Qué dependencia amplió su autoridad desde ayer?” Como el compilador sigue la cadena de autoridad de cada función, puede devolver el camino.

El modelo puede explicar el resultado. El compilador debería proveerlo.

#Lo que estamos haciendo consultable

Primero, deberíamos exponer los hechos alrededor de los cuales Concrete ya está construido: qué funciones pueden asignar memoria, leer archivos, tocar la red, llamar código unsafe o cruzar FFI; por qué se requiere cada autoridad; qué funciones son recursivas o entran en ciclos de llamadas; qué loops son acotados; qué obligaciones de seguridad en tiempo de ejecución existen; qué afirmaciones de prueba están vigentes, probadas, desactualizadas, faltantes, asumidas, aplicadas, informadas o trusted.

Después debería responder las preguntas que la gente hace en una revisión. ¿Esta dependencia agregó un camino hacia File, Network o Env? ¿Este módulo se volvió menos predecible? ¿Alguna prueba quedó desactualizada? ¿Se movió una frontera trusted? ¿Se amplió la autoridad entre el build de ayer y el de hoy?

El artefacto de hechos va primero. Una CLI de consultas, MCP, chequeos de CI, herramientas de revisión y la integración con agentes deberían leer todos los mismos hechos verificados.

#El compilador debería decir qué es verdad

Un compilador debería decir qué es verdad sobre el programa, más allá de “pasó el type check”. ¿Qué puede tocar esta función? ¿Es recursiva? ¿Sus loops son acotados? ¿Cruza FFI? ¿La prueba está vigente? ¿Qué camino explica la autoridad?

Esos son hechos del programa. Concrete produce algunos, aplica otros, prueba otros y etiqueta el resto. La dirección no es solo mejores reportes. Es un artefacto del compilador sobre el cual otras herramientas pueden construir con seguridad.