타입 검사는 통과했고, 포매터는 아무 말도 하지 않았다

모델이 문법적으로 올바른 코드를 수백 줄씩 즉시 내놓게 된 이상, 생산성의 율속 단계는 얼마나 빨리 쓰는지가 아니라 얼마나 빨리 검토하고 검증하는지가 되었다. 이 진단은 옳다고 생각한다. 그리고 처방은 대개 언어 기능으로 쓰인다. 정적 타입이 환각을 걸러내고, 포매터가 스타일의 흔들림을 지우고, 빠른 컴파일이 자기 수정 루프를 돌리고, 두꺼운 표준 라이브러리가 수상한 의존성을 막는다. 마지막 방어선으로 “사람이 빨리 읽을 수 있는 코드”가 놓인다.

나는 지난 한 주 동안 Mere라는 자작 언어의 컴파일러를 v0.1.263에서 v0.1.273까지 진행했다. 다섯 개의 백엔드(인터프리터, C, LLVM, Wasm, RV32I)를 가진 처리계로, 문자열 표현을 이행하고, 실패의 의미를 맞추고, 꼬리 호출을 고치고 있었다. 진단이 옳다면 그 한 주의 기록은 처방의 효과에 대해서도 무언가 말할 수 있어야 했다. 세어 보니, 실제로 오류를 잡아낸 것 중 언어 안에 있는 것은 하나도 없었다.

아래는 Mere에 대한 홍보가 아니다. 다섯 개의 구현을 가진 처리계는 이런 종류의 기록을 남기기 쉽다는, 딱 그 이유만으로 증거로 쓴다.

일주일 분량의 표

무슨 일이 있었나	정적 타입	포매터	사람이 읽기	실제로 잡아낸 것
셀프 호스트한 백엔드가 옛 문자열 표현 그대로 같은 ABI 번호를 내걸었다	통과	침묵	사흘간 지나갔다	네 구현에 같은 값을 출력시키는 차분 테스트
nan < 0.0이 인터프리터에서만 true였다	통과	침묵	보이지 않는다	쓸 수 있게 된 값으로 새로 쓴 게이트
“키가 없다”를 컴파일 계열 세 곳에서 catch할 수 없었다	통과	침묵	보이지 않는다	컬렉션 값 영역 게이트
str_repeat s 0이 LLVM에서만 길이 필드 없이 할당했다	통과	침묵	보이지 않는다	문자열 값 영역 게이트
list_filter만 꼬리 재귀가 아니었다	통과	침묵	보이지 않는다	10만 요소를 흘린 게이트, 그다음 grep
스택 오버플로에 이름이 없어 두 구현이 말없이 죽었다	대상 밖	대상 밖	사인이 안 나온다	실패할 프로그램들을 모아둔 게이트
게이트가 사흘 전 바이너리를 검사하고 있었다	—	—	“코드가 나쁘다”로 잘못 읽었다	CI와 내 기계의 환경 차이를 의심한 것
이미 사실이 아닌 pin이 디스크에 남아 있었다	대상 밖	대상 밖	아무도 눈치채지 못한다	pin의 실효 자체를 실패로 만든 것

세 번째 열이 하나도 잡아내지 못했다. 처방의 마지막 방어선이 바로 그 열이므로, 이건 작은 이야기가 아니다.

가드레일은 하나의 프로그램을 지키고, 게이트는 질문을 지킨다

이렇게 되는 이유는 지키는 대상이 다르기 때문이다. 타입 검사기도 포매터도 지금 눈앞에 있는 하나의 프로그램의 내부 정합성을 본다. 표현이 일관되는가, 이름이 해결되는가, 서식이 맞는가. 모두 “이 프로그램은 그 자신과 모순되지 않는가”라는 질문이다.

