⏱️ Lectura: 12 min
Un lenguaje de programación nuevo llamado Bend promete correr casi tan rápido como C en un solo núcleo y escalar hasta 100 veces más rápido usando el mismo binario en GPU, según su sitio oficial. Pero ese no es el dato más llamativo.
📑 En este artículo
Lo llamativo es su compilador: funciona como un demostrador de pruebas, al estilo de Lean o Rocq, capaz de bloquear cualquier cambio de código (aunque lo haya escrito un agente de IA) si rompe una regla que vos declaraste de antemano en un archivo llamado LAWS.bend.
TL;DR
- Bend es un lenguaje nuevo que compila a código nativo y corre casi tan rápido como C en un solo núcleo.
- El mismo binario escala a 16 núcleos o a GPU sin cambiar el código, hasta 100 veces más rápido que un núcleo.
- Su verificador de tipos funciona como un demostrador de pruebas al estilo Lean o Rocq y tarda como máximo un segundo.
- LAWS.bend declara reglas invariantes; PROOF.bend certifica que el código las cumple antes de mergear.
- La instalación es un solo script: curl -fsSL https://bend-lang.com/install.sh | sh.
- El proyecto recomienda instrucciones específicas en AGENTS.md para que agentes como Claude Code usen Bend solos.
- Bend se apoya en dos papers propios: BendTT, teoría de tipos dependiente afín, y BendRT, su runtime paralelo.
- El propio sitio de Bend advierte que el lenguaje es joven y hay que esperar bugs propios.
Introducción
El lenguaje Bend nace de una premisa incómoda: si cada vez más código lo escribe una IA, el humano deja de leerlo línea por línea. La pregunta que responde Bend no es cómo escribir mejor prompts, sino cómo confiar en un código que nadie revisó a mano. Su respuesta es matemática, no editorial: declarar una ley una sola vez y dejar que el compilador la haga cumplir para siempre.
Esto conecta con una tensión que ya se discute en la industria: la generación masiva de código por agentes está creciendo más rápido que la capacidad de revisarlo. Bend no intenta resolver ese problema con más revisión humana, sino con pruebas formales que corren en cada build.
Qué pasó con el lenguaje Bend
Bend se presenta con un eslogan directo: velocidad de C, paralelismo de CUDA, pruebas de Lean y sintaxis de Python. La instalación es un único script pensado para macOS y Linux:
# macOS / Linux
curl -fsSL https://bend-lang.com/install.sh | shEn Windows no hay instalador nativo documentado: la vía práctica es correrlo dentro de WSL2, ya que el propio proyecto aclara que Bend funciona mejor en Linux y macOS.
# Windows (via WSL2)
wsl --install
wsl -d Ubuntu -- bash -c "curl -fsSL https://bend-lang.com/install.sh | sh"⚠️ Ojo: antes de correr cualquiercurl | sh, conviene descargar el script y leerlo (curl -fsSL https://bend-lang.com/install.sh -o install.sh) en vez de ejecutarlo a ciegas, sobre todo en máquinas con acceso a credenciales de producción.
La segunda parte del anuncio apunta directo a los agentes de codificación: el proyecto sugiere pegar instrucciones en el archivo AGENTS.md que ya leen herramientas como Claude Code, Cursor o Codex.
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 possibleCon eso, según Bend, alcanza con decirle al agente “usá Bend” para que el flujo completo (leer la guía, respetar las leyes, probar antes de commitear) quede delegado.
Contexto e historia
La idea de que un compilador verifique propiedades matemáticas del código no es nueva. Demostradores de teoremas como Lean y Rocq (la continuación del histórico Coq) llevan más de una década usándose para formalizar matemática y verificar software crítico. El microkernel seL4 es el ejemplo más citado de código con pruebas matemáticas de corrección funcionando en producción desde hace años.
Lo que cambia con Bend es la audiencia. Lean y Rocq están pensados para matemáticos y para equipos de verificación formal con presupuesto dedicado; sus chequeos pueden tardar minutos en una base de código mediana. Bend apunta a un desarrollador (o a un agente de IA) que necesita una respuesta en segundos, dentro del mismo ciclo en el que hoy corre un linter o un test unitario.
Detalles técnicos y rendimiento
Bend compila a código nativo. En un solo núcleo, el proyecto afirma que corre cerca de la velocidad de C. El mismo binario, sin recompilar ni reescribir el código, puede correr sobre 16 núcleos o sobre GPU, con una ganancia de hasta 100 veces frente a un solo núcleo, según las mediciones publicadas en su sitio para un Apple M4 Max.
Un ejemplo mínimo, solo para ver la sintaxis:
def main():
return "Hola desde Bend"El caso interesante no es este, sino cómo Bend paraleliza sin hilos ni locks. Si una función se divide en dos llamadas independientes, el runtime las reparte solo:
def suma_rango(lo, hi):
if hi - lo <= 1:
return lo
else:
medio = (lo + hi) / 2
(izquierda, derecha) = (suma_rango(lo, medio), suma_rango(medio, hi))
return izquierda + derechaLas dos llamadas recursivas de suma_rango no dependen una de la otra, así que BendRT (el runtime paralelo descrito en el paper del proyecto) puede despacharlas a núcleos distintos, o a hilos de GPU distintos, sin que el desarrollador escriba un solo thread o lock.
| Modo de ejecución | Cuándo usarlo | Ventaja | Limitación |
|---|---|---|---|
| Un núcleo (CPU) | Prototipado y depuración | Comportamiento predecible y fácil de razonar | No aprovecha el paralelismo disponible |
| Múltiples núcleos (CPU) | Cargas medianas sin GPU a mano | Mismo binario, sin reescribir código | El techo lo pone la cantidad de núcleos físicos |
| GPU | Cargas masivamente paralelas, como el ejemplo pow2.bend del proyecto | Hasta 100 veces más rápido que un núcleo, según bend-lang.com | Exige que el algoritmo se pueda partir en tareas independientes |
El otro pilar técnico es el chequeo de tipos, que en Bend es, literalmente, un chequeo de pruebas. El propio proyecto compara la operación con Lean y Rocq, pero remarca la diferencia de tiempos: mientras esos demostradores pueden tardar minutos en una base de código mediana, Bend tarda como máximo un segundo, lo que permite que un agente de IA lo corra después de cada cambio.
💭 Clave: una prueba en LAWS.bend no detecta bugs en general: solo bloquea las violaciones de la ley específica que alguien escribió. Si nadie declaró la ley, Bend no la va a inventar.
El ejemplo que usa el propio proyecto para mostrar esto es un juego de tres en raya con una ley: you_cant_win, es decir, que ninguna secuencia de movimientos lleva a ganar la partida.
# LAW: no move sequence leads to victory.
law you_cant_win:
for moves: List<move> # cualquier secuencia de movimientos
board = replay(start(), moves) # el tablero resultante
is_won(board) == False # nunca lleva a ganar</move># PROOF: you_cant_win holds.
def Laws.you_cant_win(moves):
# ... prueba escrita por la IACuando le piden al agente que agregue una función nueva (que el tablero “envuelva” en los bordes), sin LAWS.bend el bug pasa directo a producción. Con LAWS.bend, el compilador rechaza el cambio hasta que la IA reconstruye la función y vuelve a probar que la ley se sostiene.
flowchart TD
A["Agente de IA modifica el código"] --> B["bend PROOF.bend"]
B --> C{"¿Se cumple la ley en LAWS.bend?"}
C -->|"sí"| D["Merge permitido"]
C -->|"no"| E["Bloqueado: la IA debe reintentar"]
E --> ACómo empezar con el lenguaje Bend
Para probarlo hoy, el flujo que describe el propio proyecto tiene tres pasos. Primero, instalar:
curl -fsSL https://bend-lang.com/install.sh | shSegundo, pegar el bloque de instrucciones en AGENTS.md del repositorio (el mismo archivo que ya leen Claude Code, Cursor y Codex):
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 possibleTercero, verificar que la instalación quedó activa corriendo la guía completa del lenguaje:
bend guidePara confirmar que una ley realmente se sostiene (y no que Bend simplemente no encontró nada que probar), lo más directo es revisar el código de salida del chequeo de pruebas:
bend PROOF.bend; echo $?Un 0 significa que la prueba pasó; cualquier otro valor indica que el compilador rechazó el cambio porque rompe alguna ley declarada en LAWS.bend.
Impacto y análisis
El caso de uso que más entusiasmo genera es el de bases de código mantenidas casi enteramente por agentes de IA. Si un equipo ya delega el 80% de sus commits a un asistente, según cifras que Google, Anthropic y OpenAI vienen repitiendo este año, la pregunta de quién revisa ese código se vuelve central. Bend propone que la revisión la haga el compilador, no una persona leyendo un diff.
Pero hay un costo real que el propio proyecto no esconde: escribir una ley en LAWS.bend requiere entender, aunque sea de forma superficial, la teoría de tipos dependiente afín en la que se basa Bend (descrita en el paper BendTT). No es lo mismo escribir un test unitario que formalizar un invariante. En la práctica, quien redacta la prueba suele ser la propia IA, lo que traslada el problema de confianza un nivel más abajo: ahora hay que confiar en que el agente no escribió una prueba vacía o trivialmente verdadera para pasar el chequeo.
Otra limitación honesta: las pruebas solo cubren lo que alguien pensó en declarar como ley. Un bug de rendimiento, una regresión de estilo o un caso de borde que nadie anticipó no quedan bloqueados por LAWS.bend simplemente porque nunca se escribieron como ley. Bend no reemplaza el testing, lo complementa para el subconjunto de invariantes que un equipo decide volver innegociables.
Qué sigue
El propio sitio de Bend es explícito: el lenguaje es joven, hay que esperar bugs propios del compilador y del runtime, y el pedido es que se reporten como issues. La documentación central vive en GUIDE.md, accesible también desde la terminal con bend guide, y el sustento teórico está en dos papers: BendTT, sobre la teoría de tipos que hace de base, y BendRT, sobre el runtime paralelo para CPU y GPU.
La convención de instrucciones en AGENTS.md es, quizás, lo más fácil de adoptar hoy: no depende de reescribir un proyecto entero en Bend, sino de decidir declarar como leyes un puñado de invariantes críticos (por ejemplo, que una función de facturación nunca cobre de más) y dejar que el propio agente de IA se encargue de mantenerlos.
📖 Resumen en Telegram: Ver resumen
Probalo vos: corré curl -fsSL https://bend-lang.com/install.sh | sh y seguí con bend guide para ver la sintaxis completa en minutos.
Preguntas frecuentes
¿Qué es el lenguaje Bend?
Es un lenguaje de programación con sintaxis parecida a Python, compilador a código nativo y un verificador de tipos que funciona como demostrador de pruebas, pensado para que agentes de IA escriban código sin romper invariantes declaradas.
¿Necesito escribir las pruebas a mano?
No necesariamente. En el flujo que propone el proyecto, la IA escribe tanto el código como la prueba en PROOF.bend; la persona solo declara la ley en LAWS.bend.
¿Bend corre en Windows?
No hay instalador nativo documentado para Windows. La alternativa práctica es usar WSL2, ya que el proyecto aclara que funciona mejor en Linux y macOS.
¿Qué son BendTT y BendRT?
BendTT es el paper que describe la teoría de tipos dependiente afín que sostiene el sistema de pruebas de Bend. BendRT describe el runtime paralelo que reparte el cómputo entre CPU y GPU.
¿Bend reemplaza a los tests unitarios?
No. Solo bloquea violaciones de las leyes que alguien declaró explícitamente en LAWS.bend; cualquier comportamiento no cubierto por una ley sigue necesitando tests tradicionales.
¿Bend es apto para producción hoy?
El propio sitio del proyecto pide esperar bugs y reportarlos como issues, y recomienda usarlo sobre todo en el backend, en Linux y macOS.
Referencias
- bend-lang.com: sitio oficial de Bend, con la propuesta, los ejemplos y el script de instalación.
- lean-lang.org: sitio del demostrador de teoremas Lean, referencia directa que usa Bend para explicar su verificador de tipos.
- rocq-prover.org: sitio de Rocq (la continuación de Coq), el otro demostrador de teoremas que Bend cita como comparación.
- sel4.systems: microkernel verificado formalmente, antecedente histórico del código con pruebas matemáticas de corrección en producción.
📱 ¿Te gusta este contenido? Únete a nuestro canal de Telegram @programacion donde publicamos a diario lo más relevante de tecnología, IA y desarrollo. Resúmenes rápidos, contenido fresco todos los días.
0 Comentarios