저자임. HN 운영진께, 다른 분이 먼저 게시했는데 제목을 “Bend - 증명으로 AI의 실수를 막고 GPU에서 실행되는 언어”로 바꿔줄 수 있을까요?
질문은 무엇이든 환영하지만, 이번에는 조금만 예의와 존중을 갖춰주길 부탁함. 1년간 거의 매일 16시간씩, 주 7일 작업했고 무료로 공개하는 것이며, 누구에게도 사용을 강요하지 않음. 간혹 실패하는 부분이 있더라도 불구덩이에 던지듯 몰아붙이기보다 정중하게 짚어주면 감사하겠음.

흔한 결과인지는 모르겠지만, “벽 제거하기” 예제를 실행했더니 무서운 결과가 나옴. 이동을 전부 대각선으로 바꾸고, 위·아래 키는 양의 대각선 방향으로, 왼쪽·오른쪽 키는 음의 대각선 방향으로 움직이도록 임의로 결정해버림. “이길 수 없다”라는 규칙 하나만으로는 명세가 너무 불충분함. 그런데 해결책이 지나치게 영악해서 이 접근법의 약점이 드러남. 어느 순간에는 규칙을 작성하는 일이 코드 작성보다 더 어려워지므로, 모든 프로그램의 명세에는 빈틈이 남을 수밖에 없음. 불충분하면서도 엄격한 규칙은 AI가 규칙의 취지가 아닌 문구만 만족하는 “창의적” 해법을 찾도록 유도함. 이번에는 명백했지만, 잘 드러나지 않는 경우에는 어떤 편법이 생길지 정말 걱정됨.

가이드의 “같은 파일이 CPU 프로그램이자 GPU 커널이며, clang이 호스트용으로, Metal이나 CUDA가 장치용으로 빌드하므로 !는 어느 칩에서나 정확히 같은 코드를 실행한다”라는 문장은 정확히 무슨 뜻인가요? !의 의미가 명시적으로 정의되어 있지 않음. clang이 호스트와 Metal용으로 빌드하고 CUDA가 장치용으로 빌드한다는 건지, clang이 호스트·Metal·CUDA용으로 빌드한다는 건지, 아니면 전혀 다른 뜻인지 불분명함.

처음부터 증명을 염두에 둔 언어라는 발상이 마음에 들고, 코딩 에이전트 시대에는 특히 설득력 있어 보임. 남들이 아직 예상하지 못한 좋은 아이디어인 만큼, 자주 오해받거나 심한 말까지 들을 각오는 해야 할 듯함!

보드와 깃발 애니메이션이 Bend의 컴파일 타임 검사와 어떻게 연결되는지 설명해줄 수 있나요? 실제로 Bend가 검사를 실행하는 과정을 직접 보여주는 건가요?

사전 지식 없이 논리적 토대를 완전히 이해할 수 있는 자료, 가능하면 책 한 권을 추천해줄 수 있나요?
왜 이렇게 설계했는지, 아핀성(affinity)이 어떤 문제를 해결하는지, 클로저를 왜 최대 한 번만 호출할 수 있는지, 반환하지 않는 함수가 어떻게 무엇이든 증명할 수 있는지 등을 이해하고 싶음.

증명이 실제로 어떻게 작동하는지 설명이 부족함. 이런 발상은 다들 해봤을 것 같은데, 가능한 모든 이동 순서를 어떻게 증명하나요? 가능한 상황이 너무 많아 증명하거나 테스트할 수 없다면 어떻게 하나요?
2차원 게임은 쉽겠지만, 차원을 늘리고 소수 번호의 차원이나 특정 좌표 조건에서만 점프를 허용하는 식으로 특수 규칙을 끝없이 추가할 수도 있음. 그럴 때 Bend는 어떻게 보장하나요?
GitHub와 논문도 살펴봤지만 깊이 파고들 만큼 의욕이 생기지는 않았고, 증명 방식 자체에 대한 설명이 빠진 느낌임. Lean이 어떻게 작동하는지는 이해하지만, 여기서는 모르겠음.

게임이 크면 증명도 거대해져야 함. 기본적으로 Lean과 같은 방식으로 작동함.

LAWS.bend의 규칙이라는 발상은 좋지만, 실제로는 에이전트가 개발 중인 새 기능에 맞춰 규칙 자체를 바꿔버려 취지가 무색해지곤 함.
따라서 일부 규칙은 고정해야 하지만, 전부 고정하면 아무것도 추가하거나 수정할 수 없음. 결국 판단은 여전히 인간 몫이고, 다시 인간이 병목이 됨.
에이전트가 비합리적인 행동을 할 때마다 증명에 가까운 검사를 CI에 추가하는 방식은 어느 정도 효과가 있었고, 모든 코드베이스에 포함해야 한다고 봄. 코드와 증명을 함께 두는 https://code-contracts.cc/도 있음.

