Inspección aduanera para el código: cómo garantizar la optimización sin errores de los programas infantiles ✛

Un niño construye un juego sencillo en Scratch: un personaje aparece en el centro y salta instantáneamente a una esquina. El primer movimiento se pierde entre fotogramas: nadie lo ve. Eliminar esa instrucción es seguro. Pero, ¿cómo lo sabe un optimizador automático? Hoy, el repositorio de Scratch alberga decenas de millones de proyectos escritos por jóvenes autores. Un error del mejorador podría distorsionar su intención sin que nadie lo note.

La solución recuerda a una inspección aduanera. Un optimizador no verificado escanea el proyecto, construye un grafo de dependencias y propone eliminar, por ejemplo, un disfraz no utilizado o una instrucción muerta. La corrección viene acompañada de un «certificado», una declaración digital que indica el tipo de cambio y las condiciones de seguridad. Un inspector-controlador de confianza, sin creer una sola palabra, vuelve a analizar ambas versiones del programa. Recalcula todas las condiciones. La lente de observación (el conjunto de eventos visibles para el jugador) sirve de guía principal: si una escritura en un recurso se sobrescribe antes de que pueda ser observada, se puede eliminar. Este es el teorema central del marco cooperativo, demostrado en Lean. Ningún truco puede ocultarse del certificado.

El experimento con 300 proyectos reales mostró que al menos una mejora segura se obtuvo en 283 proyectos, es decir, el 94,3 %. Principalmente se limpiaron recursos no utilizados, pero en 17 casos también se eliminaron escrituras semánticamente muertas. Lo más importante: un ataque adversarial con 4278 correcciones que incluían errores deliberados no logró burlar el control ni una sola vez. El controlador rechazó todas las opciones peligrosas. Un oráculo diferencial, que comparó el comportamiento de los programas original y optimizado en una máquina virtual, no registró ninguna discrepancia.

Por primera vez, para un lenguaje paralelo orientado a eventos se ha construido un sistema en el que cada cambio lleva un certificado verificable. Esto traslada la disciplina de los compiladores verificados a un mundo donde el precio del error es especialmente alto. El teorema del marco cooperativo está parametrizado por el tipo de recurso y la lente de observación: una sola demostración cubre toda una clase de optimizaciones. Garantiza la completitud informacional de las condiciones de corrección, cortando cualquier canal de observación inesperado. La base confiable es compacta: 9 921 líneas en Python y 5 909 líneas de demostración en Lean, un volumen asumible para la auditoría de un equipo pequeño. Además, el enfoque no necesita suposiciones probabilísticas ni inferencia bayesiana: ofrece garantías absolutas. El programa puede considerarse como un sistema dinámico, y su verificación como un análisis determinista, no como un proceso estocástico.

La aduana del código ya está en funcionamiento. En el futuro podrá verificar correcciones propuestas por inteligencia artificial y se convertirá en la base de asistentes de IA confiables. Por ahora, el inspector está listo para trabajar: cuando el niño pulse «ejecutar», su idea permanecerá intacta.