Bend 2, AI가 만든 언어의 함정: 442줄 증명 대신 12줄로 끝낼 수 있었다
Bend 2 and the Vibe-Coding Trap
Bend 2는 AI 코딩 시대를 위한 언어로, 인간이 '법칙'을 쓰면 AI가 구현과 증명을 작성하고 컴파일러가 검증한다고 홍보된다. 그러나 데모에서 플레이어가 깃발에 닿을 수 없음을 보이려면 58줄의 법칙과 442줄의 증명이 필요하다. 저자는 이를 '바이브 코딩 함정'이라 부른다. 형식 검증 분야를 조사했다면 SPARK로 12개 검사만으로 같은 정확성을 증명할 수 있었고, LLM은 기존 연구를 알려주지 않는다.
바이브 코딩은 문제에 대해 충분히 알기 전에 상당한 해결책을 만들어 버릴 수 있게 한다. 그래서 훨씬 더 나은 해결책이 존재한다는 사실을 인식하지 못한 채 말이다.