적어도 AI가 LAWS.bend에 무엇을 넣는지는 읽어봐야 함. 다만 코드베이스보다 훨씬 작으므로, 궁극적으로 읽어야 할 코드가 엄청나게 줄어드는 것이지 0이 되는 것은 아님.

바이브 코딩으로 만든 작은 회의 일정 조정용 cron 작업을 이식해봤음. 본질적으로 달력의 불변 조건을 만족시키는 작업이라 잘 맞을 것 같았고, 대체로 성공했지만 Claude (Opus 5) 가 몇 가지 아쉬움을 제시함.
“Base가 제공하는 산술 법칙은 U32.add_comm 하나뿐이고 순서 이론은 없음. PROOF.bend 163줄 중 약 60줄이 cmp_refl, and_false, and_comm, le_max_l, le_max_r, add_succ처럼 당연히 있을 법한 사실을 증명하는 코드임. 프로젝트마다 한 번만 작성하면 되지만, 그 비용은 잡아둬야 함.”
“Base의 Nat.max는 증명에 사용할 수 없음. 구현이 Bool.pick(Nat, Nat.is_lt(a,b), b, a)인데, 증명에서는 계산된 값을 기준으로 경우를 나눌 수 없음. 그래서 Nat.cmp와 보조를 맞춰 전개되는 구조적 재귀 함수 nat_max를 작성함.”
“가장 원했던 법칙은 출력된 어떤 두 일정도 겹치지 않는다는 것이었지만, 명시하지 못함. collapse 입력이 정렬되어 있다는 가정이 필요한데 Base의 List.sort에는 정렬됨을 보장하는 법칙이 없어서, 먼저 병합 정렬의 정확성을 증명해야 함. 이것이 원리상 증명 가능함과 오늘 오후 안에 증명 가능함의 간극을 보여줌.”
컴퓨터 과학은 사실상 부전공 수준으로만 공부해서 증명에는 문외한임. 유용한 피드백인지, 단순히 Claude가 뭔가를 오해한 건지는 모르겠음.

커밋 이력에 감정적으로 애착을 가져 공개할 때 취약함까지 느낄 수 있다는 게 안타까움. 동시에 작업이 어떻게 만들어졌는지 쉽게 파악할 수단이 없으면, 다른 이들이 결과물 자체에 집중하지 못하고 그 출신 배경을 평가하게 된다는 것도 안타까움.
배경이 궁금하다면 Reddit에서 SrPeixinho를 검색하면 작업의 맥락을 이해할 만한 이력을 많이 찾을 수 있음. Discord 서버에 들어가 직접 대화할 수도 있음.

Go 같은 다른 언어로 테스트를 작성하고 실행하는 것보다 어떤 점이 더 나은가요?

결국 모든 규칙도 바이브 코딩으로 작성해야 할 텐데, 규칙 자체가 틀릴 수 있음.

농담을 빼고 보면, 규칙은 간단하게 작성하고 그 규칙이 성립한다는 증명은 에이전트가 맡는 것이 핵심인 듯함. 다만 더 복잡한 규칙을 표현하려 할수록 이 전제가 덜 성립할 것 같음.

AI를 언급하지 않고도, 증명에 새로운 접근을 도입한 빠른 신생 언어라고 소개했다면 그것만으로 관심을 가졌을 것임. 이제는 AI라는 단어가 없으면 아무도 관심을 갖지 않는 듯함. 예전에는 이런 것 자체에 관심을 갖는 이들이 많았음.

증명 자체를 자연어로 정의하지 않는 한 인간이 받아들일 것 같지 않음. 증명은 쓰기는커녕 읽는 데도 인지 부담이 큼.

하지만 자연어에는 모호함이 있음. AI의 출력에는 가정도 포함되어야 하며, “프롬프트”라는 말도 진지하게 “대화”로 바꿔야 함.

Victor Taelin의 HVM 덕분에 컴파일 대상으로서 상호작용 조합자(interaction combinators)에 관심을 갖게 됐고, 지금은 대학 연구의 일부로 구현 작업을 진행 중임. Bend 2.0 출시가 반가움!

그렇다면 Marc Thatcher의 최근 상호작용망 박사학위 논문도 흥미로울 듯함. 곱셈적 선형 논리의 증명망을 통해 상호작용망을 훌륭하게 풀어내며, 상호작용망의 생산성 분석 같은 새로운 기여도 여러 가지 담고 있음. https://hdl.handle.net/10779/uos.32024301에서 볼 수 있음.