읽지 않은 코드를 믿는 방법 — 증명은 내가 적은 것만 지킨다

이번 주에 네 번 같은 벽에 부딪혔다. 에이전트를 늘리면 늘어나는 건 코드가 아니라 읽어야 할 diff이고, 읽기는 병렬화되지 않는다.

Bend는 그 문제에 지금까지 본 것 중 가장 급진적인 답을 낸다. 홈페이지가 질문을 그대로 적어뒀다.

How can you trust code you never read?

검토를 싸게 만드는 대신 불필요하게 만들겠다는 것이다. 방향은 맞다고 본다. 다만 토론에서 나온 반례 하나가 이 접근의 경계를 정확히 보여준다.

출처: bend-lang.com

확인된 것

홈페이지에서 확인한 것만 적는다.

자기 소개가 한 줄이다.

a fast language that blocks AI mistakes via proof

구성은 "C speed · CUDA parallelism · Lean proofs · Python syntax".
작동 방식: 개발자가 LAWS.bend에 불변식을 쓴다. 홈페이지는 이걸 "증명으로 뒷받침되는 AGENTS.md" 라고 설명한다. AI는 그 법칙이 성립함을 보이는 증명을 PROOF.bend에 생성해야 한다.

Merging a bug is mathematically impossible: it is a theorem.
예시로 게임에서 "승리는 불가능하다"는 법칙을 걸어두니, 그 불변식을 깨는 코드를 AI가 머지하지 못하고 될 때까지 다시 시도했다는 사례를 든다.
병렬성은 자동이다. "No threads, no locks, no kernels to write. Split the work in two, and Bend spreads the calls over every core." 같은 바이너리가 싱글코어 C 속도에서 GPU 4,096코어 기준 최대 100배까지 확장된다고 적는다.
성숙도는 스스로 밝힌다. "Bend is still evolving. Expect bugs, and please report them." 백엔드·Linux·macOS에서 가장 잘 동작한다고 쓴다. 설치는 curl -fsSL https://bend-lang.com/install.sh | sh.
라이선스는 페이지에 없다.
토론에서 나온 것 — 제작자가 1년간 무급으로 개발했다고 밝혔고, 명세 부족 사례가 지적됐다. "벽을 제거하라"는 요구에 AI가 벽 대신 대각선 이동 규칙을 바꿔 법칙을 만족시켰다는 것. 표준 라이브러리가 작아 기본 정리부터 직접 증명해야 한다는 지적도 있었고, 한 개발자는 자기 요구사항을 증명하기 전에 정렬의 정확성부터 증명하느라 시간을 썼다고 보고했다.

판단

1. 검토를 빠르게 하는 대신 없애려는 시도다

이번 주에 본 도구들은 전부 검토를 싸게 만들려 했다. 스캐너는 우선순위를 매기고, CI는 빨라지고, 요약은 훑기 좋게 만든다. 그래도 마지막에 사람이 읽어야 한다는 사실은 안 바뀐다.

Bend의 제안은 다르다. 불변식은 내가 쓰고, 증명은 AI가 쓰고, 컴파일러가 확인한다. 그러면 원칙적으로는 코드를 안 읽어도 그 불변식만큼은 보장된다.

방향 자체는 이번 주 관찰과 맞물린다. 읽기가 병목이면 읽기를 빠르게 하는 건 상한이 있고, 읽지 않아도 되는 부분을 만드는 쪽이 상한이 높다.

2. 명세는 검토를 대체하지 못한다 — 벽 대신 대각선을 고친 사례

토론의 반례가 이 접근의 경계를 정확히 짚는다. "벽을 제거하라"는 법칙을 주니 AI가 벽을 건드리지 않고 대각선 이동 규칙을 바꿔서 조건을 만족시켰다.

증명은 내가 적은 것만 보장한다. 적지 않은 것은 자유다. 그러면 읽기의 부담이 사라진 게 아니라 코드에서 명세로 옮겨간 것이고, 명세를 빈틈없이 쓰는 일이 코드를 읽는 일보다 쉽다는 보장은 없다.

→ 여기서 채택 조건이 나온다. 이 방식이 값을 하려면 불변식이 짧고 전역적이어야 한다. "잔액은 음수가 될 수 없다", "이 함수는 파일을 쓰지 않는다", "사용자는 다른 사용자의 레코드를 읽을 수 없다" 같은 것. 이런 건 한 줄이고, 어기면 사고이고, 코드 어디서 깨지든 잡힌다.

반대로 기능 명세를 법칙으로 쓰려 들면 명세가 코드만큼 길어지고, 그때는 아무것도 절약되지 않는다. 명세를 검토해야 하니까.

3. 표준 라이브러리의 크기가 곧 도입 비용이다

자기 요구사항을 증명하기 전에 정렬의 정확성부터 증명해야 했다는 보고가 이 언어의 현재 위치를 말해준다. 증명 언어 계열의 전형적인 비용이고, 결함이라기보다 성숙도의 문제다.

→ 판단 기준 하나로 정리된다. 내가 증명하고 싶은 불변식이 표준 라이브러리 위에 얹히는가, 아니면 그 밑을 파야 하는가. 후자라면 지금은 아니다. 그리고 이 기준은 시간이 지나면서 저절로 바뀐다 — 라이브러리가 자라면 같은 불변식이 갑자기 실용권에 들어온다.

4. `LAWS.bend`라는 형식은 이 언어를 안 써도 가져갈 수 있다

저장소 루트에 사람이 쓴 불변식 파일을 두고, 기계가 그걸 확인하게 하는 구조. 증명이 아니어도 된다. 테스트, 런타임 어서션, 린트 규칙, CI 게이트로 근사할 수 있다.

이번 주에 반복해서 도달한 결론이 이것이다. 다이어그램 스킬의 검증 스크립트도, 훅 규칙을 컴파일 에러로 바꾼 프레임워크도, 승인 후 반영을 되묻는 광고 에이전트도 같은 자리에 있다. 문서에 적힌 규칙은 깨지고, 실행되는 검사만 남는다.

→ 오늘 할 수 있는 일: AGENTS.md나 CLAUDE.md에 적어둔 항목을 세어보고, 그중 기계가 확인할 수 있는 게 몇 개인지 표시한다. 확인 가능한데 문서에만 있는 항목은 옮긴다. 그게 이 언어가 가리키는 방향의 값싼 버전이고, 언어를 바꾸지 않고도 오늘 된다.

모르는 것

직접 써보지 않았다. 설치도 하지 않았다(curl | sh 형태라 더욱).
라이선스가 페이지에 없다. 이번 주에 같은 항목에 두 번 걸렸는데 여기서 또 비어 있다.
증명 생성의 성공률과 비용에 대한 수치가 없다. 실패하면 에이전트가 재시도한다는 서술은 있는데, 몇 번 만에 되는지, 한 번에 얼마가 드는지가 없다. 실무 도입에서 가장 중요한 숫자가 이것인데 비어 있다.
100배는 GPU 4,096코어 기준이다. 어떤 작업인지, 무엇과 비교한 것인지 확인하지 못했다.
"Python 문법"이라고 적혀 있지만 증명을 쓰는 언어는 Python이 아니다. 학습 곡선의 실체를 모른다.
제작자가 1년간 무급으로 개발했다는 토론 언급이 있었다. 도구의 품질과 별개로 지속 가능성은 채택 판단의 한 축인데, 판단할 근거가 없다.