메뉴
HN
Hacker News • 8일 전

Bend – 증명으로 AI 실수를 차단하는 CPU·GPU 프로그래밍 언어

IMP
7/10
핵심 요약

Bend는 C 수준의 속도로 네이티브 코드를 생성하고 CUDA 병렬화를 지원하며, Lean·Rocq 스타일의 증명 검사기를 통해 AI가 작성한 코드가 '법칙(LAWS.bend)'을 위반하지 않음을 수학적으로 보장하는 프로그래밍 언어입니다. AI 에이전트가 매 변경마다 1초 이내에 검증할 수 있어, 코드를 읽지 않고도 AI 생성 코드를 신뢰할 수 있게 하는 것이 핵심입니다.

번역된 본문
  1. 설치 curl -fsSL https://bend-lang.com/install.sh | sh

  2. AGENTS.md에 다음을 추가하세요: Bend 사용 시:

  • bend guide를 실행하여 언어를 학습할 것
  • 중요한 규칙은 LAWS.bend에 보관할 것
  • 커밋 전에 bend PROOF.bend를 실행할 것
  • 가능하면 항상 코드를 병렬화할 것
  1. 버그 없고 빠른 바이브 코딩 앱을 즐기세요!

Bend: 증명을 통해 AI의 실수를 차단하는 빠른 언어 C 수준 속도 · CUDA 병렬성 · Lean 스타일 증명

포스트-AGI 경제에서 인간은 결국 코드를 직접 쓰고 읽는 일을 그만두겠지만, 우리 주변 세상을 만드는 AI에게 무엇을 원하는지 모호함 없이 전달할 방법은 여전히 필요합니다. '법칙(laws)'을 통해 우리의 의도를 자연어보다 훨씬 정확하게 표현할 수 있습니다. '증명(proofs)'을 통해 AI가 프롬프트를 올바르게 구현했는지 검증할 수 있습니다. 그리고 빠른 컴파일러가 이를 고속으로 실행합니다. 그것이 바로 Bend입니다.

  1. Bend는 빠르게 실행됩니다. Bend는 네이티브 코드로 컴파일됩니다. 단일 코어에서는 C와 거의 동등한 속도로 실행됩니다. 동일한 바이너리가 16개 코어 또는 GPU에서도 실행되어 단일 코어 대비 최대 100배 빨라집니다.

  2. Bend는 빠르게 컴파일됩니다. Bend의 타입 검사기는 Lean이나 Rocq처럼 증명 검사기입니다. 그런 도구들은 중간 규모 코드베이스에서 수 분이 걸리지만, Bend는 최대 1초 밖에 걸리지 않아 AI 에이전트가 매번 변경 후에 검사할 수 있습니다.

  3. Bend는 병렬입니다. 스레드도, 락(lock)도, 커널도 작성할 필요가 없습니다. 작업을 둘로 나누면 Bend가 사용 가능한 모든 코어에 호출을 분산한 뒤 다시 합칩니다. pow2가 4,096개의 GPU 코어에서 실행되는 것을 확인해 보세요.

  4. Bend는 증명으로 실수를 차단합니다. 읽어보지 않은 코드를 어떻게 신뢰할 수 있을까요? 증명을 요구하면 됩니다. LAWS.bend에 법칙을 선언합니다. 그 순간부터 어떤 AI도 법칙을 위반하는 코드를 한 줄이라도 배포할 수 없습니다.

게임을 지키는 모습을 보세요: 새 기능 요청: "Claude, 보드가 화면 끝에서 반대편으로 이어지게 해줘" LAWS.bend가 없으면 버그가 그대로 배포됐습니다. LAWS.bend가 있으면 AI는 벽을 만들고 법칙이 유지됨을 증명할 때까지 재시도해야 했습니다. 버그가 병합되는 것은 수학적으로 불가능합니다. 그것은 정리(theorem)이기 때문입니다.

LAWS.bend 예시:

법칙: 어떤 이동 조합으로도 승리할 수 없다.

law you_cant_win : for moves: List # 어떤 이동 순서라도 board = replay(start(), moves) # 시작부터 재생하면 is_won(board) == False {} # 절대 승리로 이어지지 않는다

PROOF.bend 예시:

증명: you_cant_win이 성립한다.

def Laws.you_cant_win (moves):

... AI가 작성함

