HigherOrderCO 의 빅터 타엘린이 9월 17일 공개한 Bend 2 는 Bend 1·HVM 과 호환되지 않는 새 언어로, LAWS.bend 에 적은 규칙을 PROOF.bend 의 증명으로 지키게 하고 타입 검사기가 Lean 처럼 증명 검사기 역할을 하며 C·CUDA·Metal·자바스크립트로 컴파일돼요. 저장소 README 는 「컴파일러(커널 제외)는 99% AI 가 썼고 아직 완전히 감사되지 않았다」「Lean 형식화와 구현이 어긋난다」고 적어 두었고, 공개 당시 커밋 이력을 한 개로 뭉갠 것이 지적되자 타엘린이 이력을 복구하고 사과했어요. 다음 날 리엄 파웰이 올린 「Bend 2 와 바이브 코딩 함정」은 데모에서 규칙 58줄에 증명 442줄이 붙는 점을 들어 LLM 으로 빨리 만들 수 있으니 SPARK 같은 자동 증명기 기반 기존 도구를 조사하지 않은 설계라고 비판했는데, 타엘린은 형식 검증을 10년 해 왔고 증명이 장황한 것은 속도를 위한 의도적 설계라고 반박했고 파웰은 SPARK 비교 예제를 LLM 에 그대로 맡겨 만들었다고 밝히며 Bend 는 일반론의 예시일 뿐이라는 주석을 글 상단에 달았어요.
용어 풀이
- HVM
- Higher-order Virtual Machine. Bend 1 이 돌던 HigherOrderCO 의 병렬 실행 엔진
- SPARK
- Ada 언어의 형식 검증용 부분집합. 자동 증명기 GNATprove 로 성질을 검사
- SMT
- Satisfiability Modulo Theories. 논리식의 참·거짓을 자동으로 판정하는 풀이기 계열
- LLM
- Large Language Model, 대규모 언어 모델
- CUDA
- 엔비디아 GPU 에서 범용 계산을 돌리는 플랫폼
운영자 인사이트
「AI 실수를 증명으로 막는다」는 도구를 검토할 때는 도구 자체가 검증됐는지(컴파일러 99% AI 작성·감사 전·형식화와 구현 불일치)와 규칙 한 줄에 증명 몇 줄이 붙는지를 따로 봐야 하고, SMT 자동 증명기 기반 SPARK·Dafny 와의 우열은 양쪽 예제를 모두 LLM 이 쓴 상태라 아직 결론이 없어요.
여러 관점으로 보기
- 프로젝트 주장 타입 검사기가 Lean·Rocq 처럼 증명 검사기라서 LAWS.bend 를 어기는 코드는 「병합이 수학적으로 불가능하다」고 소개하고, GPU 에서 한 코어보다 최대 100배 빠르다고 적어요. Bend
- 프로젝트 주장 저장소 README 가 「Bend 2 는 새 언어라 Bend 1·HVM 은 이어지지 않는다」「컴파일러(커널 제외)는 99% AI 가 썼고 아직 완전히 감사되지 않았다」고 적어 두었고, 라이선스는 아파치 2.0 이에요. GitHub
- 비판 리엄 파웰은 데모의 규칙 58줄에 증명 442줄이 붙는 점을 들어, LLM 으로 빨리 만들 수 있으니 자동 증명기 GNATprove 를 쓰는 SPARK 같은 기존 도구를 조사하지 않고 설계했다고 비판했고, SPARK 예제는 자기도 LLM 에 그대로 맡겨 만들었다고 밝혔어요. Liam Powell's Blog
- 커뮤니티 반응 타엘린은 7년 전 DevCon 형식 검증 발표와 2018년 Formality 를 들어 「그 분야를 모른다」는 비판을 반박하고 증명이 장황한 것은 속도를 위한 의도적 설계이며 어려운 설계 결정은 자기가 한 뒤 LLM 으로 코드를 채운다고 적었고, 파웰은 일반론과 Bend 비판을 뒤섞었다고 인정했어요. Hacker News
- 커뮤니티 반응 공개 당일 토론에서는 커밋 이력을 한 개로 뭉개 벤치마크 SHA 를 재현할 수 없다는 지적, 규칙이 덜 정해져 있어 AI 가 규칙은 지키면서 게임 자체를 바꿨다는 지적, GPU 가 증명 검사에 도움이 되는지 불분명하다는 지적이 나왔고 직접 설치해 돌려 본 보고는 없었어요. Hacker News