Bend: CPU와 GPU에서 AI의 실수를 차단하는 증명 검증 언어

Bend는 AI 생성 코드를 겨냥한 컴파일형 병렬 언어입니다. 핵심 주장은 읽지도 않는 출력을 신뢰하는 대신, LAWS.bend 파일에 법칙을 선언하고 에이전트가 병합 전에 이를 증명하도록 요구한다는 것입니다.

이 제안은 다른 AI 코딩 도구와 비슷해 보이지만 작동 방식은 다릅니다. Bend의 타입 검사기는 증명 검사기로, Lean이나 Rocq와 같은 개념입니다. 강조하는 차이점은 속도입니다. 기존 검사기는 중간 규모 코드베이스에서 몇 분이 걸릴 수 있지만, Bend는 최대 1초를 주장하므로 에이전트가 모든 변경 후 검사를 실행할 수 있습니다.

속도의 원천

• 네이티브 코드로 컴파일됩니다. 단일 코어에서 거의 C 속도에 가깝습니다.
• 동일한 바이너리가 16개 코어 또는 GPU로 확장됩니다. 문서에서는 단일 코어보다 최대 100배 빠르다고 주장합니다.
• 병렬화는 자동입니다. 작업을 둘로 나누면 Bend가 호출을 코어나 GPU 코어에 분산한 후 결합합니다. 스레드, 잠금, 커널 코드가 필요 없습니다.

사이트에는 4,096개 GPU 코어에서 실행되는 pow2.bend 예제가 있습니다.

법칙과 증명 모델

LAWS.bend에 법칙을 작성합니다:

# LAW: no move sequence leads to victory.
law you_cant_win : for moves: List<Move>
    board = replay(start(), moves)
    is_won(board) == False

그런 다음 에이전트가 PROOF.bend에 일치하는 증명을 작성합니다:

# PROOF: you_cant_win holds.
def Laws.you_cant_win (moves):
    # ... written by the AI

법칙이 선언되면 사이트는 에이전트가 이를 위반하는 코드를 병합할 수 없다고 주장합니다. 데모에서는 게임을 사용합니다. Claude에게 보드를 랩어라운드하게 만들어 달라고 요청합니다. LAWS.bend가 없으면 버그가 병합되어 배포됩니다. 있으면 에이전트가 증명을 구축할 때까지 재시도해야 합니다. 출처의 표현: 버그 병합이 "수학적으로 불가능"해집니다.

설정

설치:

curl -fsSL https://bend-lang.com/install.sh | sh

그런 다음 AGENTS.md에 다음 블록을 추가하여 에이전트가 수행할 작업을 알 수 있도록 합니다:

When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible

Bend는 본질적으로 LAWS.bend를 증명으로 뒷받침되는 AGENTS.md로 취급합니다. "실수하지 마"가 타입 검사됩니다.

출처의 주의사항

문서는 솔직합니다. Bend는 젊고 버그가 있을 수 있으니 보고하세요. 백엔드에서 가장 잘 작동하며 Linux와 macOS를 대상으로 합니다. 핵심은 두 논문—BendTT(아핀 의존 타입 이론)와 BendRT(병렬 CPU/GPU 런타임)—에 기반합니다.

누구를 위한 것인가

에이전트가 읽지 않는 코드를 배포하도록 허용하는 팀, 특히 "잔액은 절대 음수가 되지 않는다"와 같은 규칙을 코드 리뷰가 아닌 강제로 시행해야 하는 백엔드 서비스에 적합합니다.