위 표의 모든 행은 그 질문에 대해서는 건강했다. 번호를 내거는 코드는 타입이 맞는다. nan 비교도 타입이 맞는다. 사흘 전 바이너리를 검사하는 셸 스크립트는 그 자체로는 올바르게 작동하고 있었다. 모순은 하나의 프로그램 안이 아니라 두 가지 사이에 있었다 — 두 구현 사이, 선언과 구현 사이, 검사하는 것과 검사되는 것 사이.

하나의 프로그램 안을 보는 도구는 원리적으로 거기에 닿지 못한다.

세 건만 안을 들여다보자.

ABI 번호는 선언이지 검사가 아니다. 이 시스템은 Wasm 모듈과 JS 호스트 사이의 표현을 ABI 번호로 약속한다. 문자열은 “길이 4바이트, 본체, NUL”이고 값은 본체의 첫머리를 가리킨다. 그런데 모듈을 만드는 컴파일러가 둘이다. OCaml 구현과, 언어 자신이 컴파일한 셀프 호스트 판. 셀프 호스트 판만 길이 필드가 없는 옛 표현 그대로였고, 그러면서 같은 번호를 내걸고 있었다. 길이 필드를 믿은 호스트는 문자열 하나에 대해 567KB의 NUL을 출력했다. 번호가 일치한다는 것은 구현이 일치한다는 뜻이 아니다. 같은 번호를 내거는 구현이 둘 이상 있다면, 번호가 아니라 동작을 맞춰보는 검사가 필요하다. 잡아낸 것은 네 구현에 같은 문자열을 출력시키는 테스트였다.

게이트는 검사 대상 자체를 캐시해서는 안 된다. 셀프 호스트 검사 스크립트가 7건 전부 실패했다. 컴파일러는 고장 나지 않았다. 스크립트는 셀프 호스트 컴파일러를 /tmp에 만드는데, “파일이 없으면 만든다”로 쓰여 있었다. 거기 있던 것은 사흘 전, ABI를 바꾸기 전의 바이너리였고, 게이트는 아무도 묻지 않은 컴파일러를 검사하고 있었다. 입력과 오라클과 vendoring한 데이터를 캐시하는 것은 옳다. 피검체를 캐시하면 게이트는 다른 것을 검사한다.

이 거짓에는 곤란한 형태가 있다. 고장 났다는 얼굴로 나타난다. 말없는 초록이 아니라 빨강이므로, “게이트가 빨갛다, 그러면 코드가 나쁘다”라는 당연한 추론이 그대로 작동해 버린다. 게다가 CI는 한 번도 반대하지 않았다. CI 러너는 /tmp가 비어 있으니 매번 새로 만들어서 늘 초록이었다. 같은 커밋이 아무도 보지 않는 기계에서는 초록, 작업하는 기계에서는 빨강이었고, 빨강 쪽이 틀렸다. 매번 만들어도 260 밀리초다. 캐시할 이유는 처음부터 없었다.

게이트에 “이제 위반하지 않는다”도 검출시켜라. 이 시스템에는 고칠 수 없는 차이를 테스트에서 빼지 않고 고정해 두는 장치가 있다. 어떤 구현만 답이 다를 때, 그 차이를 선언으로 적어 둔다. 그런데 그 차이가 일치하기 시작했을 때 테스트는 조용히 통과시켰다 — 일치한 케이스는 선언을 읽지 않기 때문이다. 즉 “이제 사실이 아닌 선언”이 디스크에 계속 남는 형태가 되어 있었고, 이것은 이 장치가 막아야 할 바로 그것이었다. 실효한 선언을 실패로 만들자, 그 주의 작업이 끝났음을 알려준 것은 그 새로운 실패였다. 위반의 검출만으로는 고쳤다는 사실이 기록에서 사라지지 않는다.

“사람이 읽기” 열에 대하여

가독성이 무가치하다는 이야기가 아니다. 위의 수정들은 어느 것도 읽을 수 있는 언어로 쓰여 있지 않았다면 불가능했다. 하지만 “AI가 쓰고 사람이 검증한다”는 공정의 그림은 이 한 주의 실제와 맞지 않았다. 실제로 일어난 것은 기계가 검증하고, 사람의 일은 물을 질문을 설계하는 것이었다.

