토니 호어의 정확성 아이디어: 논리에서 안전한 코드로

왜 “정확성”이 단순히 “대충 돌아간다”와 다른가\n\n사람들이 프로그램이 “정확하다”고 말할 때 보통 의미하는 바는: “몇 번 돌려봤고 출력이 괜찮아 보였다.” 이것도 유용한 신호이지만, 정확성은 그보다 엄격합니다. 간단히 말해, 정확성은 프로그램이 명세를 만족한다는 뜻입니다: 허용된 모든 입력에 대해 요구된 결과를 내고 상태 변경, 시간 제약, 오류 처리 규칙을 지킨다는 의미입니다.\n\n문제는 “명세를 만족한다”는 말이 들리는 것보다 훨씬 어렵다는 점입니다.\n\n### 정확성이 진짜로 어려운 이유\n\n첫째, 명세는 종종 모호합니다. 제품 요구서에 "리스트를 정렬하라"라고만 적혀 있다면, 안정 정렬(stable sorting)을 의미하는가? 중복 값, 빈 리스트, 숫자가 아닌 항목은 어떻게 처리할 것인가? 명세에 명시되어 있지 않으면 사람마다 다른 가정을 하게 됩니다.\n\n둘째, 엣지 케이스는 드물지 않습니다—단지 덜 자주 테스트될 뿐입니다. 널 값, 오버플로, 오프바이원 경계, 특이한 사용자 순서, 예상치 못한 외부 실패는 “대충 작동하던” 코드가 실제 운영에서 실패하게 만들 수 있습니다.\n\n셋째, 요구사항은 변합니다. 어제의 명세에 대해 올바른 프로그램이 오늘의 명세에 대해서는 틀릴 수 있습니다.\n\n### 이 글에서 기대할 것들\n\n토니 호어의 큰 공헌은 “모든 것을 항상 수학적으로 증명하자”는 주장만이 아닙니다. 그가 제시한 핵심은 우리가 코드가 무엇을 하기로 되어 있는지를 더 정확하게 말하고, 규율 있게 추론할 수 있다는 아이디어입니다.\n\n이 글에서는 세 가지 연결된 주제를 따라갑니다:\n\n- 호어 논리: 사전조건과 사후조건을 사용하는 가벼운 구조화된 추론\n- 퀵소트: 파티션 같은 작은 “자명해 보이는” 단계가 얼마나 신중한 사고를 요구하는지 드러내는 친숙한 알고리즘\n- 안전성 사고방식: 실패가 실제로 결과를 초래할 수 있을 때의 실용적 책임으로서의 정확성\n\n대부분의 팀이 모든 것을 완전한 형식 증명으로 작성하진 않을 것입니다. 하지만 부분적, ‘증명 스타일’의 사고만으로도 버그를 더 쉽게 찾고 리뷰를 날카롭게 하며 코드가 배포되기 전에 동작을 명료하게 만드는 데 도움이 됩니다.\n\n## 토니 호어 간단 소개: 일상 코드에 닿은 아이디어들\n\n토니 호어는 논문이나 교실에만 머물지 않은 드문 컴퓨터 과학자 중 하나입니다. 그는 학계와 산업계 사이를 오가며 모든 팀이 여전히 직면한 실용적 질문에 관심을 가졌습니다: 특히 이해관계가 클 때, 우리가 프로그램이 우리가 생각하는 대로 동작한다고 어떻게 알 수 있나?\n\n### 이 글에서 중요한 기여들\n\n이 글은 실무 코드베이스에서 계속 나타나는 몇 가지 호어 아이디어에 초점을 맞춥니다:\n\n- 호어 논리: 사전조건, 사후조건, 잘 알려진 호어 트리플 {P} C {Q}로 프로그램 동작을 기술하는 방법\n- 루프 불변식: 루프를 "내 머신에서 돌아가더라" 수준을 넘어서서 추론하는 규율적 습관\n- 퀵소트(특히 파티션 단계): 정확한 진술이 많은 것을 명료하게 하는 유명한 예시\n- 안전성 사고방식: 정확성은 사치가 아니라 불편함과 피해를 가르는 차이일 수 있다는 마인드셋\n\n### 이 글에서 하지 않을 것\n\n여기서는 깊은 수학적 정형화(formalism)를 다루지 않으며, 퀵소트의 완전한 기계검증 증명을 시도하지도 않습니다. 목표는 개념을 접근 가능하게 유지하는 것입니다: 여러분의 추론을 더 명확히 해줄 만큼의 구조는 제공하되, 코드 리뷰를 대학원 세미나로 바꾸지는 않겠습니다.\n\n### 그의 작업이 일상 프로그래밍에 영향을 미치는 이유\n\n호어의 아이디어는 일상적인 결정으로 번역됩니다: 함수가 어떤 가정에 의존하는지, 호출자에게 무엇을 보장하는지, 루프 중간에 무엇이 유지되어야 하는지, 리뷰에서 “거의 맞는” 변경을 어떻게 발견할지 등에 관한 것입니다. {P} C {Q}를 명시적으로 적지 않더라도 그런 형태로 생각하면 API, 테스트, 까다로운 코드에 대한 논의의 질이 좋아집니다.\n\n## 실무에서 ‘정확성’이 의미하는 것\n\n호어의 관점은 “몇 가지 예제를 통과했다”보다 엄격합니다: 정확성은 합의된 약속을 지키는 것입니다, 외형상 올바른 것처럼 보이는 것과는 다릅니다.\n\n### 요구사항 vs 명세 vs 구현\n\n- 요구사항(requirements): 이해관계자가 원하는 바를 평문으로 적은 것(무엇을 원하나)\n- 명세(specification): 그 요구를 정확하고 검사 가능한 형태로 옮긴 것(함수가 무엇을 해야 하는가)\n- 구현(implementation): 여러분이 작성한 코드(어떻게 하는가)\n\n버그는 팀이 중간 단계(명세)를 건너뛰고 요구사항에서 바로 코드로 넘어갈 때 자주 발생합니다. 약속이 흐릿해집니다.\n\n### 부분적 정확성 vs 전칭적 정확성\n\n자주 혼동되는 두 주장이 있습니다:\n\n- 부분적 정확성(Partial correctness): 코드가 반환한다면 결과가 올바르다.\n- 전칭적(전체) 정확성(Total correctness): 코드가 반환하고 그 결과가 올바르다. (즉 종료성도 주장에 포함)\n\n실제 시스템에서는 ‘끝나지 않음’이 잘못된 답을 내는 것만큼 해로울 수 있습니다.\n\n### 정확성은 항상 가정에 의존한다\n\n정확성 주장은 결코 보편적이지 않습니다; 다음과 같은 가정에 의존합니다:\n\n- 입력(예: 리스트가 메모리에 들어간다, 요소들이 비교 가능하다)\n- 제약(예: 시간 제한, 정수 범위)\n- 환경(예: 동시성, I/O 실패, 설정)\n\n가정을 명시적으로 쓰면 “내 머신에선 된다”는 말을 다른 사람이 추론 가능하게 만듭니다.\n\n### 작은 명세 예시\n\n함수 sortedCopy(xs)를 생각해보세요.\n\n유용한 명세는 다음과 같을 수 있습니다: “새 리스트 ys를 반환하되 (1) ys는 오름차순으로 정렬되어 있고, (2) ys는 xs와 정확히 같은 요소들을 갖는다(각 요소의 개수 동일), (3) xs는 변경되지 않는다.”\n\n이제 ‘정확하다’는 것은 이 세 조건이 명시된 가정 아래 코드에 의해 만족되는 것을 의미하며, 단순히 출력이 빨리 보기에는 정렬되어 보이는 것과는 다릅니다.\n\n## 호어 논리 기본: 사전조건, 사후조건, 삼중관계\n\n호어 논리는 계약처럼 코드에 대해 말하는 방법입니다: 특정 가정을 만족하는 상태에서 이 코드 조각을 실행하면 특정 보증을 가진 상태로 끝난다는 식으로요.\n\n핵심 표기법은 호어 트리플(Hoare triple)입니다:\n\n{precondition} program {postcondition}\n\n### 사전조건(Preconditions): 무엇을 가정하나\n\n사전조건은 코드 조각이 실행되기 전에 참이어야 할 사실을 말합니다. 이는 여러분이 바라거나 기대하는 것이 아니라 코드가 실제로 필요로 하는 것입니다.\n\n예: 두 수의 평균을 오버플로 검사 없이 계산하는 함수가 있다고 합시다.\n\n- 사전조건: a + b가 정수 타입 범위를 넘지 않는다\n- 프로그램: avg = (a + b) / 2\n- 사후조건: avg는 a와 b의 수학적 평균과 같다\n\n사전조건이 만족되지 않으면(오버플로 가능) 사후조건의 약속은 더 이상 적용되지 않습니다. 트리플은 그 점을 명확히 말하게 합니다.\n\n### 사후조건(Postconditions): 무엇을 보장하나\n\n사후조건은 코드가 실행된 후(사전조건이 만족되었다는 가정 하에) 참일 것을 보장합니다. 좋은 사후조건은 구체적이고 검사 가능해야 합니다. “결과가 유효하다” 대신에 유효가 무슨 의미인지(정렬됨, 음수 아님, 범위 내, 특정 필드를 제외하고 변경되지 않음 등)를 분명히 쓰세요.\n\n### 할당과 순차 실행(상징을 과하게 쓰지 않고)\n\n호어 논리는 작은 문장부터 다단계 코드까지 확장됩니다:\n\n- 할당(assignment)은 상태를 정확히 변경합니다. x = x + 1 이후 x에 대해 어떤 사실이 참인지 묻는 식으로 추론합니다.\n- 순차(sequencing)는 보증을 연결합니다: 1단계가 2단계의 사전조건을 성립시키면 전체 블록을 신뢰하기가 쉬워집니다.\n\n요점은 모든 곳에 중괄호를 뿌려대는 것이 아니라 의도를 읽기 쉽게 만드는 것입니다: 명확한 가정, 명확한 결과, 그리고 리뷰에서 “대충 돌아가더라”식 대화가 줄어드는 것.\n\n## 실무 팀이 쓸 수 있는 루프 불변식\n\n루프 불변식은 루프가 시작되기 전 참이고 각 반복 뒤에도 유지되며 루프가 끝났을 때도 여전히 참인 주장입니다. 단순한 아이디어지만 큰 보상이 있습니다: ‘대충 돌아가는 것 같다’는 추론을 루프의 각 단계에서 실제로 점검 가능한 주장으로 바꿔줍니다.\n\n### 불변식이 손으로 하는 추정적(reasoning) 사고를 멈추게 하는 이유\n\n불변식이 없으면 리뷰는 종종 “리스트를 순회하며 점차 고친다” 같은 표현이 됩니다. 불변식은 “지금 정확히 무엇이 이미 올바른가”를 강제합니다. 루프가 끝나지 않았더라도 어떤 부분이 이미 정확한지 명확히 말할 수 있으면 오프바이원 버그나 누락된 경우가 불변식이 깨지는 순간으로 드러납니다.\n\n### 재사용 가능한 불변식 템플릿\n\n일상 코드의 대부분은 몇 가지 신뢰할 수 있는 템플릿을 사용할 수 있습니다.\n\n1) 경계 / 인덱스 안전\n\n인덱스를 안전한 범위로 유지합니다.\n\n- 0 <= i <= n\n- low <= left <= right <= high\n\n이 유형의 불변식은 범위 밖 접근을 방지하고 배열 추론을 구체화하는 데 유용합니다.\n\n2) 처리된 항목 vs 미처리 항목\n\n데이터를 “완료된 영역”과 “아직” 영역으로 나눕니다.\n\n- “a[0..i)의 모든 요소는 검사되었다.”\n- “result로 옮겨진 모든 항목은 필터 술어를 만족한다.”\n\n이렇게 하면 모호한 진행 상황이 ‘지금 무엇이 처리되었나’에 대한 명확한 계약으로 바뀝니다.\n\n3) 정렬된 접두사(또는 분할된 접두사)\n\n정렬, 병합, 분할에서 흔히 사용됩니다.\n\n- “a[0..i)는 정렬되어 있다.”\n- “a[0..i)의 모든 항목은 <= pivot이고 a[j..n)의 모든 항목은 >= pivot이다.”\n\n전체 배열이 아직 정렬되지 않았더라도 어떤 부분이 고정되어 있는지를 고정해 둡니다.\n\n### 종료성(termination)을 평범하게 말하면: 줄어드는 측정값\n\n정확성은 단지 ‘정확한 결과’뿐 아니라 루프가 끝나야 한다는 점도 포함합니다. 이를 주장하는 간단한 방법은 측정값(variant)을 이름 붙이는 것인데, 보통 각 반복에서 감소하고 무한히 감소할 수 없는 값입니다.\n\n예:\n\n- “n - i가 매 반복마다 1씩 줄어든다.”\n- “미처리 항목의 수가 감소한다.”\n\n줄어드는 측정값을 못 찾으면 실제 위험(특정 입력에서 무한 루프)을 발견했을 수 있습니다.\n\n## 퀵소트: 코드 추론의 사례 연구\n\n퀵소트는 간단한 약속을 가집니다: 배열의 일부 구간을 주면 그 요소들을 비감소 순서로 재배열하되, 값을 잃거나 새로 만들어내지 않아야 합니다. 알고리즘의 높은 수준은 쉽게 요약됩니다:\n\n1. 피벗 값을 고른다.\n2. 범위를 파티션하여 피벗보다 작은 요소는 한쪽으로, 피벗보다 큰 요소는 다른 쪽으로 옮긴다(‘같음’ 처리 규칙 포함).\n3. 왼쪽과 오른쪽 부분 범위에 대해 재귀를 수행한다.\n\n퀵소트는 머릿속에 넣기에는 작지만 비공식적 추론이 실패하는 지점을 보여주기에는 충분히 풍부해서 정확성 교육용으로 좋습니다. 몇 번의 랜덤 테스트에서 “대충 동작하는” 퀵소트가 특정 입력이나 경계에서 여전히 잘못될 수 있습니다.\n\n### “자명해 보이는” 구현을 망가뜨리는 함정들\n\n주요 문제들:\n\n- 중복(Duplicates): 파티션이 ‘같음’을 일관되게 처리하지 않으면 부분 범위가 줄어들지 않아 무한 재귀가 생기거나 파티션 속성이 깨질 수 있습니다.\n- 빈 범위 또는 한 원소 범위: 기저(base) 케이스가 정확해야 인덱스 범위를 벗어나거나 무한 재귀에 빠지지 않습니다.\n- 오프바이원 인덱스: 파티션 알고리즘은 두 포인터를 쓰는 경우가 많고, 비교나 증가/감소가 하나 틀리면 요소를 건너뛰거나 범위를 벗어난 교환이 발생할 수 있습니다.\n\n### 실제로 증명해야 할 것\n\n호어식 방식으로 정확성을 주장하려면 일반적으로 증명을 두 부분으로 나눕니다:\n\n- 파티션 정확성: 파티션 후 왼쪽의 모든 요소는 피벗과의 관계를 만족하고, 오른쪽의 모든 요소는 반대 관계를 만족하며, 결과는 원래 요소의 순열(permutation)이다.\n- 재귀적 정확성: 재귀 호출은 엄밀히 더 작은 범위에서 동작하고(종료성), 만약 그 하위 범위들이 정렬된다면 전체 범위도 정렬된다는 것을 보인다.\n\n이 분리는 추론을 관리 가능하게 합니다: 파티션을 정확히 만들고 그 위에 정렬의 정확성을 쌓으면 됩니다.\n\n## 파티션 정확성: 퀵소트의 핵심\n\n퀵소트의 속도는 속이 되게 작은 루틴인 파티션에 달려 있습니다. 파티션이 조금이라도 잘못되면 퀵소트는 잘못 정렬되거나 무한 루프에 빠지거나 엣지 케이스에서 크래시 날 수 있습니다.\n\n### 파티션 계약(무엇을 보장해야 하는가)\n\n여기서는 고전적인 호어 파티션(Hoare partition) 방식(두 포인터가 안쪽으로 이동)을 사용합니다.\n\n입력: 배열 슬라이스 A[lo..hi]와 선택된 pivot 값(종종 A[lo]).\n\n출력: 인덱스 p를 반환하되 다음을 만족:\n\n- A[lo..p]의 모든 요소는 <= pivot\n- A[p+1..hi]의 모든 요소는 >= pivot\n\n약속하지 않는 것에 주의하세요: 피벗이 반드시 p 위치에 놓인다는 보장은 없고, 피벗과 같은 값들은 양측에 섞여 있을 수 있습니다. 그건 괜찮습니다—퀵소트는 올바른 분할만 필요로 합니다.\n\n### 스캔과 교환 중의 핵심 불변식\n\n알고리즘이 왼쪽에서 i, 오른쪽에서 j라는 두 인덱스를 이동시키는 동안 좋은 추론은 이미 “고정된” 것이 무엇인지에 초점을 둡니다. 실용적인 불변식 집합은:\n\n- A[lo..i-1]의 모든 항목은 <= pivot(왼쪽 부분은 깨끗함)\n- A[j+1..hi]의 모든 항목은 >= pivot(오른쪽 부분은 깨끗함)\n- A[i..j]의 모든 것은 분류되지 않음(아직 검사해야 함)\n\nA[i] > pivot이고 A[j] < pivot인 경우에 이 둘을 교환하면 이런 불변식들이 보존되고 분류되지 않은 가운데 영역이 줄어듭니다.\n\n### 정확성이 다뤄야 할 엣지 케이스\n\n- 모두 피벗보다 작음: i가 오른쪽으로 계속 이동해도 파티션은 종료되어 합리적인 p를 반환해야 합니다.\n- 모두 피벗보다 큼: j가 왼쪽으로 이동해도 동일한 종료 문제가 존재합니다.\n- 많은 같음: 비교를 < 대 <= 식으로 일관성 없이 쓰면 포인터가 멈춥니다. 호어 방식은 진행이 계속되도록 일관된 규칙에 의존합니다.\n- 이미 정렬/역순 정렬: 성능은 악화될 수 있지만 계약을 깨면 안 됩니다.\n\nLomuto, Hoare, three-way 등 다양한 파티션 방식이 있습니다. 핵심은 하나를 골라 그 계약을 명시하고 코드 리뷰에서 그 계약에 맞춰 일관되게 검토하는 것입니다.\n\n## 재귀에 대한 추론: 기저 사례와 종료성\n\n재귀는 언제 멈추는지와 각 단계가 왜 유효한지를 명확히 답할 수 있을 때 가장 신뢰하기 쉽습니다. 호어식 사고방식은 호출 전 무엇이 참이어야 하고 반환 후 무엇이 보장되는지를 명시하게 해주어 도움이 됩니다.\n\n### 기저(base) 사례는 정확해야 한다\n\n재귀 함수는 적어도 하나의 기저 사례가 있어야 하며, 이 경우 더 이상의 재귀 호출 없이 약속한 결과를 만족해야 합니다.\n\n정렬의 전형적 기저 사례는 “길이 0 또는 1의 배열은 이미 정렬되어 있다”입니다. 여기서 ‘정렬’은 명확히: 순서 관계 ≤에 대해 모든 인덱스 i < j에 대해 a[i] ≤ a[j]가 성립한다는 것을 의미합니다. (동일한 요소의 원래 순서를 유지하는지 여부는 안정성(stability)이라는 별도 속성입니다; 기본 퀵소트는 보통 안정적이지 않습니다.)\n\n### 부분 문제가 줄어들어야 한다\n\n각 재귀 단계는 반드시 엄밀히 더 작은 입력에 대해 자기 자신을 호출해야 합니다. 이 ‘축소’가 종료성의 근거입니다: 크기가 감소하고 0 이하로 더 줄일 수 없으면 무한히 재귀할 수 없습니다.\n\n축소는 스택 안전성(stack safety)에도 중요합니다. 올바른 코드라도 재귀 깊이가 너무 깊으면 크래시 납니다. 퀵소트에서는 편향된 분할이 깊은 재귀를 유발할 수 있습니다. 이것은 종료 증명 외에 최악의 경우 깊이를 고려하라는 실용적 알림입니다.\n\n### 정확성 우선, 성능은 그 다음\n\n퀵소트의 최악 시간 복잡도는 분할이 매우 편향되면 O(n²)로 악화될 수 있지만, 이는 성능 문제이지 정확성 실패는 아닙니다. 여기서의 추론 목표는: 파티션이 요소를 보존하고 피벗에 따라 분할한다고 가정하면, 하위 범위들을 재귀적으로 정렬했을 때 전체가 정의한 의미의 정렬 상태가 된다는 것입니다.\n\n## 증명 스타일 사고와 테스트: 어떻게 결합하나\n\n테스트와 증명 스타일의 추론은 같은 목표—신뢰성—을 향하지만 접근 방식이 다릅니다.\n\n### 테스트는 버그를 찾고, 추론은 버그 범주를 배제한다\n\n테스트는 구체적 실수를 잡아내는 데 탁월합니다: 오프바이원, 경계 누락, 회귀 등. 하지만 테스트 스위트는 입력 공간을 샘플링할 뿐입니다. 심지어 “100% 커버리지”도 모든 동작을 확인했다는 뜻이 아니라 주로 모든 코드 라인이 실행되었다는 뜻에 가깝습니다.\n\n증명 스타일의 사고(특히 호어식 추론)는 명세에서 출발해: 이 사전조건이 성립하면 코드가 항상 사후조건을 만족시키는가?를 묻습니다. 이를 잘하면 단순히 버그를 찾는 것을 넘어서 전체 범주(예: 배열 접근의 범위 초과 없음, 루프가 파티션 속성을 깨지 않음)를 배제할 수 있습니다.\n\n### 명세는 더 나은 테스트 케이스를 만들어낸다\n\n명확한 명세는 테스트 생성기의 역할을 합니다.\n\n사후조건이 “출력이 정렬되어 있고 입력의 순열이다”라고 하면 자동으로 테스트 아이디어가 생깁니다:\n\n- 경계: 빈 리스트, 한 원소, 이미 정렬된 리스트, 역순 정렬된 리스트\n- 불변식: 중간 속성들(예: 파티션이 <= pivot을 왼쪽에 유지한다)\n- 잘못된 입력: 널, NaN, 범위를 벗어난 인덱스, 비교자가 일관성 없는 경우\n\n명세가 무엇이 ‘정확함’인지 말해주고, 테스트는 현실이 그와 일치하는지 검사합니다.\n\n### 속성 기반 테스트(Property-based testing): 증명과 예제의 실용적 다리\n\n속성 기반 테스트는 증명과 예제 사이의 다리 역할을 합니다. 몇 가지 수동 사례 대신 속성을 선언하고 도구가 많은 입력을 생성하도록 합니다.\n\n정렬에 대해 두 가지 간단한 속성이 크게 도움이 됩니다:\n\n- 정렬성: 결과가 비감소 순서다.\n- 순열성: 결과가 입력과 정확히 같은 요소들을 가진다(개수 포함).\n\n이 속성들은 본질적으로 실행 가능한 사후조건입니다.\n\n### 팀이 실제로 쓸 수 있는 워크플로우\n\n확장 가능한 가벼운 루틴:\n\n1. 먼저 명세 쓰기(사전조건, 사후조건, 핵심 불변식).\n2. 까다로운 부분을 사고(루프, 파티션, 재귀 경계)에 대해 숙고.\n3. 명세를 테스트로 전환(경계 사례 + 속성 기반 검사).\n4. 명세와 테스트를 코드와 리뷰와 함께 보관하여 향후 변경이 원래 의도를 몰래 위반하지 않도록 함.\n\n이를 제도화하고 싶다면 PR 템플릿이나 코드 리뷰 체크리스트에 “명세 + 추론 노트 + 테스트”를 포함시키세요 (참고: /blog/code-review-checklist).\n\n채팅 기반 인터페이스에서 코드를 생성하는 워크플로우를 사용한다면(예: 분위기 코딩), 동일한 규율이 더 중요합니다. 예를 들어 Koder.ai에서는 Planning Mode에서 사전/사후조건을 고정한 다음 코드 생성 중 스냅샷과 롤백을 하며 속성 기반 테스트를 추가할 수 있습니다. 도구가 구현을 빠르게 해주지만 빠름이 ‘취약함’으로 바뀌지 않도록 지키는 건 여전히 명세입니다.\n\n## 안전성 사고방식: 실제 세계의 결과를 고려한 정확성\n\n정확성은 단지 “프로그램이 올바른 값을 반환한다”에 그치지 않습니다. 안전성 사고방식은 다른 질문을 던집니다: 어떤 결과가 받아들일 수 없으며, 코드가 스트레스받거나 오용되거나 부분적으로 실패할 때 그 결과를 어떻게 방지할 것인가? 실무에서 안전성은 우선순위가 있는 정확성입니다: 어떤 실패는 단순 불편이고, 어떤 실패는 재정적 손실, 개인정보 침해, 물리적 피해를 초래할 수 있습니다.\n\n### 위험(hazard) vs 버그: 왜 영향이 중요한가\n\n버그는 코드나 설계의 결함입니다. **위험(해저드, hazard)**은 받아들일 수 없는 결과로 이어질 수 있는 상황입니다. 같은 버그도 문맥에 따라 무해할 수도 있고 위험할 수도 있습니다.\n\n예: 사진 갤러리의 오프바이원 오류는 이미지를 잘못 라벨링할 수 있지만, 같은 오류가 약 복용량 계산기에서는 환자에게 해를 줄 수 있습니다. 안전성 사고방식은 코드 동작을 ‘명세 준수’가 아니라 결과와 연결시키도록 강제합니다.\n\n### 최악의 결과를 막는 간단한 기법들\n\n무거운 정형 기법 없이도 즉각적인 안전 이득을 얻을 수 있습니다. 팀이 채택할 수 있는 작고 반복 가능한 관행들:\n\n- 안전 실패 기본값(Fail-safe defaults): 시스템이 확신할 수 없을 때는 더 안전한 동작을 선택하세요. 예: 권한 검사 오류 시 허용하지 말고 거부하세요.\n- 경계에서의 입력 검증: 사용자 입력, 파일 내용, 네트워크 데이터는 신뢰하지 마세요. 유형, 범위, 형식, 불변식을 조기에 검증하세요.\n- 한도와 타임아웃: 메모리 사용, 요청 크기, 재귀 깊이, 재시도 횟수, 실행 시간을 제한하세요. 많은 사고는 ‘정상’인 코드가 비정상적인 입력에서 실행될 때 발생합니다.\n\n이 기법들은 호어식 사고와 자연스럽게 결합됩니다: 사전조건을 명시하고(허용할 입력), 사후조건에 안전 속성을 포함시키면(절대 발생하면 안 되는 것들) 됩니다.\n\n### 트레이드오프: 검사에는 비용이 따른다\n\n안전 중심 검사는 비용을 동반합니다—CPU 시간, 복잡성, 때로는 거짓된 거부(사용자 불편).\n\n- 성능 vs 검사: 빠른 경로는 중요하지만 중요한 경계는 검증, 속도 제한, 타임아웃을 둘 가치가 있습니다.\n- 엄격성 vs 사용성: 모든 불완전한 입력을 거부하면 사용자가 불편해합니다; 모든 것을 허용하면 모호성과 악용을 초래할 수 있습니다. 현실적 타협은 “핵심에서는 엄격하게, 가장자리에서는 관대하게”이고, 가장자리 사례가 얼마나 자주 발생하는지 로깅하고 측정하는 것입니다.\n\n안전성 사고방식은 우아함을 증명하려는 것이 아니라 감당할 수 없는 실패 모드를 예방하려는 것입니다.\n\n## 호어식 사고를 코드 리뷰에 적용하기\n\n코드 리뷰는 정확성 사고가 가장 빠르게 효과를 내는 곳입니다. 그곳에서 누락된 가정을 프로덕션 이전에 발견할 수 있습니다. 호어의 핵심 동작—‘무엇이 들어오기 전에 참이어야 하고, 끝난 뒤 무엇이 참이어야 하는가’를 명확히 하는 것—은 리뷰 질문으로 곧장 옮겨갑니다.\n\n### 호어 아이디어를 리뷰 질문으로 바꾸기\n\n변경을 읽을 때 주요 함수마다 작은 약속처럼 다음을 프레이밍해보세요:\n\n- 가정(사전조건): 입력, 상태, 환경에 대해 무엇이 참이어야 하는가?(예: “리스트는 비어 있지 않다”, “사용자가 인증되었다”, “락이 걸려있다”)\n- 보장(사후조건): 그 뒤에 무엇이 참인가? 반환값과 부작용을 포함하여(예: “잔액이 금액만큼 감소했다”, “레코드가 단 한 번 삽입되었다”)\n- 불변식: 루프, 재시도, 다단계 워크플로에서 무엇이 유지되어야 하는가?(예: “processed_count ≤ total”, “지금까지의 차감 합계는 동일”)\n- 오류 동작: 에러 시 시스템을 안전한 상태에 남기는가? 부분 업데이트는 롤백되는가?\n\n간단한 리뷰 습관: 사전/사후 조건을 한 문장으로 말할 수 없다면 코드가 더 명확한 구조가 필요할 가능성이 큽니다.\n\n### 중요한 함수에 대한 ‘계약 주석(Contract comments)’\n\n위험하거나 중심이 되는 함수에는 시그니처 바로 위에 작은 계약 주석을 추가하세요. 구체적으로: 입력, 출력, 부작용, 오류를 적습니다.\n\n```python

