Bend 2 se presenta como un lenguaje de programación para la era de la IA, donde los humanos definen las leyes y la IA genera las implementaciones y pruebas. Sin embargo, el proyecto presenta un problema fundamental: ignora el campo de la verificación formal, que ya existe y permite probar la corrección de software de manera rigurosa. El artículo argumenta que el enfoque de Bend 2 cae en la 'trampa del vibe-coding', un fenómeno donde los desarrolladores construyen soluciones complejas sin reconocer que existen métodos más eficientes y establecidos en la industria.
Para ilustrar esto, el texto compara el demo de Bend 2, que requiere 58 líneas para definir las leyes y 442 líneas para generar la prueba, con una implementación equivalente en SPARK, un lenguaje de verificación formal de código abierto. Al usar SPARK, el código se reduce drásticamente y permite verificar la corrección mediante herramientas estándar como GNATprove, confirmando que las pruebas son válidas. La conclusión es que Bend 2 ha desarrollado un sistema de especificaciones y pruebas excesivamente verboso y redundante, basándose en la creencia de que la IA debe generar todo desde cero. En realidad, la IA puede aprovechar herramientas de verificación formal existentes, lo que eliminaría la gran mayoría del trabajo y evitaría la creación de lenguajes que son décadas por detrás de la tecnología actual. Este error de diseño demuestra cómo el vibe-coding puede llevar a soluciones deficientes si no se realiza la investigación previa necesaria para identificar las mejores prácticas del campo.