그렇게 보면 그 주에 얻은 규칙이 전부 “질문의 설계” 이야기였던 것에 설명이 붙는다. 게이트는 검사 대상을 캐시하지 않는다. 게이트는 몇 건을 검사했는지 말한다(0건은 “돌지 않았다”와 구별되지 않는다). 오라클에는 버전이 있으니 고정하고, 무엇과 비교했는지 출력한다. 묻지 않음으로써 일치시키지 않는다. 숫자는 둘을 가진다(한쪽이 움직이지 않을 때 다른 쪽이 움직일 수 있다). 의존성 부재로 인한 skip과 진짜 실패로 인한 skip을 나눈다. 어느 하나도 가독성 이야기가 아니다.

증명은 어떤가

여기까지 “가드레일”이라고 불러온 것은 타입 검사기와 포매터였다. 그런데 그것은 이 논의의 가장 강한 형태가 아니다. MoonBit은 0.9에서 형식 검증을 언어의 일급 요소로 만들었다 — 계약(contract), 술어, 루프 불변식, proof_assert가 문법이고, 컴파일러가 그것을 직접 이해한다. 목표는 명시적으로 AI를 향해 있다. 생성된 코드가 단지 동작하는 것을 넘어 옳다고 증명할 수 있게 하는 것이다. 이것은 타입 검사보다 훨씬 멀리 닿고, 위의 이분법은 그것을 놓치고 있다.

그 누락을 메운 뒤에도 결론은 달라지지 않는다고 생각한다. 증명과 게이트는 다른 방식으로 깨지기 때문이다.

증명이 답하는 것은 “구현이 명세를 만족하는가”이고, 그 명세는 사람이 쓴 것이다. 위 표의 행을 다시 보면 어느 것이나 위반된 주장을 아무도 적어두지 않았던 경우였다.

• ABI 번호는 명세 그 자체였다. 문자열은 “길이 4바이트, 본체, NUL”이라고 적혀 있다. 깨진 것은 구현과 명세의 관계가 아니라, 같은 명세를 내건 구현이 둘 있었고 그중 하나가 다른 것이었다는 점이다. 어느 구현도 자기 자신에 대해서는 거짓말을 하지 않는다.
• 사흘 전 바이너리를 검사하던 게이트는 검사 대상에 대한 올바른 명세를 가지고 있어도 구제되지 않는다. 틀린 컴파일러 쪽이 명세를 만족했기 때문이다. 물어야 했던 것은 “제대로 검사했는가”가 아니라 “무엇을 검사했는가”였다.
• 실효한 pin은 이미 사실이 아닌 명세 그 자체였다. 구현을 명세에 비추는 장치는 명세 쪽이 낡았다는 것을 알려주지 않는다.

게이트에도 고유한 파손 방식이 있고, 그것은 다음 절에 쓴다.

어느 한쪽이 다른 쪽을 포함하는 이야기가 아니다. 증명은 명세의 품질로 상한이 정해지고, 게이트는 비교하는 것들의 독립성으로 상한이 정해진다. 그리고 증명만이 닿는 범위가 실제로 있다. 경계 조건이나 불변식처럼 계약으로 쓸 수 있는 종류의 버그에 대해서는, 형식 검증이 내가 가진 것보다 엄밀하게 강하다. 게이트가 우연히 물어본 입력이 아니라 모든 입력에 대해 답하기 때문이다. 표의 str_repeat s 0이 그쪽에 있다. “결과는 항상 타당한 길이 필드를 가진다”고 적혀 있었다면, 아무도 0을 시도해 볼 생각을 하지 않았어도 잡혔을 것이다.

이로써 주장은 유익하게 좁아진다. “답은 언어 밖에 있다”가 아니라, 이 한 주 동안 들은 것은 전부 언어 밖에 있었고, 그중 일부에 닿을 수 있었던 언어 쪽 장치는 타입이 아니라 증명이었다, 이다.

