Проблема и решение
Bend 2 позиционируется как язык для эпохи AI-кодирования: разработчики пишут «законы», ИИ реализует их и строит доказательства корректности, компилятор проверяет эти доказательства. Звучит впечатляюще, и легко понять, почему кто-то захочет язык с такими возможностями. Но есть серьёзные концептуальные проблемы с этим подходом — однако это не тема данной статьи. Вместо этого стоит обсудить, как сам Bend попал в типичную ловушку vibe-coding, которую редко упоминают.
Начнём с базовой информации: посмотрим, что Bend требует разработчику написать для демонстрации на главной странице:
https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend
Сам код здесь не критичен. Важно, что это довольно объёмный файл — 58 строк кода только для утверждения того, что игрок не может коснуться флага и выиграть. Кроме того, в этом подходе есть проблема: ИИ может переопределить подпрограммы Game так, как ему угодно — но это опять же не главный вопрос статьи.
Теперь посмотрим, что ИИ должен написать, чтобы доказать эти «законы»:
https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend
Это объемно. 442 строки кода, чтобы доказать эти простые свойства.
В чём заключается ловушка vibe-coding?
Проблема в том, что vibe-coding позволяет реализовать существенное решение до того, как разработчик достаточно изучит предметную область и понимает, что существует намного лучший подход. Он может создать полноценный язык и компилятор, так и не узнав об апрохе, который сразу же предложила бы вводная лекция по соответствующей дисциплине.
Речь идёт о формальной верификации. Примечательно, что эти два слова не встречаются ни на веб-сайте Bend, ни в его кодовой базе. Разработчик создал целый язык вокруг области знаний, похоже, не осознав, что эта область вообще существует.
Чтобы наглядно показать, почему это проблема, возьмём ту же игровую программу, которую использует Bend как демонстрацию, и перепишем её на SPARK — открытом языке и компиляторе для формальной верификации. В честность к Bend надо сказать, что я полностью следовал принципу vibe-coding: просто попросил ИИ переписать демо на SPARK без дополнительных указаний:
package Game with SPARK_Mode is
subtype 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 : String) return State
with Post => not Replay'Result.Won
and Cell (Replay'Result.X, Replay'Result.Y) /= 'F';
end Game;
------------------------------
package body Game with SPARK_Mode is
procedure Step (G : in out State; Key : Character) is
X : Column := G.X;
Y : Row := G.Y;
begin
case Key is
when 'w' => Y := (Y - 1) mod 8;
when 's' => Y := (Y + 1) mod 8;
when 'a' => X := (X - 1) mod 12;
when 'd' => X := (X + 1) mod 12;
when others => return;
end case;
if not Wall (X, Y) then
G := (X, Y, G.Won or Cell (X, Y) = 'F');
end if;
end Step;
function Replay (Keys : String) return State is
G : State := Start;
begin
for Key of Keys loop
pragma Loop_Invariant (Safe (G));
Step (G, Key);
end loop;
return G;
end Replay;
end Game;
------------------------------
with Ada.Text_IO; use Ada.Text_IO;
with Game; use Game;
procedure Main is
G : State := Start;
begin
Put_Line ("Winning is impossible. WASD + Enter to move; q + Enter to quit.");
loop
for Y in Row loop
for X in Column loop
Put (if X = G.X and Y = G.Y then 'P' else Cell (X, Y));
end loop;
New_Line;
end loop;
Put_Line (if G.Won then "WON (this should be unreachable)" else "still not won");
exit when End_Of_File;
declare
Keys : constant String := Get_Line;
begin
exit when Keys = "q";
for Key of Keys loop
Step (G, Key);
end loop;
end;
end loop;
end Main;Теперь у нас есть те же законы, что и в Bend. В чём смысл этого сравнения?
Отличие в том, что здесь содержится всё необходимое для доказательства корректности программы — ИИ не тратит время и токены на строительство 442-строчного доказательства с нуля. Запускаем GNATprove и получаем:
Success: all checks proved (12 checks).Разработчик Bend полностью упустил, что это — текущий стандарт в области формальной верификации (если вообще знает, что такая область существует). Вместо этого создал целую систему с громоздкими спецификациями и ещё более громоздкими доказательствами. Небольшое исследование перед vibe-coding целого языка и компилятора могло бы существенно улучшить результат, потому что разработчик узнал бы, что на самом деле нужно просить.
Почему это имеет значение
Этот пример важен не только для Bend. Vibe-coding делает слишком легким реализацию проекта, который либо принципиально сломан, либо отстаёт на десятилетия от современного состояния искусства. Можно получить результат немедленно, никогда не проводя никаких исследований. Если попросить ИИ создать язык, в котором можно доказать формальную корректность функции, строя доказательство с базовых принципов — ИИ с удовольствием это сделает. Но ИИ никогда не остановится, чтобы подсказать, что компьютеры уже могут строить сложные доказательства самостоятельно, без помощи LLM, исключая при этом 99% работы. Никогда не скажет, что то, что вы строите, уже в основном существует в виде работ, на которых можно построить.