Bend, el lenguaje que quiere que la IA demuestre sus cambios antes de fusionarlos
Es un lenguaje compilado que usa pruebas formales como comprobador de tipos y se engancha a los agentes de IA a través de AGENTS.md. La web no da versión ni licencia.
Bend es un lenguaje de programación que compila a código nativo, reparte el trabajo entre los núcleos que encuentre o la GPU y sustituye el comprobador de tipos por un verificador de pruebas al estilo de Lean y Rocq. Su web promete dos cosas: rendimiento cercano a C y una barrera que impida a un agente de IA fusionar una línea que rompa una regla declarada de antemano. Se instala con un script que se descarga con curl y se pasa a sh, y de momento no publica número de versión ni licencia.
El rendimiento que anuncia la página es suyo, no de un tercero. Sobre un núcleo dice que va casi como C; el mismo binario se reparte después por dieciséis núcleos o por la GPU, donde llega hasta cien veces más rápido que uno solo. Las gráficas están medidas en un Apple M4 Max y esa comparación de las cien veces es contra el propio lenguaje en un solo núcleo, no contra otra herramienta.
El comprobador de tipos es un verificador de pruebas, el mismo enfoque de Lean y Rocq, con una diferencia que el texto considera clave: donde esos tardan minutos en una base de código mediana, Bend dice que tarda como mucho un segundo. Ese margen es lo que permite a un agente comprobar después de cada cambio en lugar de al final.
Leyes y demostraciones
El mecanismo son dos ficheros. En LAWS.bend se declaran las leyes del programa; en PROOF.bend vive la demostración, que escribe el propio agente. El ejemplo de la web es un juego: una ley afirma que ninguna secuencia de movimientos puede llevar a la victoria. Sin el fichero de leyes, un agente al que se pide que el tablero se enrolle fusiona el error; con él, el error queda bloqueado y el agente tiene que reintentar hasta demostrar que la ley se sostiene. La afirmación es fuerte: fusionar el fallo es imposible porque es un teorema.
Para engancharlo a un agente se añaden cuatro instrucciones a AGENTS.md: que ejecute el comando que imprime la guía del lenguaje, que guarde las reglas importantes en LAWS.bend, que lance la comprobación de pruebas antes de cada commit y que paralelice siempre que pueda. Después basta con decirle «usa Bend». La misma web ofrece un hub de paquetes y una línea de comandos para traer dependencias de ahí.
Bend se declara joven, avisa de que habrá fallos y funciona mejor en backend, solo en Linux y macOS. Dos datos que cualquier equipo mira antes de meterlo en un pipeline, versión y licencia, no aparecen por ningún lado. Lo que sí está sobre la mesa es la propuesta: un contrato que la máquina puede verificar entre quien pide el código y quien lo escribe, sea una persona o un modelo. Lo que falta es una demo pública y alguien que no sea el propio proyecto midiendo lo que promete.
