Bend - CPU와 GPU에서 증명으로 AI의 실수를 차단하는 언어

Bend는 지켜야 할 규칙을 코드로 선언하고 AI가 구현의 정확성을 증명하도록 하는 언어로, 자연어보다 정밀한 요구사항과 빠른 실행을 결합함 네이티브 코드로 컴파일하며, 단일 코어에서 C에 가까운 속도로 실행되고 같은 바이너리를 여러 CPU 코어나 GPU에서도 실행할 수 있음 타입 검사기가 증명 검사기 역할을 하며, 제네릭 인스턴스화 3,200개 비교에서 검사 시간이 0.38초로 AI 에이전트가 변경할 때마다 검증할 수 있음 자동 병렬화를 지원해 작업을 둘로 나누면 사용 가능한 코어에 호출을 분산하고 결과를 합치므로, 스레드, 잠금, GPU 커널을 직접 작성할 필요가 없음 LAWS.bend에 선언한 규칙을 증명으로 지키도록 하지만, Bend 자체는 아직 발전 중이며 버그가 있을 수 있음 실행 성능과 증명 검사 Bend는 사람이 코드를 쓰거나 읽지 않게 될 미래에도 AI에 원하는 동작을 모호함 없이 전달할 방법이 필요하다는 구상에서 출발함 규칙으로 의도를 자연어보다 정밀하게 명시하고, 증명으로 AI가 요구사항을 올바르게 구현했는지 검증하며, 빠른 컴파일러로 실행함 네이티브 컴파일을 지원하며, 같은 바이너리를 단일 코어, 16개 코어, GPU에서 실행할 수 있음 Apple M4 Max의 Game of Life 비교: TypeScript 18.8초, Lean 13.8초, C 6.78초, Bend 단일 코어 7.80초를 기록함 Bend 16코어는 0.65초로 단일 코어 대비 12배, GPU는 0.06초로 124배 빠름 타입 검사와 증명 검사를 통합하며, 중간 규모 코드베이스에서 수분이 걸릴 수 있는 Lean/Rocq와 달리 최대 1초 내 검사를 내세움 Apple M4 Max에서 제네릭 인스턴스화 3,200개를 비교한 결과 Isabelle과 Agda는 각각 5분 초과, Lean은 19.2초, Rocq는 6.04초, Bend는 0.38초를 기록함 빠른 검사를 통해 AI 에이전트가 변경할 때마다 검증할 수 있음 병렬 실행은 작업을 둘로 나누면 호출을 사용 가능한 코어에 분산하고 다시 합치는 방식임 스레드, 잠금, 커널을 직접 작성할 필요가 없으며, pow2.bend를 GPU 코어 4,096개에서 실행하는 시연을 제공함 규칙으로 AI 구현을 검증하는 개발 흐름 LAWS.bend 에 반드시 지킬 규칙을 선언하고, AI가 PROOF.bend 에 해당 규칙이 성립한다는 증명을 작성함 AGENTS.md의 지시를 증명으로 뒷받침하는 ...