Bend – un lenguaje que bloquea errores de IA mediante pruebas y se ejecuta en GPUs

Artículo original ↗ Discusión en Hacker News ↗

Un nuevo lenguaje de programación llamado Bend busca permitir que los desarrolladores especifiquen “leyes” formales que el código generado por IA debe cumplir, usando un sistema de tipos dependiente afín y un runtime acelerado por GPU para verificar pruebas rápidamente. Los comentaristas se muestran intrigados por la idea de restringir a los LLM con invariantes verificadas por máquina, pero plantean preocupaciones prácticas: escribir leyes completas y correctas puede ser tan difícil como escribir el programa, las leyes mal especificadas pueden ser manipuladas, y el ecosistema actual (stdlib, ergonomía, herramientas) sigue siendo inmaduro. También surgen dudas de confianza por el uso intensivo de IA en el propio código y la documentación del proyecto, la eliminación previa del historial de git y las afirmaciones audaces sobre rendimiento y corrección frente a asistentes de prueba maduros como Lean o Agda.

Objetivos del proyecto y posicionamiento

  • Bend se presenta como un lenguaje con una teoría de tipos dependiente afín, orientado a demostrar “leyes” sobre programas y compilar a código eficiente para CPU/GPU.
  • La idea central: humanos/agentes escriben una pequeña especificación LAWS.bend; la IA (o humanos) escribe el resto; el compilador verifica que todo el código satisfaga las leyes.
  • Se comercializa explícitamente para el mundo “post-AGI” y para agentes de codificación basados en LLM.

Historial del repositorio, confianza y código generado por IA

  • Preocupa mucho que el repositorio de GitHub se haya reducido a un solo commit, borrando historial, bifurcaciones y reproducibilidad; se percibe como un problema de confianza, especialmente dadas las grandes afirmaciones.
  • Más tarde se restauró el historial tras las críticas; algunos sostienen que se exageró, otros lo ven como crucial para la auditabilidad y los benchmarks.
  • Partes significativas del compilador y la documentación fueron generadas o ayudadas por LLMs; algunos lo ven como normal, otros como “AI slop” y una señal de alarma cuando se combina con afirmaciones grandilocuentes.

Sistema de tipos, pruebas y “leyes”

  • Bend usa tipos lineales/afines y universos indexados por cantidad, prohibiendo la clonación en tiempo de ejecución de cierres para garantizar terminación y un buen comportamiento en GPU.
  • Las leyes son esencialmente invariantes/pruebas verificadas en tiempo de compilación; las pruebas se contrastan explícitamente con los tests, ya que no ofrecen las mismas garantías.
  • Varios comentaristas señalan el problema clásico: especificar leyes correctas y no vacías para sistemas grandes es al menos tan difícil como escribir el código.
  • Riesgo de “programación por espacio negativo”: la IA satisface las leyes cambiando el problema (por ejemplo, reglas de movimiento del juego, tamaño del mundo) en lugar de reflejar la intención del usuario.

Rendimiento, historia de GPU y comparaciones

  • Las afirmaciones de una verificación de pruebas entre órdenes de magnitud más rápida que Lean/Agda/Isabelle se reciben con escepticismo:
    • Bend evita la unificación, las tácticas y la inferencia, por lo que las comparaciones con elaboradores de funciones completas se consideran engañosas.
    • El uso de GPU actualmente es para paralelismo en tiempo de ejecución; la verificación de pruebas en GPU en tiempo de compilación es “todavía no”.
  • A algunos les interesa el linaje de interaction nets/HVM; otros señalan que Bend 2 es arquitectónicamente diferente del trabajo anterior.

Diseño del lenguaje, ergonomía y documentación

  • La documentación (GUIDE) es elogiada por su ambición, pero criticada por ser confusa:
    • Preguntas sobre argumentos eliminados, parámetros Kind, sintaxis de arrays y tipos sorprendentes como Array<T> & U32.
    • Los arrays/la linealidad conducen a API poco intuitivas (lecturas que devuelven (array, value)), algo que se reconoce que probablemente necesite rediseño.
  • La falta de tácticas e inferencia hace que las pruebas sean verbosas; la postura del autor es que la verbosidad es aceptable si la IA escribe las pruebas.

Adopción, ecosistema y alternativas

  • Preocupan:
    • La stdlib pequeña, la falta de bibliotecas matemáticas y la dificultad de portar grandes pruebas existentes desde sistemas como Cubical Agda.
    • Herramientas ausentes o incipientes (changelogs, releases, integración con lenguajes existentes).
  • Algunos están entusiasmados y experimentando (por ejemplo, portando pequeñas apps, planificadores de reuniones); otros prefieren herramientas existentes como Lean, Coq, Dafny, Verus o contratos de tipo de prueba en lenguajes convencionales.
  • Varios señalan que se trata de investigación/ingeniería prometedora en fase temprana, pero que el marketing actual exagera la madurez y el alcance.