Bend 2 and the Vibe-Coding Trap

Bend 2 позиционируется как язык для эпохи AI-кодинга: человек пишет «законы», а ИИ генерирует реализации и доказательства, которые компилятор проверяет на корректность. Однако автор статьи указывает, что в демонстрации Bend для простого свойства — что игрок никогда не коснётся флага и не выиграет игру — требуется 58 строк кода для формулировки законов и целых 442 строк для их доказательства ИИ. Это выглядит избыточно, особенно если сравнить с существующими подходами в формальной верификации.

Автор показывает, что эквивалентную задачу можно решить гораздо проще на SPARK — языке с встроенной поддержкой формальной верификации. После указания типов, инвариантов и условий, достаточно запустить GNATprove, который подтверждает корректность программы за 12 проверок без необходимости писать громоздкие доказательства вручную или через ИИ. Это демонстрирует, что Bend изобретает велосипед, игнорируя десятилетия исследований в области формальной верификации, термины которой даже не упоминаются на его сайте или в коде.

Основная проблема — не в самом Bend, а в явлении «vibe-coding»: когда разработчик, вдохновлённый возможностями ИИ, сразу приступает к созданию сложной системы (языка, компилятора), не проверив, существует ли уже эффективное решение. ИИ с радостью поможет построить что-то с нуля, но не подскажет, что 99% работы уже сделано и доступно для переиспользования. В результате получается решение, которое работает, но является избыточным и устаревшим по сравнению с текущим состоянием области. Это не просто плохой дизайн — это системная рискованная практика, когда отсутствие предварительного исследования приводит к изобретению хуже существующего.

Комментарии (235)

Обсуждение опровергает утверждение статьи о незнании автором Bend формальной верификации: он публиковал работы и доклады по этой теме за последние 7–8 лет, включая реализацию Cedille Core и выступления на DevCon. Критика Bend за использование 442 строк доказательства некорректна: современные системы вроде Isabelle/HOL и Lean имеют доказательства в десятки тысяч строк — размер не показатель неэффективности. Сравнение Bend с GNATprove некорректно: SMT-решатели автоматически генерируют доказательства, но не масштабируются на сложные системы, тогда как Bend пытается использовать LLM для генерации символьных доказательств — это ново. Vibe-coding позволяет быстро создавать рабочие решения, но мешает осознать, что существуют более эффективные подходы, особенно без предварительного исследования. Проблема не в Bend, а в том, что LLM не предупреждают о существующих решениях — пользователь должен сам запрашивать prior art, иначе повторяет уже решённые задачи. Совет: перед созданием языка или фреймворка стоит начинать с запроса к LLM о существующих решениях — это экономит время и предотвращает повторение известных подходов. Формальная верификация не требует упрощения синтаксиса — её сложность обусловлена природой задачи, и LLM могут помочь управлять этой сложностью, а не заменять её. Критика Bend как «ужасно устаревшего» — это стратегический соломенный человек: автор не игнорирует поле, а пытается сделать его доступнее, что требует иного подхода к UX, а не к теории. Компилятор Bend, написанный на 99% ИИ и не аудитированный, — серьёзный риск, но он не опровергает идею языка, а лишь указывает на необходимость более осторожной реализации. Пользователи не требуют идеальных решений — если работоспособное решение решает их задачу, то 442 строки доказательства не являются препятствием, особенно в корпоративной среде. Совет: лучший язык для взаимодействия с LLM — не компилируемый, а интерактивный, как Lisp, потому что доказательства требуют итеративной корректировки, а не однократной генерации. Попытки создать новый язык из-за недовольства существующими часто приводят к худшим результатам, если не основаны на глубоком понимании предметной области и её исторического контекста. Самая большая опасность vibe-coding — уверенность в том, что сгенерированное решение уникально и лучше, тогда как оно часто является переоткрытием уже существующего. Критики Bend не провели базовое исследование о его авторе — это пример vibe-coding в критике: судят по внешнему виду, а не по содержанию. Совет: вместо осуждения попыток инноваций следует фокусироваться на том, как сделать их более осознанными: исследование, прозрачность и признание существующих работ — ключ к уважаемым проектам.