Bend 2와 바이브 코딩의 함정

바이브 코딩은 문제를 충분히 이해하기 전에 큰 규모의 해법을 완성하게 해, 기존에 더 나은 접근법이 있다는 사실을 놓치게 할 수 있음 Bend 2는 사람이 법칙을 작성하고 AI가 구현과 증명을 만들면 컴파일러가 증명의 타당성을 검사하는 언어지만, 데모의 단순한 속성에도 긴 명세와 증명이 필요함 데모에서 플레이어가 깃발에 닿거나 게임에서 이길 수 없다는 조건을 명시하는 데 58줄, 이를 증명하는 데 442줄이 쓰임 같은 데모를 SPARK로 재현한 예제는 별도의 장황한 증명을 LLM에 작성시키지 않고도 GNATprove로 12개 검사를 모두 증명함 문제는 구현 속도 자체보다 사전 조사 없이 설계를 굳히는 것에 있음. 기존 분야의 도구와 접근법을 알아야 LLM에도 더 나은 요구를 할 수 있음 Bend를 사례로 삼는 범위 Bend는 최근의 주목도 높은 사례이며 비교하기 쉬운 특성이 있어, 바이브 코딩의 일반적인 함정을 살펴보는 대상으로 쓰임 Bend 개발자의 언어 설계 이력이나 아래의 절충점을 실제로 검토했는지는 확인되지 않음 따라서 개발자의 지식이나 의도를 확정하기보다는, 같은 결과물을 만들 수 있는 가상의 개발자에게도 적용되는 비판으로 읽을 필요가 있음 Bend 2는 AI 코딩 시대의 언어를 지향함 사람은 법칙을 작성하고, AI는 구현과 증명을 작성하며, 컴파일러는 증명의 타당성을 검사함 이 구상 자체의 다른 문제점보다, 언어를 만드는 과정에서 기존 해법을 놓칠 수 있다는 점에 초점을 맞춤 단순한 속성에 필요한 긴 명세와 증명 홈페이지 데모의 LAWS.bend는 플레이어가 깃발에 닿을 수 없고 게임에서 이길 수 없음을 명시하는 데 58줄의 코드를 사용함 LLM이 해당 법칙을 증명하기 위해 작성하는 PROOF.bend는 442줄에 달함 LLM이 Game 하위 프로그램을 임의의 동작으로 재정의할 수 있다는 별도의 문제도 있으나, 이번 비교의 중심은 아님 구현보다 앞서야 할 분야 탐색 바이브 코딩의 함정은 문제를 충분히 배우기 전에 상당한 규모의 해법을 만들 수 있다는 데 있음 해당 분야를 입문 수준으로 훑기만 해도 만날 접근법을 놓친 채, 언어와 컴파일러 전체를 구현할 수 있음 이 사례에서 관련 분야는 정형 검증(formal verification) 임 Bend 웹페이지와 코드베이스에는 이 용어가 나타나지 않음 해당 분야를 중심으로 언어를 만들면서도 기존 분야와 접근법을 인식하지 못한 듯한 결과가 나옴 SPARK로 재...