Bend — 증명으로 AI의 실수를 막는 고속 프로그래밍 언어

본문

Bend는 '증명으로 AI의 실수를 막는 빠른 언어'를 내세우는 새 프로그래밍 언어입니다. C 수준의 속도, CUDA 기반 병렬 실행, Lean 스타일의 증명을 하나로 묶은 것이 특징입니다. 제작진은 'post-AGI 경제'에서 인간이 결국 코드를 직접 쓰거나 읽지 않게 되더라도, 주변 세계를 만들어가는 AI에게 무엇을 원하는지 모호함 없이 전달할 수단은 여전히 필요하다고 주장합니다. 법칙(law)으로 의도를 자연어보다 정밀하게 표현하고, 증명(proof)으로 AI가 프롬프트를 올바르게 구현했는지 검증한 뒤, 빠른 컴파일러가 그 결과를 실행 속도로 바꿔 준다는 구성입니다.

네이티브 성능과 자동 병렬화

Bend는 네이티브 코드로 컴파일됩니다. 단일 코어에서는 C에 거의 근접한 속도를 내며, 같은 바이너리가 16코어 CPU나 GPU에서도 그대로 동작해 단일 코어 대비 최대 100배까지 빨라진다고 소개합니다. 스레드도, 락도, 직접 작성할 커널도 없습니다. 작업을 둘로 나누기만 하면 Bend가 찾을 수 있는 모든 코어에 호출을 분산시켰다가 다시 합쳐 줍니다. 사이트에서는 pow2 예제가 4,096개의 GPU 코어에서 실행되는 모습을 시연합니다.

타입 검사기 = 증명 검사기

Bend의 타입 검사기는 Lean과 Rocq처럼 증명 검사기입니다. 다만 기존 시스템들은 중간 규모 코드베이스에서도 수 분이 걸릴 수 있는 반면, Bend는 최대 1초면 검사가 끝나므로 AI 에이전트가 매 변경 후에 결과를 확인할 수 있다고 설명합니다.

LAWS.bend — 증명이 뒷받침하는 AGENTS.md

읽지 않은 코드를 어떻게 신뢰할 수 있을까요? 증명을 요구하면 됩니다. LAWS.bend는 법칙을 선언하는 파일이며, 한번 선언하면 어떤 AI도 그 법칙을 어기는 코드 한 줄을 배포할 수 없습니다. 사이트의 게임 예시에서는 '보드를 wrap-around로 만들어 달라'는 요청에, LAWS.bend가 없을 때는 버그가 그대로 라이브에 올라갔지만 있을 때는 AI가 벽을 만들어 법칙이 성립함을 증명할 때까지 재시도했다고 합니다. 버그가 머지되는 것은 수학적으로 불가능하며, 그것이 정리(theorem)라고 강조합니다. 예시 법칙 'you_cant_win'은 임의의 Move 리스트를 처음 상태부터 리플레이했을 때 is_won(board) == False를 요구하는, '어떤 수열로도 승리에 이르지 않는다'는 명제입니다. 제작진은 이를 '증명이 뒷받침되는 AGENTS.md'이며, '실수하지 말 것'이라는 지시가 이제 타입 검사된다고 설명합니다.

사용법과 현재 상태

설치는 curl로 install.sh를 실행하는 한 줄이며, bend guide를 실행하면 언어 전체를 담은 GUIDE.md를 확인할 수 있습니다. AGENTS.md에 'use Bend'를 쓰라는 지시를 추가하고, 절대 깨지면 안 되는 부분에 법칙을 작성하게 하고 빠르게 돌릴 부분은 모두 병렬화하라는 힌트를 제시합니다. Bend는 백엔드와 Linux·macOS에서 가장 잘 동작합니다. 핵심 이론으로 affine dependent type theory인 BendTT와, CPU·GPU용 병렬 런타임(VM)을 다룬 BendRT 논문이 공개돼 있습니다. 다만 아직 발전 중인 언어이므로 버그를 예상하고 이슈로 보고해 달라고 덧붙입니다.

Hacker News 반응

• @boxed — GitHub에 커밋이 하나뿐이고, 어차피 컴파일러도 없습니다. 컴파일러는 어디에 있나요?
• @robinhouston — 저도 이제 막 처음 살펴보는 중이지만, 컴파일러가 github.com/bendlang/bend의 bend2/comp.ts에 있는 것 아닌가요?
• @LightMachine — 컴파일러는 런타임과 함께 comp.ts에 있습니다. 파일이 깔끔한 편은 아니고 지금은 gambiarra(땜질식 임시 코드)와 AI 슬롭이 많습니다. 읽을 가치가 있는 걸 원하면 커널(bend.ts)을 읽어 보세요.
• @tyushk — Victor Taelin의 작업(HVM)이 계기가 되어 저는 컴파일 타깃으로서의 interaction combinator에 관심을 갖게 됐습니다. 지금은 대학 연구의 일환으로 구현을 진행 중입니다. Bend 2.0 릴리스를 보니 반갑네요!
• @etiamz — 그렇다면 interaction nets를 전문으로 다룬 Marc Thatcher의 최근 박사 논문이 흥미로울 겁니다. multiplicative linear logic의 proof nets를 통해 interaction nets를 훌륭하게 설명하고 있고, interaction nets의 생산성 분석 같은 새로운 기여도 담겨 있습니다.

원문: Hacker News / 번역·요약: Trawling