18 de septiembre de 2026 Bend sirve como un ejemplo útil de mi punto general respecto al vibe-coding, ya que es reciente, de alto perfil y tiene aspectos que lo hacen fácil de usar como ejemplo. No sé nada sobre el historial del autor en el diseño de lenguajes o si realmente consideró los intercambios a continuación y tomó lo que creo es una mala decisión. Siéntase libre de reemplazar “el autor” abajo con “un autor hipotético que podría haber creado lo mismo”.

Obviamente no me gusta el diseño tomado en Bend y quería presentar eso, sin embargo eso ha sido excesivamente confundido con el punto principal que intento hacer abajo. No quiero editar esto ahora y hacer que parezca que cualquier comentario existente está siendo excesivamente severo, así que siento que la mejor solución es explicar cuál era mi modelo mental del artículo mientras lo escribía. Aquí está un comentario del autor de Bend.

Bend 2 se está promocionando como un lenguaje para la era de la codificación con IA: los humanos escriben “leyes”, la IA escribe implementaciones y pruebas, y el compilador verifica que las pruebas sean sólidas. Todo eso suena bastante impresionante y puedo ver por qué alguien querría un lenguaje que haga eso. En realidad hay algunos problemas mayores con esta idea; sin embargo, eso no es de qué trata este artículo.

En cambio, quiero hablar sobre cómo Bend mismo parece haber caído en una trampa común con el vibe-coding que no veo mencionada mucho. Empecemos con una línea base de lo que Bend requiere que el desarrollador escriba para su demostración en la página principal:https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend No lo reproduciré aquí porque el código no es demasiado importante. Lo importante para este artículo es que es bastante código.

Son 58 líneas de código solo para afirmar que el jugador nunca puede tocar la bandera o ganar el juego. También hay otros problemas en que el LLM puede redefinir los subprogramas de Game para hacer cualquier cosa; sin embargo, eso nuevamente no es el punto del artículo. A continuación, veamos qué necesita escribir el LLM que está escribiendo el código para este programa para probar las “leyes”:https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend Eso es mucho.

Son 442 líneas de código para probar esas propiedades simples. Entonces, ¿cuál es el problema que tengo con esto? ¿Por qué lo llamo una trampa de vibe-coding? El problema es que el vibe-coding hace posible construir una solución sustancial antes de aprender lo suficiente sobre el problema para reconocer que existe una solución mucho mejor. Un desarrollador puede producir un lenguaje y un compilador enteros mientras pasa por alto un enfoque que una encuesta introductoria del campo habría puesto directamente frente a ellos.

El campo en cuestión es la verificación formal. Es notable que esas dos palabras no aparecen en ninguna parte en la página web de Bend ni en su base de código. El desarrollador ha construido un lenguaje entero alrededor de un campo aparentemente sin darse cuenta de que dicho campo existe.

Para demostrar claramente por qué esto es un problema, recreemos el mismo programa que Bend usa como demostración en SPARK, un lenguaje y compilador de código abierto para verificación formal. Para ser justo con Bend, yo mismo vibe-codifiqué esto, simplemente le dije a un LLM que recreara la demostración en SPARK sin más orientación:package Game with SPARK_Mode issubtype Column is Integer range 0 .. 11;subtype Row is Integer range 0 .. 7;type State is record X : Column; Y : Row; Won : Boolean;end record; Start : constant State := (8, 5, False);function Wall (X : Column; Y : Row) return Boolean is(((X = 3 or X = 11) and Y <= 3)or ((Y = 3 or Y = 7) and X <= 3));function Cell (X : Column; Y : Row) return Character is(if Wall (X, Y) then '#' elsif X = 1 and Y = 1 then 'F' else '.');-- Inductive invariant: outside the sealed room, off walls, not won.function Safe (G : State) return Boolean is((G. X > 2 or G.

Y > 2) and not Wall (G. X, G. Y) and not G.

Won)with Ghost;procedure Step (G : in out State; Key : Character)with Post => (if Safe (G'Old) then Safe (G));-- Both Bend laws, including the actual cell drawn by the terminal.function Replay (Keys : St...