머릿속에서 작은 증명을 하며 더 나은 프로그래머가 되는 방법

(the-nerve-blog.ghost.io)

1P by GN⁺ 23시간전 | ★ favorite | 댓글 1개

더 좋은 프로그래머가 되기 위해선 코드 작성 시 작은 증명을 머릿속으로 그리는 습관이 중요함
단조성, 불변성, 전제·결과 조건, 불변조건 등은 이런 미니 증명을 할 때 핵심적인 개념임
코드 변경이 시스템 전체에 미치는 영향 범위(격리, 파이어월)를 고려해 설계하는 것이 복잡도와 위험 줄임에 큰 도움이 됨
귀납법을 활용하면 재귀 함수나 구조의 올바름을 단계적으로 증명할 수 있음
이러한 사고는 연습과 습관화로 배양되며, 실제 수학적 증명 및 알고리듬 문제 풀이 훈련이 큰 도움임

소개 및 핵심 아이디어

필자는 경력을 쌓아가며 코드의 정확도와 속도를 높이기 위해 자연스럽게 ‘작은 증명을 그려보는 습관’ 을 갖게 되었음
코딩 중 예상 동작을 머릿속에서 검증하고 추론하는 과정은 연습이 필요하며, 능숙해지면 코드의 완성도가 눈에 띄게 향상됨
구체적으로 어떻게 하는지가 중요하지는 않고, 다양한 방식으로 본인에게 맞게 연습해볼 수 있음

단조성(Monotonicity)

단조성(monotonicity)은 함수나 코드가 한 방향으로만 진행하는 성질을 의미함
예시로 체크포인팅을 들 수 있는데, 이는 작업 단계가 앞으로만 나아가고, 이미 끝난 작업을 뒤로 돌아가 다시 실행하지 않음
LSM 트리와 비교되는 B-트리 예시에서, LSM 트리는 대부분 공간이 누적되며, 컴팩션 과정에만 줄어드는 특성을 가짐
단조성이 보장되면 복잡한 상태나 결과 일부를 자연스럽게 배제하거나 예측할 수 있음
불변성(immutability)도 유사한 개념으로, 한 번 설정된 값이 절대 바뀌지 않으므로 상태 변화의 가능성을 배제할 수 있음

전제 조건과 결과 조건(Pre- and post-conditions)

전제 조건(pre-condition)과 결과 조건(post-condition)은 함수가 실행되기 전후에 반드시 참이어야 하는 주장임
함수 작성 시 이 조건을 명시적으로 추적하면 논리적 사고 및 테스트에 도움이 됨
결과 조건을 명확히 규정하면 유닛 테스트 케이스를 더 쉽게 도출할 수 있음
코드에 이러한 조건을 검증하는 assertion을 추가하여 예기치 않은 상황에서 조기 중단되도록 하는 것이 예측가능성과 안전성을 높임
함수에 아예 명확한 전제/결과 조건을 부여하기 어려운 경우도 있는데, 이를 발견하는 것 자체도 시사점이 있음

불변조건(Invariants)

불변조건은 코드가 어떤 상황에서도, 실행 전·후·중에 항상 참이어야 하는 속성임
예를 들어 복식부기 회계의 회계 등식이 대표적인 불변조건 예시임 (총 대변 = 총 차변)
코드 전체를 작은 단계로 분리하고, 각 단계가 불변조건을 보존하는지 증명하면 전체의 무결성을 확보할 수 있음
불변조건을 유지하기 위해 리스너나 라이프사이클 메서드를 사용하는 방식(C++의 생성자/소멸자, React의 useEffect 등)이 있음
변경점이 적거나 경로가 단순할 때 불변조건 검증이 훨씬 쉬움

격리(Isolation)

좋은 소프트웨어의 핵심 중 하나는 기존 시스템을 불안정하게 만들지 않고 새 기능을 추가·수정하는 것임
코드 변경의 ‘영향 반경’ (blast radius)을 파악하고, 구조적 ‘파이어월’ (방화벽)을 만들어 영향이 퍼지는 범위를 최소화해야 함
실제 서비스 Nerve의 예시에서, 쿼리 플래너와 쿼리 실행기의 경계를 명확히 하고, 변경된 부분이 이 경계를 넘지 않도록 설계하는 방식을 소개함
불필요한 변경 전파를 막으면 검증과 유지보수가 쉬워지고, 안정성이 높아짐
이는 OCP(Open-Closed Principle) 의 철학(기존 동작을 바꾸지 않고 기능을 확장)과도 일맥상통함

귀납법(Induction)