def withdraw(account, amount): """Contract: Pre: amount is an integer > 0; account is active. Post (success): returns new_balance; account.balance decreased by amount. Post (failure): raises InsufficientFunds; account.balance unchanged. """ ...

이 주석들은 형식적 증명은 아니지만 리뷰어가 구체적으로 체크할 것을 제공합니다.\n\n### 위험한 코드에 대한 경량 체크리스트\n\n파싱/검증(잘못된 입력 경로, 경계 사례), 동시성(락, 경쟁, 멱등성, 재시도), 금전/쿼터(반올림, 이중 청구, 오버플로), 권한(누가 무엇을 할 수 있는지) 등을 다루는 코드는 더 명시적으로 다루세요.\n\n변경이 이런 부분을 건드리면 항상 묻습니다: “사전조건은 무엇이고 어디에서 강제되는가?” 그리고 “무언가 실패했을 때도 어떤 보장을 제공하나?”\n\n## 언제 형식 도구를 쓰고, 실용적 체크리스트\n\n형식적 추론이 코드베이스 전체를 수학 논문으로 바꾸는 것을 의미할 필요는 없습니다. 목표는 보통의 리뷰+테스트로는 부족한 곳에 추가 확실성을 투입하는 것입니다: 테스트만으로는 충분치 않은 작은 핵심 모듈(인증, 결제 규칙, 권한, 안전 인터록)이거나 오프바이원 버그가 오래 숨어있을 수 있는 까다로운 알고리즘(파서, 스케줄러, 캐시/삭제 정책, 파티션 스타일 코드 등)입니다.\n\n### 형식 기법이 가장 도움이 되는 곳\n\n작고 중요한 모듈(모든 것이 의존하는 핵심)이나 상태공간이 복잡한 시스템(프로토콜, 동시성, 상태 기계)에서 특히 효과적입니다. 유용한 규칙: 버그가 실제 손해, 큰 재정 손실, 또는 묵시적 데이터 손상으로 이어질 수 있으면 평범한 리뷰+테스트 이상이 필요합니다.\n\n### 고려해볼 도구들(개요)\n\n가볍게부터 무겁게까지 선택할 수 있고, 보통 결합해서 쓰는 것이 효과적입니다:\n\n- **타입 시스템**(널 비허용, 단위/측정 단위 포함): 잘못된 상태 범주를 예방\n- **정적 분석**: 의심스러운 경로, API 오용, 데이터 경쟁, 타깃 불량 흐름 탐지\n- **계약(사전/사후조건, 어서션)**: 호어식 진술의 실행 가능한 버전\n- **모델 검사**: 상태 기계 탐색(프로토콜, 동시성에 유용)\n- **형식 검증(Formal verification)**: 가장 높은 보증이 필요한 부분에 대해 기계 검증 증명\n\n### 얼마나 깊게 해야 하나?\n\n형식성의 깊이는 다음을 저울질해 결정하세요:\n\n- **위험**: 영향 × 발생 가능성. 위험이 높으면 더 강한 보증이 필요합니다.\n- **비용**: 명세화, 증명, 유지보수에 드는 시간.\n- **변경 빈도**: 빨리 바뀌는 코드는 형식적으로 고정하기 어렵습니다; 먼저 인터페이스를 안정화하세요.\n- **팀 역량**: 증명이 개발 속도를 지나치게 늦추면 계약과 정적 분석부터 시작하세요.\n\n실무에서는 형식성을 점진적으로 추가할 수 있습니다: 먼저 명시적 계약과 불변식을 쓰고 자동화로 이를 지속적으로 검증하게 하세요. Koder.ai처럼 빠르게 프런트엔드, 백엔드, 스키마를 생성하는 팀에서도 스냅샷/롤백과 소스 내보내기는 빠른 반복을 가능하게 하면서 테스트와 정적 분석으로 계약을 지키게 해줍니다.\n\n### 실용적 체크리스트\n\n계획이나 코드 리뷰에서 “더 형식적으로 해야 하나?”를 판단하는 빠른 게이트로 사용하세요:\n\n1. 최악의 현실적 실패는 무엇이고 누가 피해를 입는가(사용자, 운영, 규제당국)?\n2. 테스트로 중요한 경계 사례와 상태를 현실적으로 커버할 수 있나?\n3. 로직이 상태적(stateful), 동시성, 또는 불변식/경계에 민감한가?\n4. 공개 진입점에 대해 명확한 사전/사후조건을 쓸 수 있나?\n5. 더 깊이 검증할 수 있는 작은 핵심을 분리할 수 있나?\n6. 여기서 가장 가성비 좋은 도구는 무엇인가: 강한 타입, 정적 분석, 계약, 모델 검사, 증명 중 무엇인가?\n7. 다음 분기에는 무엇이 바뀔 것이며 약속이 흐려지지 않게 하려면 어떻게 할 것인가?\n\n추가 읽을거리: 디자인 바이 컨트랙트(design-by-contract), 속성 기반 테스트, 상태 기계에 대한 모델 검사, 언어별 정적 분석기, 증명 도구와 형식 명세 입문 자료 등.