벤드 2와 바이브 코딩의 함정
1. 이게 뭔가요?
이 기사는 인공지능을 활용해 코드를 작성하는 시대에 만들어진 벤드 2라는 프로그래밍 언어와, 인공지능에 의존할 때 빠지기 쉬운 함정을 다룹니다. 벤드 2는 사람이 규칙을 적으면 인공지능이 실제 작동하는 코드와 그 규칙이 맞는지 증명하는 코드를 작성하고, 컴파일러가 그 증명이 올바른지 확인하는 방식을 사용합니다. 기사에서 지적하는 문제는 인공지능을 쓰면 깊이 있는 사전 조사나 공부 없이도 대규모 시스템을 빠르게 만들 수 있다 보니, 이미 수십 년 전에 연구되어 온 형식 검증이라는 기존 기술 분야를 놓치고 훨씬 비효율적인 방식을 고안하게 된다는 점입니다.
2. 왜 화제인가요?
이 주제가 주목받는 이유는 인공지능으로 코드를 작성하는 방식이 개발 현장에서 빠르게 늘어나고 있지만, 이 과정에서 치명적인 한계가 드러나기 때문입니다. 인공지능에게 코딩을 맡기면 개발자가 관련 분야를 따로 공부하거나 기존 연구를 찾아보지 않아도 결과물을 쉽게 만들어 낼 수 있습니다. 하지만 이는 개발자가 이미 수십 년 전에 완성된 더 효율적인 표준 기술을 모른 채, 수백 줄에 달하는 장황한 코드를 인공지능에게 일일이 시키는 비효율을 낳을 수 있습니다. 기사는 기존의 검증된 기술인 스파크 언어와 비교하며, 사전 조사 없이 인공지능의 답변에만 의존해 시스템을 구축할 때 발생하는 문제점을 짚어냅니다.
3. 핵심 내용
벤드 2와 바이브 코딩의 함정
2026년 9월 18일
여기서 벤드(Bend)는 최근에 큰 주목을 받았고 예시로 활용하기 좋은 면이 많아서 바이브 코딩에 대한 일반적인 주장을 설명하기 위한 유용한 사례로만 사용합니다. 저는 이 언어를 만든 사람의 과거 프로그래밍 언어 설계 경력에 대해 잘 알지 못하며, 그가 아래에서 언급할 여러 장단점을 실제로 고려했으나 결과적으로 아쉬운 선택을 한 것인지도 알 수 없습니다. 독자 여러분은 아래의 '작성자'라는 표현을 '똑같은 결과물을 만들어 냈을 수 있는 가상의 개발자'로 바꾸어 읽으셔도 좋습니다.
벤드 2는 인공지능(AI) 코딩 시대에 맞춘 프로그래밍 언어로 홍보되고 있습니다. 사람이 규칙인 '법칙'을 작성하면 인공지능이 실제 작동하는 코드인 '구현체'와 그것이 올바르다는 것을 증명하는 '증명' 코드를 작성하고, 컴퓨터의 번역기 역할을 하는 프로그램인 '컴파일러'가 그 증명이 올바른지 확인하는 방식입니다. 이 구상은 매우 인상적이며 누구나 이런 언어를 쓰고 싶어 할 이유를 충분히 이해할 수 있습니다. 하지만 이 아이디어에는 몇 가지 큰 문제가 있습니다. 그렇지만 이번 글의 주제는 그것이 아닙니다. 대신 저는 벤드 자체가 사람들이 자주 언급하지 않는, 바이브 코딩에서 흔히 빠지는 함정에 어떻게 빠진 것처럼 보이는지 이야기하고자 합니다.
먼저 벤드가 공식 홈페이지의 시연 프로그램에서 개발자에게 작성하도록 요구하는 기본 내용부터 살펴보겠습니다.
https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend
코드가 아주 중요하지는 않으므로 여기서는 그대로 옮기지 않겠습니다. 이 글에서 중요한 점은 코드가 꽤 많다는 사실입니다. 플레이어가 결코 깃발에 닿거나 게임에서 이길 수 없다는 규칙 하나를 명시하는 것만으로도 58줄의 코드가 필요합니다. 인공지능 모델인 대형 언어 모델(LLM)이 게임의 하위 프로그램(서브프로그램)을 재정의해 무엇이든 하게 만들 수 있다는 점 등 다른 문제도 있지만, 이 역시 이번 글의 핵심은 아닙니다.
다음으로, 이 프로그램의 코드를 작성하는 대형 언어 모델이 '법칙'이 옳음을 증명하기 위해 무엇을 작성해야 하는지 살펴보겠습니다.
https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend
정말 분량이 많습니다. 고작 단순한 성질들을 증명하기 위해 442줄의 코드가 필요합니다.
그렇다면 제가 이 상황에서 문제 삼는 점은 무엇일까요? 왜 이것을 바이브 코딩의 함정이라고 부를까요?
문제는 바이브 코딩을 하면 훨씬 더 나은 해결책이 존재한다는 사실을 깨달을 만큼 해당 문제에 대해 깊이 알기도 전에, 상당한 규모의 결과물을 먼저 구축해 버리게 된다는 점입니다. 개발자는 해당 분야의 기초적인 조사만 했어도 곧바로 눈앞에 나타났을 접근법을 전혀 모른 채, 언어와 컴파일러 전체를 만들어 낼 수 있습니다.
여기서 문제의 그 분야는 바로 '정형 검증(formal verification)'입니다. 흥미롭게도 이 두 단어는 벤드의 웹페이지나 소스 코드 어디에도 나타나지 않습니다. 개발자는 정형 검증이라는 분야가 존재한다는 사실조차 모른 채 그 분야를 기반으로 하는 언어 전체를 구축한 셈입니다.
이것이 왜 문제가 되는지 명확히 보여 주기 위해, 벤드가 시연에서 사용하는 것과 똑같은 프로그램을 정형 검증을 위한 공개 소스(오픈 소스) 언어이자 컴파일러인 '스파크(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 '.');
-- 귀납적 불변식: 밀폐된 방 바깥, 벽이 아닌 곳, 승리하지 않은 상태. 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));
-- 화면에 그려진 실제 칸을 포함하여 벤드의 두 가지 규칙 모두. 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;
자, 이제 벤드와 똑같은 규칙을 정의했으니, 여기서 제가 하려는 말은 무엇일까요?
이 예시가 벤드와 다른 점은, 인공지능이 1단계 원리부터 442줄짜리 증명을 만드느라 시간과 토큰(인공지능이 처리하는 글자 조각 단위)을 낭비하게 하지 않고 프로그램의 정확성을 증명하는 데 필요한 모든 것을 우리가 직접 제공했다는 것입니다. 이제 '지네트프로브(GNATprove)'라는 프로그램을 실행하면 다음과 같은 결과를 얻을 수 있습니다.
성공: 모든 검증 통과 (12개 검증 항목).
벤드의 개발자는 이 방식이 형식 검증 분야의 현재 표준이라는 점을 전혀 눈치채지 못했습니다. 이 분야가 존재한다는 사실조차 모를 수도 있습니다. 그 대신 장황한 명세와 훨씬 더 장황한 증명이 필요한 시스템을 통째로 만들어냈습니다. 전체 언어와 컴파일러를 바이브 코딩으로 만들기 전에 약간의 조사만 했더라도 무엇을 요구해야 할지 알았을 것이므로 결과물이 훨씬 좋아졌을 것입니다.
이 예시는 벤드에만 국한되지 않고 중요한 의미를 갖습니다. 바이브 코딩을 쓰면 조사를 전혀 하지 않고도 즉시 결과물을 얻을 수 있기 때문에, 심각하게 망가졌거나 수십 년 뒤처진 설계 방식을 너무나 쉽게 구현하게 됩니다. 인공지능에게 기초 원리부터 증명을 쌓아 올려 함수가 형식적으로 올바름을 증명할 수 있는 언어를 만들어달라고 요청하면 인공지능은 기꺼이 그렇게 해줄 것이며, 인공지능의 도움 없이도 컴퓨터가 이미 복잡한 증명을 스스로 만들어내어 99%의 노력을 없애줄 수 있다는 점은 절대 멈춰 서서 제안해주지 않습니다. 또한 지금 만들고 있는 것이 이미 다른 사람들이 해놓은 작업이라 그 위에 얹어서 개발할 수 있다는 사실도 절대 알려주지 않습니다.
4. 나에게 어떤 영향이 있나요?
이 내용은 프로그램을 만드는 개발자와 기술 설계자에게 중요한 시사점을 줍니다. 개발자가 인공지능이 주는 편리함에만 의존해 깊은 공부나 기술 조사를 소홀히 하면, 이미 해결된 문제에 불필요한 노력을 쏟거나 수십 년 뒤떨어진 방식을 채택하게 될 수 있습니다. 따라서 새로운 도구나 언어를 만들거나 도입할 때는 인공지능이 만들어주는 결과물만 믿기보다, 해당 분야의 기존 표준과 연구가 어떻게 되어 있는지 살펴보는 태도가 필요합니다.