많은 프로그램이 재귀 함수 또는 재귀 구조를 포함하며, 이에 대한 논리를 정립할 때 귀납법이 강력하게 쓰임
재귀 함수의 동작과 올바름을 단계적으로 증명하려면, 기저(base) 케이스와 귀납 단계(inductive step)를 각각 검증해야 함
예시로 AST(구문 트리) 구조의 노드 단순화 과정을 들며, 각 단계별 귀납적 논증을 통해 불변조건 유지와 올바른 동작을 증명함
귀납법적 사고가 체화되면 재귀 코드 작성과 검증이 훨씬 직관적이고 쉬워짐
귀납적이 아닌 전역적(holistic) 검증 시도와 비교해보며 어느 방식이 더 자연스러운지 고찰해볼 만함

Proof-affinity(증명 친화성)이라는 품질 지표

필자는 ‘머릿속에서 작은 증명을 그려볼 수 있는 코드’가 좋은 코드라는 주장을 전개함
코드가 단조성, 불변성, 명확한 조건, 불변조건 분할, 화재벽 경계, 귀납법 활용 등의 구조를 가지면, 실제로 증명하기 쉬워지고, 따라서 코드 자체도 품질이 높아짐
코드가 이해하기 어렵고 검증이 힘든 상태라면 리펙터링이나 구조 재고가 필요함을 시사함
이때 ‘증명 가능성’ 대신 ‘proof-affinity’(증명 친화성)이라는 용어를 제안함
증명 친화성은 소프트웨어 품질의 유일한 요소는 아니지만, 코드의 이해·확장·테스트·유지에 매우 중요한 촉진제임

실력을 높이는 방법

이러한 논리적 사고 방식은 연습이 쌓여야 무의식 중에 자연스럽게 적용됨
(수학적) 증명을 자주 써보고 논리적 추론 능력을 기르는 것이 필수임
알고리듬 문제 풀이(Stanford의 EdX 강의, Leetcode 등)도 좋은 훈련장이 되며, 단순 요령 문제가 아닌 꼼꼼한 구현과 증명적 사고가 필요한 문제를 집중하면 성과를 높일 수 있음
여러 번 결과를 고쳐가며 맞추기보다는, 한 번에 정답에 가까이 접근하려는 연습이 중요함
이런 습관화를 통해 논리적 시스템 설계와 코드 품질이 큰 폭으로 향상됨

▲

GN⁺ 23시간전 [-]

Hacker News 의견

