Bend 2, AI 코드 규칙을 증명으로 검사…2.0.39서 업로드 경로 제한

프로그래밍 언어 Bend 개발팀은 공식 GitHub 릴리스 노트를 통해 2.0.39 버전의 변경 사항을 공개했다. 한국시간 24일 나온 이번 버전은 패키지 발행 과정에서 외부 파일이 포함되지 않도록 경로 검사를 강화했다.

공식 설명에 따르면 bend --publish는 진입 파일이 있는 디렉터리 안의 파일만 전송한다. 상위 디렉터리로 이동하는 ../ 경로, 디렉터리 밖을 가리키는 심볼릭 링크, 외부 파일로 연결된 LICENSE는 허브에 요청을 보내기 전에 거부한다. 컴파일 결과물이 하드 링크 등을 통해 입력 파일을 덮어쓰지 않도록 하는 수정도 포함됐다.

Bend 2가 내세우는 특징은 코드와 수학적 증명을 함께 다루는 개발 방식이다. 공식 가이드는 사람이 프로그램의 규칙을 LAWS.bend에 적고, AI가 그 규칙에 맞는 코드와 PROOF.bend의 증명을 작성하는 구성을 제시한다. 예를 들어 정렬 함수가 어떤 숫자 목록을 받아도 같은 원소를 오름차순으로 돌려준다는 성질을 규칙으로 삼을 수 있다.

검사 명령인 bend PROOF.bend는 규칙이 미해결 상태이거나 증명이 성립하지 않으면 실패를 표시한다. PROOF.bend가 같은 위치의 LAWS.bend를 가져오지 않는 경우에도 거부한다. 자연어로 오류를 내지 말라고 지시하는 대신, 지켜야 할 성질을 명시해 검사 대상으로 삼는 접근이다.

추가 옵션인 --verdict는 Lean으로 증명이 작성된 소규모 검증 커널을 사용해 한 차례 더 검사한다. 공식 가이드는 이때 외부 코드나 @unsafe에 의존하지 않는 증명이어야 한다고 설명한다. AI가 구현을 바꾸더라도 사람이 정한 규칙 자체는 바꾸지 않는 작업 구분도 제시했다.

다만 이를 모든 버그가 사라지는 언어로 받아들여서는 안 된다. 개발팀은 README에서 일반 검증기 자체에는 증명이 없고 버그가 있을 수 있다고 명시했다. --verdict도 변환된 항을 검사할 뿐, 소스 파서와 커널 입력으로 바꾸는 변환 과정까지 증명된 것은 아니다. Bend의 의미 체계에서 증명된 성질과 실제 실행 백엔드 사이에 차이가 생길 수 있다는 한계도 밝혔다.

적용 범위 역시 아직 제한적이다. 공식 문서는 Bend 1 프로그램과 HVM이 Bend 2로 그대로 이어지지 않으며, 기본 제공 TLS·HTTP 라이브러리와 JSON·정규식 지원도 없다고 안내한다. C·Metal·CUDA·JavaScript를 대상으로 하지만 초기 단계의 컴파일러이므로 버그를 예상해야 한다는 설명이다.

Bend 2의 의미는 AI가 만든 코드를 무조건 신뢰하게 해준다는 데 있지 않다. 사람이 명세한 규칙과 그 규칙을 충족한다는 증명을 개발 절차에 넣는 데 있다. 검증 대상으로 삼은 규칙의 범위와 검증 도구 자체의 신뢰 범위를 함께 살펴야 한다.

출처: Bend 개발팀 공식 GitHub 릴리스 노트(2.0.39) https://github.com/bendlang/bend/releases/tag/v2.0.39
Bend 2 공식 가이드 https://github.com/bendlang/bend/blob/v2.0.39/guide/GUIDE.md
Bend 공식 README(제약 사항) https://github.com/bendlang/bend/blob/v2.0.39/README.md