Bend: un lenguaje con verificación de pruebas que bloquea los errores de la IA en CPU y GPU

Bend es un lenguaje compilado y paralelo orientado a código generado por IA. Su premisa central: en lugar de confiar en resultados que nunca revisas, declaras leyes en un archivo LAWS.bend y exiges que el agente las demuestre antes de fusionar.

La propuesta suena como la de cualquier otra herramienta de codificación con IA, pero la mecánica es distinta. El verificador de tipos de Bend es un verificador de pruebas, la misma idea que Lean o Rocq. La diferencia que enfatiza es la velocidad: esos verificadores pueden tardar minutos en bases de código medianas, mientras que Bend afirma que tarda como máximo un segundo, para que un agente pueda ejecutar comprobaciones tras cada cambio.

De dónde viene la velocidad

• Compila a código nativo. Casi a la velocidad de C en un solo núcleo.
• El mismo binario escala a dieciséis núcleos o a la GPU. La documentación afirma hasta 100 veces más rápido que un solo núcleo.
• El paralelismo es automático. Divides el trabajo en dos; Bend reparte las llamadas entre núcleos de CPU o de GPU y luego las une. Sin hilos, sin bloqueos, sin código de kernel.

El sitio muestra un ejemplo de pow2.bend ejecutándose en 4.096 núcleos de GPU.

El modelo de leyes y pruebas

Escribes una ley en LAWS.bend:

# LAW: no move sequence leads to victory.
law you_cant_win : for moves: List<Move>
    board = replay(start(), moves)
    is_won(board) == False

Luego el agente escribe la prueba correspondiente en PROOF.bend:

# PROOF: you_cant_win holds.
def Laws.you_cant_win (moves):
    # ... escrito por la IA

Una vez declarada una ley, el sitio sostiene que el agente no puede fusionar una línea que la rompa. La demo usa un juego: pídele a Claude que haga que el tablero se envuelva. Sin LAWS.bend, el error se fusiona y se publica. Con él, el agente debe reintentar hasta construir una prueba. La frase en la fuente: fusionar un error se vuelve "matemáticamente imposible".

Configuración

Instalación:

curl -fsSL https://bend-lang.com/install.sh | sh

Luego añade este bloque a tu AGENTS.md para que los agentes sepan qué hacer:

When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible

Bend básicamente trata LAWS.bend como un AGENTS.md respaldado por pruebas. "No cometas errores" pasa a estar verificado por tipos.

Advertencias de la fuente

La documentación es clara: Bend es joven, espera errores y repórtalos. Funciona mejor en el backend y apunta a Linux y macOS. El núcleo está respaldado por dos artículos: BendTT (teoría de tipos afines dependientes) y BendRT (runtime paralelo de CPU/GPU).

Para quién es

Equipos que dejan que los agentes publiquen código que no leen, especialmente servicios de backend donde una regla como "los saldos nunca son negativos" necesita aplicación, no una revisión de código.