이 주제에 딱 맞는, 단순하지만 놀라운 예시가 있음. 바로 이진 탐색임. 왼쪽, 오른쪽 변형도 있지만, 루프 불변식에 대해 생각하지 않으면 제대로 구현하기 매우 어려움. 이 글에서 불변식 접근법과 그에 맞는 파이썬 코드 예시를 설명해둠. Programming Pearls의 저자 Jon Bentley가 IBM 프로그래머들에게 평범한 이진 탐색을 구현해 보라고 했더니 90%가 버그가 있었음. 주로 무한 루프에 빠지는 실수였음. 그 시절엔 정수 오버플로도 직접 막아야 했으니 어느 정도 이해는 되지만, 그래도 놀라운 비율임
- 이걸 보고 면접 질문으로 이진 탐색을 쓰기 시작했음. 잘 알려진 지원자들 중 약 2/3가 20분 이내에 제대로 동작하는 구현을 못 했음. 특히 쉬운 케이스에서 무한 루프에 빠지는 경우가 많았음. 성공한 사람들은 빠르게 구현했음. 문제의 원인 중 하나는 잘못된 인터페이스로 학습된 경우가 많음. 위키피디아 설명도 "L을 0으로, R을 n-1로 초기화"라고 설명하는데, 이건 R이 포함된 범위임. 실제로는 대부분의 문자열 알고리즘에서 상한을 포함하지 않는, 즉 R이 n인 형태가 더 나음. 이 가설을 직접 실험해보고 싶음. 서로 다른 함수 프로토타입과 초기값으로 많은 사람들에게 작성하게 해보고, inclusive와 exclusive upper bound, length 방식을 쓸 때 버그가 얼마나 나오는지 비교하고 싶음
- 사실 이진 탐색은 인덱스 관리가 거의 가장 까다로운 대표 예시임. Hoare 파티션 알고리즘과 더불어 실수 없이 정확하게 코딩하기 가장 어려운 기본 알고리즘임
- 테스트 삼아서 Claude Sonnet에게 버그 없는 이진 탐색 파이썬 코드를 작성하게 시켜봤음
```
def binary_search(arr, target):
    left = 0
    right = len(arr) - 1
    while left <= right:
        mid = left + (right - left) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            left = mid + 1
        else:
            right = mid - 1
    return -1
```
예제 배열로 다양한 테스트 케이스도 확인함
- 이진 탐색 버그가 잘못된 모범 사례로 유명하단 걸 알고 버그 없는 첫 구현을 책에 실어보겠다고 도전함. 정말 신중하게 작성했지만 그래도 버그가 있어서 웃음이 남. 다행히 Manning의 사전 피드백 시스템 덕분에 인쇄 전에 수정할 수 있었음
- 나는 왼쪽/오른쪽 이진 탐색 구현을 항상 "이전까지 가장 좋은 값"을 기억하며 구현함. C++의 lower_bound, upper_bound 같은 방식임. while (l < r) 구조에서 중간 지점을 찾고, 현재 위치를 체크하여 알맞게 범위를 조정함. 예시로 upper_bound면 좌측 경계를 올리고, lower_bound면 우측 경계를 내리는 식임. 오랜만에 leetcode 풀다가 머리가 멍해서 포맷이 엉망일 수 있음
오래전에 대학원 수업에서 이와 비슷한 개념을 알게 된 듯함. 학부 마지막 즈음부터 수학 시험을 아예 볼펜으로만 치렀음. 이유는 잘 몰랐는데 성적이 늘 높았고, 한 번에 풀어가며 아예 머릿속에서 풀이 과정을 완전히 그려놓고 썼기 때문임. 덕분에 실수가 많이 줄었음. 코딩할 때도 이런 식으로 머릿속에서 완성도 있게 설계해두고 시작함
더 나은 프로그래머가 되려면 코드에 작은 증명을 작성하는 습관을 들여야 함 테스트와 타입 정의가 바로 그런 행위의 예임 특히 테스트를 먼저, 그 다음 타입, 마지막에 코드 작성 순서로 접근함 각각의 acceptance criteria별로 테스트를 만들고, 입력/출력이 명확하게 설명된 테스트를 작성함이 바람직함 API라면 OpenAPI나 GraphQL로 모든 속성과 타입 포함해 명세를 먼저 만들 수 있음. 런타임에서 이 명세 기반으로 데이터 검증이 가능하고, 이 명세서 자체가 앱이 명세대로 동작한다는 증명이 됨 요약하자면 OpenAPI/GraphQL, 테스트, 타입을 통해 실제로 시스템이 의도한 대로 동작한다는 증명을 확보함이 중요함 명세 자체를 먼저 잘 설계하면 코드 구현은 유연하게 바꿔도 명세로 올바름을 증명할 수 있음 코드 자체보다 명세가 더 중요함
- 글에서 언급된 다섯 속성은 좋은 타입 시스템에서 표현 가능함. 이런 방법으로 명세의 상당 부분이 코드가 되고, 컴파일러가 올바름을 보장해줌. 프로그래밍의 미래는 이런 접근이 당연해지는 방향이어야 함 OpenAPI와 GraphQL의 타입 시스템은 너무 빈약해서, 이런 미래에 도달하려면 50년은 발전이 더 필요함
대학에서 이론 컴퓨터 과학 기초를 배웠고, 이 글의 취지에 공감함. 실천이 쉽지는 않음 사전/사후 조건 외에도, 루프 불변식(loop invariant), 구조적 귀납법(structural induction) 같은 CS 증명 테크닉이 매우 강력함 loop invariant, structural induction 링크와 함께, UofT CSC236H 강의 노트(강의 노트)를 추천함
- 이 CSC236 강의노트가 매우 훌륭하고, David Liu 교수도 정말 괜찮은 분임 교수 소개
- UofT 언급됐네! 반갑다는 마음임
"코드에 대해 머릿속에서 작은 증명을 직접 만들어보기"란 주장은 자명해야 할 정도로 중요한 원칙임. 코드의 각 부분이 무엇을 하는지에 대한 간단한 명제를 늘 의식해야 함
- 이 취지는 그린필드 프로젝트(최근에 직접 모든 코드를 쓴 경우)에서는 쉽지만, 다양한 함수나 글로벌 상태를 여러 개발자가 건드리는 진짜 코드베이스에서는 훨씬 어렵게 느껴짐
  - 진짜 좋은 개발자는 시스템을 점차 이런 방향으로 발전시키는 능력이 있음. 현실 세계의 코드는 엉망이지만, 인바리언트의 구멍을 점진적으로 줄이고, 후속 개발자들도 인바리언트를 인지한 채 그 유지에 우호적인 코드 구조를 만들어주는 것이 중요함. 문서도 도움 되지만, 내 경험상 코드 구조 자체가 그보다 더 큰 역할임
  - 사실 글로벌 상태가 위험한 결정적 이유가 이 점임. 코드의 정확성을 증명하려면 프로그램 전체를 알아야 하기 때문임. 전역 변수를 불변값으로 바꾼다든지, 함수 인자로 넘기거나, 상태를 감싸는 래퍼 클래스로 관리하면 그 함수의 호출자들만 명확히 파악하면 됨. 함수 내부에 어설션 등으로 더 제약을 추가하면 증명 난이도가 확실히 낮아짐. 이미 많은 프로그래머가 이런 결정을 하고 있지만, 증명을 의식하지 않고 본능적으로 그렇게 하고 있을 뿐임
  - 전역 상태를 여러 개발자가 관리하는 코드는 "암이 전이된" 환자와 비유할 수 있음. 치료가 훨씬 힘들고, 운과 외부 조건에 따라 살릴 수 있는 경우도 있음
  - 기사에서 말한 것처럼, 이런 코드는 버그가 생길 확률이 훨씬 높고, 유지보수로 인한 추가 버그 가능성도 큼. 처음부터 증명 가능한 구조로 작성하는 것이 훨씬 올바른 길임을 보여줌
  - 이 글을 읽고 내가 코딩 방식에 대해 끊임없이 다시 고민하고, 더 나은 방향에 대해 재정립하려 노력하는 모습을 떠올리게 됨. John Carmack 같은 개발자도 시간이 지나면 자신의 예전 코드가 부족했다 느끼고, 더 "잘" 해나가는 감각이 있을지 궁금함
