AI가 코드를 대신 짜는 일이 일상이 되면서, 한 가지 오래된 질문이 다시 무게를 얻고 있다. 사람이 읽지도 않은 코드를 어떻게 신뢰할 것인가. Bend는 이 물음에 '증명(proof)'이라는 답을 들고 나온 실험적 프로그래밍 언어다. 파이썬과 비슷한 문법을 표방하면서 C 수준의 실행 속도, CUDA를 통한 GPU 병렬성, 그리고 Lean·Rocq 계열의 정리 증명 기능을 한데 묶겠다는 것이 프로젝트가 내세우는 목표다. 아직 초기 단계이고 버그가 있을 수 있다는 점을 개발진 스스로 명시하고 있다는 사실도 함께 봐야 한다.
타입 검사기를 증명 검사기로
Bend의 핵심 주장은 타입 검사기가 곧 증명 검사기라는 점이다. Lean이나 Rocq 같은 증명 보조 도구는 중간 규모의 코드베이스에서 검증에 수 분이 걸리기도 하는데, Bend는 길어야 1초 안에 끝난다고 설명한다. 이 속도 차이가 왜 중요한가. AI 에이전트가 코드를 한 줄 고칠 때마다 즉시 검증을 돌릴 수 있느냐 없느냐가 갈리기 때문이다. 검증이 수 분씩 걸리면 개발 루프에 끼워 넣기 어렵지만, 1초면 매 변경마다 자동으로 확인하는 워크플로가 현실적으로 성립한다. Bend의 코어는 BendTT라는 아핀 의존 타입 이론 논문으로, 런타임은 CPU·GPU용 병렬 VM인 BendRT 논문으로 뒷받침된다고 소개된다.
이 언어가 겨냥하는 시나리오는 노골적으로 'AI가 코드를 쓰는 시대'다. 프로젝트 설명은 사람이 결국 코드를 읽고 쓰지 않게 되더라도, AI에게 무엇을 원하는지 모호함 없이 전달할 수단은 여전히 필요하다고 주장한다. 자연어보다 법칙(law)이 더 정밀하게 의도를 표현하고, 증명이 그 구현이 옳았는지 검증하며, 빠른 컴파일러가 이를 속도로 실행한다는 구도다. 이는 형식 검증(formal verification)이라는 오래된 분야를 AI 에이전트 협업이라는 새 맥락으로 옮겨 놓은 시도로 읽힌다.
LAWS.bend, '증명된 AGENTS.md'
가장 눈에 띄는 개념은 LAWS.bend다. 개발자가 절대 깨지면 안 되는 규칙을 이 파일에 법칙으로 선언하면, 그 이후로는 어떤 AI도 그 법칙을 위반하는 코드를 병합할 수 없다는 것이다. 프로젝트는 이를 게임에 적용한 예로 설명한다. LAWS.bend가 없으면 버그가 그대로 배포되지만, 법칙을 걸어 두면 AI는 법칙이 성립함을 증명할 때까지 재시도해야 하고, 버그를 병합하는 것은 수학적으로 불가능한 정리(theorem)가 된다는 논리다. 개발진은 이를 두고 'AGENTS.md를 증명으로 뒷받침한 것', 즉 \"실수하지 마\"라는 지시가 이제 타입 검사되는 것이라고 표현한다.
실무자 입장에서 이 아이디어의 매력은 분명하다. AGENTS.md나 각종 코딩 규칙 문서는 결국 AI가 '지키기를 바라는' 권고에 그치지만, 형식적 법칙은 위반 시 컴파일 자체가 통과되지 않는 강제력을 갖는다. 리뷰어가 놓친 불변 조건이나, 회귀 테스트가 미처 다루지 못한 경계 조건을 타입 수준에서 봉쇄할 수 있다면, 사람이 읽지 못한 대량의 AI 생성 코드에 대한 신뢰 문제를 부분적으로 해소할 여지가 생긴다.
병렬성은 언어가 알아서
성능 측면에서 Bend는 스레드, 락, 커널 작성 없이 병렬화를 지원한다고 강조한다. 작업을 둘로 쪼개면 언어가 찾을 수 있는 모든 코어에 호출을 분산했다가 다시 합친다는 것이다. 같은 바이너리가 단일 코어에서는 C에 가깝게 돌고, 16코어나 GPU에서는 단일 코어 대비 최대 100배 빠르게 실행되며, pow2 예제가 4,096개의 GPU 코어에서 도는 시연이 제시된다. 병렬 프로그래밍의 복잡성을 언어 런타임이 흡수하겠다는 방향은, 동시성 버그가 검증을 가장 어렵게 만드는 영역이라는 점에서 증명 기능과 잘 맞물린다.
다만 냉정하게 볼 지점도 많다. Bend는 스스로 밝히듯 아직 초기 단계이며 버그를 예상하고 이슈 제보를 요청하는 수준이고, 백엔드·Linux·macOS 환경에서 가장 잘 작동한다고 권장 범위를 좁혀 두고 있다. C에 근접한 속도나 100배 가속 같은 수치는 프로젝트 측 주장이며, 실제 워크로드에서의 재현성이나 의존 타입으로 임의의 비즈니스 로직을 얼마나 실용적으로 증명할 수 있는지는 별개의 문제다. 증명 기반 개발의 오랜 난제, 즉 '무엇을 법칙으로 명세할 것인가' 자체가 어렵고, 잘못 쓴 법칙은 잘못된 안전감만 줄 수 있다.
결국 Bend가 흥미로운 이유는 특정 벤치마크 수치보다, AI가 코드를 생산하는 시대에 신뢰를 기술적으로 확보하려는 접근을 구체적 언어 설계로 밀어붙였다는 데 있다. 형식 검증을 다뤄 본 팀이라면 LAWS.bend 개념을 자사 에이전트 파이프라인의 가드레일로 상상해 볼 가치가 있고, 그렇지 않은 팀이라도 '검증 가능한 불변식'을 코드 리뷰의 보조 축으로 삼는 발상은 지금 도구로도 참고할 만하다. 다만 프로덕션 도입을 논하기에는 성숙도와 검증 사례가 아직 부족하므로, 현재로서는 방향성을 관찰하고 소규모로 실험하는 편이 온당하다.