Bend 2 угодил в ловушку вайб-кодинга, пропустив десятилетия исследований в формальной верификации
Bend 2 and the Vibe-Coding Trap
Bend 2 позиционируется как язык для эпохи ИИ-кодинга: люди пишут «законы», ИИ — реализации и доказательства, а компилятор проверяет их корректность. Автор разбирает демо на главной странице и показывает, что для доказательства простого свойства «игрок никогда не коснётся флага» требуется 58 строк спецификаций и 442 строки доказательств. Проблема в том, что создатели Bend, похоже, не знают о существовании формальной верификации — области, где те же гарантии достигаются без LLM. Тот же пример на SPARK занимает около 30 строк, а GNATprove подтверждает все 12 проверок автоматически. Это иллюстрирует типичную ловушку вайб-кодинга: LLM позволяет быстро построить решение, не разобравшись в задаче и не узнав, что подобное уже существует.
Вайб-кодинг делает так, что можно построить целое решение, прежде чем узнать достаточно о проблеме, чтобы понять: существует гораздо лучший подход.