Bend 2 y la trampa del vibe-coding
Bend 2 and the Vibe-Coding Trap
Bend 2 se presenta como un lenguaje para la era de la IA: los humanos escriben 'leyes', la IA implementa y prueba, y el compilador verifica. Pero el autor señala que el proyecto cayó en una trampa del vibe-coding: construyó un sistema de verificación formal sin saber que la verificación formal ya existe. Recrea la demo en SPARK, un lenguaje de verificación formal, y logra probar todas las propiedades con solo 12 comprobaciones, frente a las 442 líneas de prueba de Bend. El problema: vibe-codear sin investigar lleva a soluciones obsoletas.
El autor de Bend ha pasado por alto por completo que este es el estándar actual en el campo de la verificación formal, si es que siquiera sabe que este campo existe.