정형 검증된 코드가 현실 세계에서 여전히 버그를 낳는 세 가지 경로—무효인 증명, 잘못된 속성, 틀린 가정—를 Leftpad 사례와 함께 설명하고, “정확성”이 실제로 무엇을 보장하는지 논의한다.
v0.12가 공개되었습니다! 이번이 마지막 대규모 콘텐츠 릴리스가 될 예정입니다. 앞으로 몇 달은 기술 리뷰, 카피에디팅, 다듬기를 거쳐 3월에 1.0을 내는 것을 목표로 하고 있습니다. 전체 릴리스 노트는 여기.
저는 Let's Prove Leftpad라는 작은 프로젝트를 운영합니다. 사람들이 그 짤의 주인공인 leftpad의 정형 증명을 제출하는 곳이죠. 최근에 “증명상 올바르다”는 Leftpad를 깨기라는 글을 읽었는데, 대부분(아니면 전부) “증명상 올바른” leftpad에 버그가 있다고 주장합니다! 예를 들어 Lean 증명에서는 leftpad('-', 9, אֳֽ֑)의 결과가 원래대로라면 ---------אֳֽ֑가 되어야 하지만 실제로는 ------אֳֽ֑가 됩니다.
왜 이렇게 되는지(유니코드 때문이죠)는 해당 글을 읽어보면 잘 설명되어 있습니다. 근본적인 문제는 "정확하다"가 두 가지 서로 다른 의미를 가질 수 있고, 이것이 형식 기법이 실제로 무엇을 보장하는지에 대한 혼란으로 이어진다는 점입니다. 그래서 저는 이것을 증명과 정확성의 본질, 그리고 “정확한” 코드가 어떻게 여전히 버그를 가질 수 있는지 이야기할 좋은 기회로 봅니다.
현실 세계 대부분에서 "정확하다"는 "버그가 없다"는 뜻입니다. 그런데 “버그”라는 범주는 그리 명확하지 않습니다. 누군가가 “이거 제대로 안 되는데, 버그야”라고 말하게 만드는 건 뭐든 버그죠. 너무 느린 것도 버그고, 오타도 버그고… “정확하다”는 개념은 좀 흐릿합니다.
정형 기법에서 "정확하다"는 아주 구체적이고 정밀한 의미를 갖습니다. 코드가 명세(specification, 이하 “스펙”)에 부합한다는 뜻이죠. 스펙은 코드의 속성을 더 높은 수준에서 서술한 것으로, 대개 그 자체를 직접 구현할 수 있는 형태는 아닙니다. 가장 대중적인 종류의 “증명된 스펙”을 하나 봅시다:
-- Haskell
inc :: Int -> Int
inc x = x + 1
이 타입 시그니처 Int -> Int 자체가 스펙입니다! 이는 논리 명제 모든 x ∈ Int에 대해: inc(x) ∈ Int에 대응합니다. Haskell 타입 체커는 이를 자동으로 검증해 줄 수 있습니다. 하지만 모든 x ∈ Int에 대해: inc(x) > x 같은 속성은(쉽게) 자동으로 검증할 수 없습니다. 정형 검증은 자동 검증 범위를 넘어서는 임의의 속성을 검증하는 데 관심을 둡니다. 대부분의 경우 증명의 형태를 취하죠. 사람이 코드를 스펙에 맞는다고 수작업으로 증명하고, 증명기는 그 증명이 올바른지 확인합니다.
그렇다고 "정확성"이 증명되었다 해도, 여전히 코드에 버그가 있을 수 있는 방법들이 몇 가지 있습니다.
어떤 이유에서든 그 증명이 실제로 코드를 스펙과 일치한다고 보여주지 못하는 경우입니다. 누군가가 “음, 좋아 보이네”라고 확인하는 식의 종이와 연필(수기) 검증에서는 꽤 흔합니다. 정형 검증에서는 훨씬 드물지만 특정 상황에서는 여전히 발생할 수 있습니다.
증명기 자체(코드 또는 컴파일된 바이너리)에 버그가 있어 잘못된 증명을 받아들이는 경우입니다. 사람들은 이걸 많이 걱정하지만, 검증된 코드가 잘못되는 다른 모든 이유에 비하면 훨씬 드뭅니다. 그래서 여기서는 완전성을 위해서만 포함합니다.
편의를 위해 대부분의 증명기와 정형 언어에는 “이 명제가 참이라고 그냥 받아들여” 같은 기능이 있습니다. 큰 그림의 증명을 진행하면서 세부는 나중에 채우는 데 도움이 되죠. 만약 이런 지름길을 남겨둔 채로, 컴파일러가 “증명 가정이 남아 있는 코드”의 컴파일을 허용하도록 설정되어 있다면, “증명 검사를 통과한” 잘못된 코드를 컴파일할 수 있습니다. 하지만 이런 건 정말 그러면 안 되죠.
다음 코드는 증명상 올바릅니다:
inc :: Int -> Int
inc x = x-1
제가 제시한 유일한 스펙은 타입 시그니처 Int -> Int뿐입니다. 어디에도 inc(x) > x라는 속성을 스펙에 넣지 않았으니, 그 속성이 성립하지 않더라도 코드는 여전히 “정확한” 것입니다.
Leftpad 증명에서 “잘못된 것”이 바로 이것입니다. 그들은 "leftpad(c, n, s)가 화면에서 n칸을 차지하거나(또는 s가 더 길면 s가 차지하는 만큼)"이라는 속성을 증명하지 않았습니다. 대신 더 약한 속성인 "len(string)을 어떻게 정의하든 len(leftpad(c, n, s)) == max(n, len(s))"를 증명했습니다. 후자는 전자를 대략적으로 대체하는 지표이고 대부분의 경우에는 잘 동작하지만, 누군가 정말로 전자의 속성이 필요하다면 버그를 겪을 소지가 있습니다.
왜 더 강한 속성을 증명하지 않을까요? 어떤 때에는 코드를 한 가지 방식으로 쓰길 의도했는데 사람들이 다른 방식으로 쓰기 때문입니다. 그러면 "증명된 코드를 오용한다"는 비난으로 이어질 수 있는데, 사실은 검증 전문가가 무엇이 실제로 “증명되었는지”를 개발자에게 충분히 교육하지 못한 경우가 더 많습니다.
어떤 때에는 그 속성을 증명하기가 너무 어렵기 때문입니다. “출력이 시각적으로 정렬되어 있다”는 것은 유니코드 입력 전반에 대한 증명인데, 유니코드의 핵심 스펙만 해도 1,243쪽에 달합니다.
또 어떤 때에는 우리가 원하는 속성을 표현하기가 너무 어렵기 때문입니다. “사람들이 출력을 시각적으로 정렬되었다고 인지한다”를 수학적으로 어떻게 표현할까요? OS와 폰트에 따라 달라질까요? 다음 두 줄은 정확히 다섯 글자이지만 시각적으로 정렬되어 있지 않습니다:
|||||
MMMMM
아니면 여러분에게는 정렬되어 보일 수도 있겠죠! 많은 사람들이 이메일을 모노스페이스 글꼴로 읽으니까요. “우리가 그 속성을 표현할 수 없다”는 문제는 수학/계산 개념이 아닌 인간/비즈니스 개념을 다룰 때 자주 등장합니다.
마지막으로, 그냥 뇌정지 같은 경우도 있습니다. 거의 모든 이진 탐색과 병합 정렬이 깨져 있다의 모든 증명은 이런 류입니다. 그들은 경계가 없는 정수로 이진 탐색의 정확성을(비형식적으로) 증명했고, 많은 프로그래밍 언어가 머신 정수를 사용한다는 사실, 즉 충분히 큰 합은 오버플로될 수 있다는 사실을 잊었습니다.
이는 아마 가장 중요하면서도 가장 미묘한 버그의 원인입니다. 우리가 증명하는 대부분의 속성은 “X는 항상 참이다”가 아닙니다. “Y가 참이라고 가정하면, X도 참이다”가 보통이죠. 그러면 Y가 참이 아닐 때 X에 대한 보장은 사라집니다. 좋은 예가 이진 탐색입니다. 이는 입력 리스트가 정렬되어 있다고 가정해야만 원소를 올바르게 찾습니다. 리스트가 정렬되어 있지 않다면 올바르게 동작하지 않습니다.
정형 검증은 여기에 두 가지 주름을 더합니다. 첫째: 어떤 때에는 속성을 타당하게 만들기 위해 가정이 필요하지만, 증명을 쉽게 만들기 위해 가정을 추가하기도 합니다. 그래서 검증에 사용한 가정이 더는 성립하지 않아도, 코드 자체는 버그가 없을 수 있습니다! 모든 유니코드 글리프에 대해 시각적 정렬을 구현한 leftpad라 하더라도, ASCII 문자열과 패딩에 대해서만 시각적 정렬을 증명 하는 편이 훨씬 쉽습니다.
둘째: 우리는 통제 밖에 있는 환경적 가정을 많이 해야 합니다. 알고리즘이 출력을 반환하나요, 아니면 스택을 쓰나요? 데이터를 저장할 충분한 메모리가 있다고 가정해야 합니다. 변수를 쓰나요? 동시성이 그 변수를 수정하지 않는다고 가정해야 합니다. 외부 서비스를 쓰나요? 벤더가 API나 응답 포맷을 바꾸지 않는다고 가정해야 합니다. 컴파일러가 제대로 동작했고, 하드웨어에 결함이 없고, OS가 무언가를 건드리지 않는다고도 가정해야 하죠. 이들 중 어느 것이든 코드가 증명되고 배포된 뒤 한참 뒤에 바뀔 수 있기 때문에, 정형 검증은 한 번 하고 끝낼 수 있는 일이 아닙니다.
사실 대부분의 가정은 하지 않아도 됩니다. 하지만 가정을 하나 덜어낼 때마다 증명은 더 어려워지고, 증명할 수 있는 속성의 범위는 더 제한됩니다. 게다가 환경적 가정이 바뀌더라도 코드가 여전히 버그 없이 동작할 수도 있으니, 증명에 들일 시간과 다른 유용한 일에 쓸 시간 사이의 트레이드오프가 존재합니다.
“가정”의 또 다른 흔한 근원은, 검증된 코드가 미검증 코드에 의존하는 경우입니다. 러스트 컴파일러는 safe 코드에 메모리 버그가 없음을 unsafe 코드에도 버그가 없다는 가정하에 증명해 줄 수 있지만, 그 가정의 확인은 인간에게 달려 있습니다. Liquid Haskell은 검증 가능하지만 일반 Haskell 라이브러리도 호출할 수 있는데, 그 라이브러리는 검증되어 있지 않습니다. 우리는 그 코드가(“스펙에 부합한다”는 의미에서) 올바르다고 가정해야 하며, 그렇지 않다면 우리의 증명은 “정확”해도 실제로는 버그를 일으킬 수 있습니다.
이 경계들은 모호합니다. 저는 “이진 탐색” 버그가 잘못된 속성을 증명했기 때문에 발생했다고 썼지만, 여러분은 정수 오버플로가 없다는(깨진) 가정 때문이라고 똑같이 주장할 수도 있습니다. 정말 중요한 것은 “이 코드는 정확하다고 증명되었다”가 실제로 여러분에게 _무엇을 말해 주는지_를 명확히 이해하는 것입니다. 어디에서 안전하게 쓸 수 있나요? 언제 걱정해야 하나요? 이 모든 것을 팀원들에게 어떻게 전달하나요?
세상에, 벌써 금요일이네
웹에서 이 글을 읽고 있다면 여기에서 구독할 수 있습니다. 업데이트는 주 1회입니다. 제 메인 웹사이트는 여기입니다.
제 신간, Logic for Programmers ,은 이제 얼리 액세스 중입니다! 여기에서 받아보세요.