두 가지 한계

이 주장에는 한계가 있고, 한쪽은 같은 주에 내가 직접 물린 것이다.

일치가 증거가 되는 것은 일치하는 것들이 독립일 때뿐이다. 얼마 전에 메모리에서 32비트를 빅 엔디언으로 읽는 함수가 부호 확장하는 버그를 고쳤다. 불투명한 픽셀은 alpha가 0xFF이므로 픽셀을 다루는 프로그램은 전부 이걸 밟는다. 그런데 이 버그는 다섯 구현의 차분 테스트로는 잡히지 않았다. JS 호스트도 동일한 버그를 가지고 있었기 때문이다(getInt32를 쓰고 있었다). 여러 구현을 맞춰보는 검사는 타입 검사보다 사거리가 넓지만 무적은 아니다. 독립성이 성립하는 범위에서만 듣는다. 이걸 말하지 않고 “차분 테스트가 지켜준다”고 쓰는 것은 “타입 검사가 지켜준다”와 같은 종류의 과장이다.

그리고 이것은 한 사람, 한 프로젝트, 한 주 분량의 기록일 뿐이다. 표의 여덟 행은 구체적이고 날짜가 있지만, 여덟 행은 여덟 행이다. 여기서 “언어 기능은 검증에 듣지 않는다”를 끌어낼 수는 없다. 끌어낼 수 있는 것은 훨씬 좁은 것으로, 적어도 이 한 주 동안 들은 것은 전부 언어 밖에 있었다는 하나의 반례에 머문다.

언어 설계에 함의가 있다면

“가드레일을 늘려라”는 아니라고 생각한다. 게이트를 놓을 수 있는 형태여라, 다. 구체적으로는 세 가지다.

첫째, 같은 질문을 독립적으로 답할 수 있는 곳을 여럿 가질 것. 이 시스템이 그 주에 찾아낸 결함의 대부분은 다섯 구현에 같은 질문을 물었기 때문에 나왔다. 단일 구현 언어는 이 검사를 원리적으로 가질 수 없다. 외부의 규범 코퍼스나 다른 구현과의 차분으로 대체할 수는 있지만, 그것은 언어 밖에 마련해야 하는 것이 된다.

둘째, “무엇이 존재하는가”를 컴파일러에 물을 수 있을 것. 이 시스템은 예전에 어느 백엔드에 어느 빌트인이 있는지를 손으로 쓴 표로 갖고 있었고, 세 개 있던 표가 셋 다 낡아 있었다. 믿을 수 없는 표는 표가 없는 것보다 나쁘다. 이제는 컴파일러에 질의해서 표를 생성하고 매번 차분을 낸다. 모델이 낡은 문서를 읽고 거짓을 쓰는 문제에 대해, 문서를 자동 갱신하는 것과는 다른 답이 있다. 문서를 빌드의 산출물로 만드는 것이다.

셋째, 실패의 표면이 균일할 것. 같은 실패가 백엔드마다 다른 이름을 가지면, 검사는 그 차이를 진짜 차이로 보고한다. 그 주에 “가장 자주 일어나는 실패가 가장 이름이 없다”는 형태를 찾았다. 이 시스템의 프로그램이 실제로 죽는 가장 흔한 형태는 스택 오버플로인데, 그것은 언어가 아무 말도 하지 않는 유일한 실패였고, 두 구현은 말없이 종료 코드 139를 돌려줄 뿐이었다. 드문 실패(0으로 나누기, 키 누락)부터 차례로 이름을 붙여 가면, 가장 빈번한 실패만이 “언어 외부의 사건”으로 남는다.

셋 다 생성된 코드를 읽기 쉽게 하는 이야기가 아니다. 기계가 질문을 계속 붙들 수 있게 하는 이야기다. 검증이 병목이라는 진단이 옳다면, 투자할 곳은 그쪽이다.