LAWS.bend는 증명이 뒷받침하는 AGENTS.md입니다. "실수하지 마라"가 이제 타입 검사됩니다. 의심스러우면 직접 게임을 깨보세요.

  1. 시작하기 5.1. 설치 curl -fsSL https://bend-lang.com/install.sh | sh

5.2. 에이전트에게 Bend를 사용하라고 알려주기 AGENTS.md에 다음을 추가하세요: Bend 사용 시:

  • bend guide를 실행하여 언어를 학습할 것
  • 중요한 규칙은 LAWS.bend에 보관할 것
  • 커밋 전에 bend PROOF.bend를 실행할 것
  • 가능하면 항상 코드를 병렬화할 것

그다음 그냥 "use Bend"라고 말하면 됩니다!

5.3. 버그 없고 빠른 바이브 코딩 앱을 즐기세요!

팁: 절대 깨지면 안 되는 것에 대한 법칙을 작성해 달라고 요청하고, 빠르게 실행하고 싶은 모든 것을 병렬화해 달라고 하세요. Bend는 아직 초기 단계이므로 문제가 생기면 이슈를 열어달라고 요청하세요. Bend는 백엔드, Linux, macOS에서 가장 잘 작동합니다. 즐기세요! <3

  1. 참고자료 가이드: GUIDE.md가 언어 전체이며, bend guide로 출력됩니다. 논문: BendTT – 아핀 종속 타입 이론, Bend의 핵심. 논문: BendRT – CPU와 GPU를 위한 병렬 런타임, VM. Bend는 계속 발전 중입니다. 버그가 있을 수 있으니 제보해 주세요.
원문 보기
원문 보기 (영어)
× 1. Install curl -fsSL https://bend-lang.com/install.sh | sh 2. Add this to your 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 3. Enjoy bug-free, fast vibe-coded apps! Bend a fast language that blocks AI mistakes via proof C speed · CUDA parallelism · Lean proofs In the post-AGI economy, humans will eventually stop writing and reading code, but we still need an ambiguity-free way to tell the AIs building the world around us what we want done. With laws , our intents can be much more precise than natural language. With proofs , we can verify that the AI implemented our prompts correctly. And a fast compiler runs it at speed. That's Bend - and nothing else. 1. Bend runs FAST . Bend compiles to native code. On one core, it runs nearly as fast as C. The same binary also runs on sixteen cores, or on the GPU, running up to a hundred times faster than one core. 2. Bend compiles FAST . Bend's type checker is a proof checker, as in Lean and Rocq. Those can take minutes on a mid-sized codebase. Bend takes a second at most, so an AI agent can check after every change. 3. Bend is PARALLEL . No threads, no locks, no kernels to write. Split the work in two, and Bend spreads the calls over every core it can find, then joins them back. Now watch pow2 run on 4,096 GPU cores: 4. Bend BLOCKS mistakes - with proof How can you trust code you never read? By demanding a proof . LAWS.bend is where you declare laws. From then on, no AI can ship one line that breaks them, ever. Watch it guard a game: New feature: “Claude, make the board wrap around” Without LAWS.bend, the bug went live. With LAWS.bend, the AI had to retry until it built a wall and proved the law holds. Merging a bug is mathematically impossible: it is a theorem . LAWS.bend # LAW: no move sequence leads to victory. law you_cant_win : for moves: List<Move> # any sequence of moves board = replay(start(), moves) # replayed from the start is_won(board) == False {} # never leads to victory PROOF.bend # PROOF: you_cant_win holds. def Laws.you_cant_win (moves): # ... written by the AI LAWS.bend is AGENTS.md backed by proof . “Make no mistakes” is now type-checked . Skeptical? Try breaking the game. 5. Get started. 5.1. Install curl -fsSL https://bend-lang.com/install.sh | sh 5.2. Tell your agent to use Bend Add this to your 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 Then, just say: "use Bend"! 5.3. Enjoy bug-free, fast vibe-coded apps! Hints: ask it to write laws for whatever should never break, and to parallelize everything you want running fast. Bend is young: if anything goes wrong, ask it to open an issue. Bend works best on the back-end, on Linux and on macOS. Enjoy! <3 6. References. Guide: GUIDE.md is the whole language; bend guide prints it. Paper: BendTT , an affine dependent type theory, Bend's core. Paper: BendRT , a parallel runtime for CPUs and GPUs, the VM. Bend is still evolving. Expect bugs, and please report them .