▲
GN⁺ 9달전 | parent | ★ favorite | on: 머릿속에서 작은 증명을 하며 더 나은 프로그래머가 되는 방법(the-nerve-blog.ghost.io)
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에서 학부 시절 이런 원칙을 명확히 교육받았음. 이후 내 인생에서 큰 도움이 됐음. 특히 재귀와 귀납법의 동등성을 배운 순간, 재귀 알고리즘을 "답 나올 때까지 마구 시도" 대신 깔끔하게 접근할 수 있게 됐던 기억이 남

    • 최근에 그 강의를 들었고, 함수형 프로그래밍 들으면서 더 크게 깨달음을 얻었음