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

17 hours ago 2

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

소개 및 핵심 아이디어

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

단조성(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 등)도 좋은 훈련장이 되며, 단순 요령 문제가 아닌 꼼꼼한 구현과 증명적 사고가 필요한 문제를 집중하면 성과를 높일 수 있음
여러 번 결과를 고쳐가며 맞추기보다는, 한 번에 정답에 가까이 접근하려는 연습이 중요함
이런 습관화를 통해 논리적 시스템 설계와 코드 품질이 큰 폭으로 향상됨

Read Entire Article