18 сентября 2026 г. Bend служит полезным примером моего общего утверждения относительно виб-кодинга, поскольку он недавний, высокопрофильный и имеет аспекты, которые делают его удобным для использования в качестве примера. Я ничего не знаю об истории автора в проектировании языков или действительно ли он рассматривал компромиссы ниже и сделал то, что я считаю плохим выбором. Не стесняйтесь заменить «автора» ниже на «гипотетического автора, который мог бы создать то же самое». Очевидно, мне не нравятся проектные решения, принятые в Bend, и я хотел бы их представить, однако это было чрезмерно смешано с основной мыслью, которую я пытаюсь донести ниже. Я не хочу редактировать это сейчас и создавать впечатление, что любые существующие комментарии являются чрезмерно строгими, поэтому я считаю, что лучшее решение — объяснить, какая была моя мысленная модель статьи во время её написания. Вот комментарий автора Bend. Bend 2 позиционируется как язык для эпохи ИИ-кодинга: люди пишут «законы», ИИ пишет реализации и доказательства, а компилятор проверяет, что доказательства корректны. Всё это звучит довольно впечатляюще, и я могу понять, почему кому-то может понадобиться язык, который делает это. На самом деле есть несколько серьезных проблем с этой идеей; однако это не то, о чём эта статья. Вместо этого я хочу поговорить о том, как Bend, кажется, попал в распространённую ловушку виб-кодинга, которую я редко вижу упомянутой. Давайте начнём с базового уровня того, что Bend требует от разработчика написать для своей демонстрации на главной странице:https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend Я не буду воспроизводить его здесь, потому что код сам по себе не слишком важен. Что важно для этой статьи, так это то, что это довольно много кода. Всего 58 строк кода просто чтобы указать, что игрок никогда не может коснуться флага или выиграть игру. Также есть другие проблемы в том, что LLM может переопределить подпрограммы Game, чтобы делать что угодно; однако это опять же не является сутью статьи. Далее, посмотрим, что LLM, пишущий код для этой программы, должен написать, чтобы доказать «законы»:https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend Это много. 442 строки кода, чтобы доказать эти простые свойства. Так в чём же моя проблема с этим? Почему я называю это ловушкой виб-кодинга? Проблема в том, что виб-кодинг позволяет создать существенное решение, прежде чем достаточно узнать о проблеме, чтобы осознать, что существует гораздо лучшее решение. Разработчик может создать целый язык и компилятор, упуская подход, который вводный обзор области поместил бы прямо перед ними. Область в вопросе — формальная верификация. Заметно, что эти два слова нигде не появляются на веб-странице Bend или в его кодовой базе. Разработчик создал целый язык вокруг области, seemingly не осознавая, что эта область существует. Чтобы чётко продемонстрировать, почему это проблема, давайте воссоздадим ту же программу, которую Bend использует в качестве демонстрации, в SPARK — открытом языке и компиляторе для формальной верификации. Чтобы быть справедливым по отношению к Bend, я сам виб-кодил это, просто сказав LLM воссоздать демонстрацию в SPARK без дополнительных указаний: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...