코드가 증명 가능해야 한다는 생각은 Dekker가 1959년 mutual exclusion 문제를 해결하면서 처음 드러난 개념임. 이에 관한 재밌는 일화가 Dijkstra의 글 EWD1303(원문 링크)에 소개됨. Dijkstra의 후속 연구도 이 통찰의 연장선상에서 이어진다고 볼 수 있음
올바른 증명을 작성하는 건 정말 어려움. 프로그램 검증도 마찬가지로 쉽지 않음. 내 생각엔, 수작업으로 증명하려 들면 효율이 없음. 해당 언어와 코드베이스의 관용적인(idiomatic) 코드를 작성하면 불변식이나 사전/사후 조건 신경 쓸 일이 별로 없음. R. Pike와 B. W. Kernighan의 "The Practice of Programming"에서 강조하는 "단순함, 명확함, 범용성"이 실무에서는 아주 큰 효과가 있음. 약간 관련 있지만 다른 얘기로, competitive programming을 해보면 코드의 정확성을 보장하는 기법을 확실히 익혀야 다음 단계로 도달할 수 있음
- 여기에 동의할 수 없음. 글 작성자가 말한 건 완전한 형식적 증명이 아니라, 자신의 코드에 어떤 논리적 속성이 보장되는지(예: 인바리언트) 꼭 고민하라는 점이라 생각함. 이 과정이 코드를 이해하고, 내용의 두려움을 해소하는 가장 좋은 길임
- 여기선 오히려 원인과 결과가 바뀐듯함. 문제를 신중히 생각하면서 접근하면 그 결과 코드도 자연스럽게 명료하고 깔끔해짐. 논리가 명확해야 코드 설계도 명확해짐. 하지만 코드를 예쁘게 쓴다고 해서 그 자체로 정확성이 따라오리라 믿는 건 어불성설임. 물론 코드가 깔끔할수록 코드 리뷰 등에서 버그가 줄어드는 건 사실임. 형태는 기능을 따른다는 점을 유념해야 함
- 증명의 가장 기본 개념은 "이게 왜 맞는지에 대한 근거"임. 사소한 실수 방지용이 아니라, 근본적으로 방향성이 맞는지 확인하는 과정임
- 코드의 정확성을 위해선 올바르게 코드를 작성하는 것 외 다른 어떤 대체 방법도 없음. 어렵더라도 무조건 올바르게 짜야 함
- 첫 문단을 완전히 뒤집어보면, 적절한 추상화(즉 언어/코드베이스에 맞는 관용적 코드)가 있으면 프로그램 검증이 쉬워짐. 적절한 추상화에서 루프 불변식 등을 고민할 필요가 없기 때문에, 코드의 옳음에서 증명이 바로 따라옴
가변성과 불변성(mutable/immutable) 역시 중요한 속성임. 최대한 상태를 불변으로 두면, 멀티스레딩뿐 아니라 프로그램의 상태 추론에서도 복잡도가 줄어듦
- 원문 기사에 이미 그런 내용이 포함돼 있음
80년대에 Carnegie Mellon에서 학부 시절 이런 원칙을 명확히 교육받았음. 이후 내 인생에서 큰 도움이 됐음. 특히 재귀와 귀납법의 동등성을 배운 순간, 재귀 알고리즘을 "답 나올 때까지 마구 시도" 대신 깔끔하게 접근할 수 있게 됐던 기억이 남
- 최근에 그 강의를 들었고, 함수형 프로그래밍 들으면서 더 크게 깨달음을 얻었음

답변달기