엔지니어링 철학: 에츠허르 데이크스트라, 우아함은 선택이 아니다

핵심 요약

• 우아함은 선택이 아닙니다. 데이크스트라에게 단순함은 정확성을 달성한 뒤에 받는 보상이 아니라 정확성의 전제 조건이었습니다. 완전히 이해할 수 없는 것은 증명할 수 없기 때문입니다.
• 증명이 테스트를 이깁니다. “테스트는 버그의 존재를 보여줄 뿐, 부재를 보여주지는 못합니다.” 정확성에 대한 확신은 프로그램을 추론하는 데서 나오지, 통과한 테스트를 쌓는 데서 나오지 않습니다.
• 코드를 짜기 전에 생각하세요. 그는 연필도 종이도 없이 최단 경로 알고리즘을 설계했고, 한 사람의 머릿속에 온전히 담길 만큼 작게 만들 수밖에 없었습니다. 그 제약이 우아함을 낳았습니다.
• 글쓰기가 곧 사고입니다. 만년필로 손수 쓴, 되돌리기가 없는 EWD 원고들은 논증이 잉크 속에서 성립하거나 무너지게 만들었습니다. 그는 같은 규율을 글에도 적용했습니다.

원칙

“단순함은 신뢰성의 전제 조건이다.” – 에츠허르 W. 데이크스트라, 출처 추정 (약 1975년)¹

이 문장은 한 줄짜리 격언처럼, 거의 여백에 적은 메모처럼 남아 1975년 무렵 그가 의도적으로 도발적으로 쓴 메모들과 함께 전해집니다. 맥락에서 떼어 놓고 보면 구호처럼 읽히지만, 데이크스트라는 이를 엄격한 논리적 주장으로 의도했습니다. 신뢰성이란 복잡한 시스템을 더 열심히 테스트해서 덧붙이는 것이 아닙니다. 완전히 이해할 수 없는 시스템은 정확함을 증명할 수 없는 시스템이고, 정확함을 증명할 수 없는 시스템은 예상하지 못한 방식으로 실패합니다. 단순함은 정확성과 경쟁하는 양식상의 취향이 아닙니다. 단순함은 정확성이 그것으로부터 지어지는 재료입니다. 첫 번째 없이는 두 번째를 가질 수 없습니다.

이는 대부분의 소프트웨어가 실제로 작성되는 방식을 뒤집습니다. 흔한 본능은 일단 물건을 만들고, 작동하게 한 다음, 버그가 더 이상 나타나지 않을 때까지 테스트하는 것입니다. 단순함은 시간이 남으면 나중에 추구할 사치로 취급되죠. 데이크스트라의 평생은 이 순서가 거꾸로 되어 있고 위험하다는 논증이었습니다. 그가 가장 많이 인용되는 문장은 거기서 곧장 이어지는 경고입니다. “테스트는 버그의 존재를 보여줄 뿐, 부재를 보여주지는 못한다.”² 통과한 테스트는 당신이 시도하지 않은 입력에 대해서는 아무것도 말해 주지 않습니다. 프로그램에 버그가 없다는 것을 아는 유일한 방법은 그것을 추론하는 것이며, 추론할 수 있는 것은 한 사람의 머릿속에 담길 만큼 단순한 것뿐입니다. 데이크스트라에게 우아함은 “없어도 되는 사치가 아니라 성공과 실패를 가르는 일이 잦은 요소”였습니다.³

그 신념이 그를 이 시리즈의 발원지에 놓습니다. 리누스 토르발스가 특수한 경우가 사라질 때까지 문제를 다시 빚어내고 존 카맥이 문제를 빠른 핵심까지 깎아 내는 자리에서, 데이크스트라는 두 사람이 모두 물려받은 근본 주장을 제공했습니다. 우아한 해법과 정확한 해법은 같은 해법이라는 것입니다. 이것이 취향을 기술적 체계로 다루는 – 미적 탐닉이 아니라 – 원조 논거이며, 누구도 그렇게 부르기 수십 년 전에 이미 그럴듯함보다 증명을 앞세운 논거입니다.

배경

에츠허르 비버 데이크스트라는 1930년 5월 11일 네덜란드 로테르담에서 태어나 2002년 8월 6일 뉘넌에서 세상을 떠났습니다.⁴ 그의 아버지는 화학자이자 네덜란드 화학회 회장이었고, 어머니는 수학자였습니다. 데이크스트라 본인의 말에 따르면 어머니는 수학적 논증이 언제 우아하고 언제 단지 작동하기만 하는지를 유난히 또렷이 가려내는 감각을 지녔습니다. 그는 레이던에서 수학과 이론물리학을 공부한 뒤, 1952년 암스테르담의 수학 센터에서 프로그래밍 일을 맡았습니다. “프로그래머”가 아직 인정받는 직업이 아니던 시절이었습니다. 1957년 결혼 증명서에 직업으로 그것을 등록하려 했을 때, 네덜란드 당국은 그런 직업이 공식적으로 존재하지 않는다는 이유로 받아들이지 않았다고 전해집니다. 그래서 그는 “이론물리학자”라고 적어야 했습니다.⁴

이 일화는 사소한 잡담이 아닙니다. 데이크스트라는 남은 평생 프로그래밍이 사무적인 기술이 아니라 엄밀한 지적 학문이라고 역설했고, 그 역설은 학문에 이름이 붙기도 전에 시작되었습니다. 그는 수학 센터에서 자리를 지키다가 1962년 에인트호번 공과대학교 교수가 되었고, 1970년대에는 버로스 사의 연구원으로 지냈으며, 1984년에는 오스틴 텍사스 대학교의 슐룸베르거 100주년 기념 컴퓨터과학 석좌를 맡아 1999년 은퇴할 때까지 그곳에 머물렀습니다.⁴

1972년 그는 ACM 튜링상을 받았습니다. 수상 인용문은 전문을 읽을 가치가 있는데, 어떤 요약보다도 그 원칙을 잘 짚어 내기 때문입니다. “프로그래밍을 고차원의 지적 도전으로 끌어올린 근본적 공헌에 대하여. 프로그램은 단지 디버깅을 통해 정확하게 만들어지는 것이 아니라 애초에 정확하게 작성되어야 한다는 점을 웅변적으로 역설하고 실증한 데 대하여. 프로그램 설계의 토대에 놓인 문제들을 꿰뚫어 본 통찰에 대하여.”⁵ 단지 디버깅으로 정확하게 만든 것이 아니라, 애초에 정확하게 작성된 것. 이 구절이 그 사람 전체입니다.

업적

최단 경로 알고리즘 (1956년, 1959년 발표)

1956년 데이크스트라는 새 ARMAC 컴퓨터의 공식 개관식에서 그 성능을 뽐낼 수 있는 문제를 찾으라는 요청을 받았습니다. 비전문가 청중도 따라올 수 있는 문제여야 했죠. 그는 네덜란드 64개 도시 가운데 두 도시 사이의 최단 경로를 골랐습니다. 누구나 질문을 이해하고 답을 확인할 수 있었기 때문입니다. 해법은 그가 두고두고 즐겨 이야기한 방식으로 떠올랐습니다. “어느 날 아침 젊은 약혼녀와 암스테르담에서 쇼핑을 하다가 지쳐서, 우리는 카페 테라스에 앉아 커피를 마셨습니다. 나는 그저 이걸 할 수 있을까 생각하고 있었고, 그러다 최단 경로 알고리즘을 설계했습니다.”⁶ 약 20분이 걸렸습니다.

그가 그것을 찾아낸 방법이 바로 교훈입니다. 훗날 그는 이렇게 말했습니다. “그것이 그토록 멋진 이유 중 하나는 연필과 종이 없이 설계했다는 점입니다. 나중에 깨달았는데, 연필과 종이 없이 설계하는 것의 장점 하나는 피할 수 있는 모든 복잡함을 거의 강제로 피하게 된다는 것입니다.”⁶ 그는 끄적일 메모에 기댈 수 없었기에, 아이디어가 머릿속에 온전히 담길 만큼 작아야 했습니다. 제약이 우아함을 낳았습니다. 그는 그것을 3년 동안 발표하지 않았습니다. Numerische Mathematik에 실린 1959년 논문 “그래프와 관련된 두 문제에 관한 노트”는 한 페이지를 겨우 넘기는 분량입니다. 그의 말로는, 프로그래밍이 아직 글로 쓸 만큼 점잖은 활동으로 여겨지지 않았기 때문입니다.⁶

이 알고리즘은 탐욕적입니다. 언제나 아직 방문하지 않은 가장 가까운 노드를 먼저 확장하며, 퍼져 나가는 파면이 모든 지점에 차례로 최단 거리로 도달합니다. 카페 테이블에서 설명할 수 있을 만큼 단순하고, 증명 가능하게 최적입니다 – 파면이 목표에 처음 닿는 순간, 그 경로는 결코 더 나아질 수 없습니다. 여기서 단순함과 정확함은 긴장 관계에 있지 않습니다. 둘은 같은 사실입니다.

“Go To 문은 해롭다고 여겨진다”와 구조적 프로그래밍 (1968년)

1968년 데이크스트라는 “goto 문에 반대하는 변론”이라는 제목으로 Communications of the ACM에 편지를 보냈습니다. 편집자였던 니클라우스 비르트는 이를 “Go To 문은 해롭다고 여겨진다”로 바꾸었는데, 이 표현은 모방작의 한 장르를 통째로 낳았고 지금은 편지 본문의 그 어떤 내용보다 유명합니다.⁷ 데이크스트라의 논증은 스타일 가이드가 아니었습니다. 인식론적인 것이었습니다. 제약 없는 goto는 제어가 어디로든 건너뛰게 만들고, 그러면 어떤 줄에서 프로그램이 무엇을 하고 있는지 이해하려면 그 지점에 이를 수 있었던 모든 경로를 추적해야 할 수도 있습니다. 프로그램 텍스트와 프로그램의 동작이 따로 놀게 되는 것입니다. 순차, 선택, 반복이라는 구조적 제어가 있으면 텍스트와 실행이 서로 대응을 유지하고, 한 블록을 읽는 것만으로 그 블록을 추론할 수 있습니다.

이 논증은 최단 경로 설계의 제약과 같은 원칙을, 언어 설계에 적용한 것입니다. 추론할 수 있을 만큼 작게 유지하라는 것이죠. 구조적 프로그래밍은 키워드 하나를 금지하는 일이 아니었습니다. 읽는 것만으로 프로그램이 정확하다는 것을 증명할 수 있는 인간의 능력을 지켜 내는 일이었습니다. 튜링상 인용문이 그의 어휘를 줄줄이 호명한 것 – “치명적 포옹(deadly embrace)”, “세마포어(semaphore)”, “goto 없는 프로그래밍”, “구조적 프로그래밍” – 은 그가 프로그래머들이 사고하는 언어를 얼마나 철저히 다시 빚어냈는지를 보여주는 기록입니다.⁵

그의 운영체제 작업도 같은 DNA를 지녔습니다. THE 멀티프로그래밍 시스템(1968년)은 엄격하게 계층화된 추상화 단계들로 지어졌고, 각 단계는 그 자체로 검증 가능했습니다. 동시에 실행되는 프로세스들을 조율하기 위해 그는 세마포어와 그 P 연산, V 연산을 발명했고, 교착 상태와 기아 상태를 가르치기 위한 정수로서 식사하는 철학자들 문제를 정식화했습니다 – 어려운 동시성 문제를 머릿속에 담길 만큼 작게 만든 것이죠.⁴⁵ 그 뒤로는 자기 안정화가 나왔고, 프로그래밍의 규율(1976년)에서는 술어 변환기(predicate transformer) / 최약 전제 조건(weakest-precondition) 계산법이 등장했습니다. 이는 코드를 작성한 다음 나중에 검증되기를 바라는 대신, 프로그램과 그 정확성 증명을 손에 손을 잡고 함께 도출하는 방법이었습니다.⁴⁵

겸손한 프로그래머: 테스트보다 증명 (1972년)

데이크스트라의 튜링상 수상 강연 “겸손한 프로그래머”(EWD340)는 왜 단순함이 단지 실용적인 문제가 아니라 도덕적인 문제인지에 대한 가장 명료한 진술입니다. 그 중심 주장은 인간 정신의 크기에 관한 것입니다. “유능한 프로그래머는 자기 두개골의 크기가 엄격하게 제한되어 있다는 사실을 충분히 자각하고 있다. 그래서 그는 온전한 겸손으로 프로그래밍 과제에 임하며, 무엇보다도 영리한 잔재주를 전염병처럼 피한다.”⁸ 영리함은 미덕이 아닙니다. 자기 머릿속에 담을 수 있는 것보다 더 많이 담을 수 있다는 내기이고, 그 내기는 운영 환경에서, 당신에게 불리하게 판가름 납니다.

이 강연은 정확하게 구성된 소프트웨어의 창립 헌장처럼 읽히는 처방으로 마무리됩니다. “우리는 훨씬 더 나은 프로그래밍을 해낼 것이다. 다만 이 과제의 엄청난 어려움을 온전히 인정하며 임할 때, 겸손하고 우아한 프로그래밍 언어를 고수할 때, 인간 정신의 본질적 한계를 존중하며 매우 겸손한 프로그래머로서 과제에 임할 때 그러하다.”⁸ 이 틀에서 테스트는 근본적으로 불충분합니다 – 테스트가 쓸모없어서가 아니라, 테스트가 입력 공간을 표본으로 추출하는 것 이상을 결코 할 수 없기 때문입니다. “구조적 프로그래밍에 관한 노트”에 나오는, 더 길고 정본에 가까운 형태의 경고는 모호함이 없습니다. “프로그램 테스트는 버그의 존재를 보여주는 데 쓸 수 있지만, 결코 그 부재를 보여주는 데는 쓸 수 없다!”⁹ 버그의 부재를 원한다면 그것을 증명해야 하고, 증명할 수 있는 것은 이해할 수 있는 것뿐입니다.

실천으로서의 EWD 원고 (1960년대–2002년)

약 40년 동안 데이크스트라는 번호를 매긴 일련의 원고 – 메모, 증명, 출장 보고서, 에세이, 논증 – 를 자기 이니셜 “EWD”를 앞에 붙여 썼습니다. 이 시리즈는 EWD1318까지 이어지며 실제 문서는 천 편이 넘습니다. 번호가 문서 수를 웃도는 이유는, 그가 한 편을 시작할 때 번호를 부여했고 모든 편이 완성되지는 않았기 때문입니다.⁴¹⁰ 대부분은 그 유명한 정밀한 필체로, 만년필을 들고 손수 작성되었습니다. 그는 컴퓨터로 초안을 쓰지 않았습니다. 원고를 한 편 쓰고, 복사한 다음, 소수의 동료 무리에게 우편으로 보냈으며, 그들은 다시 복사해 다른 사람에게 전달했습니다 – 거의 어떤 것도 정식으로 발표되지 않았다는 사실에 비하면 지나칠 만큼 큰 영향력을 EWD에 안겨 준, 인터넷 이전 시대의 사미즈다트였습니다.⁴¹⁰ 전체 시리즈는 이제 스캔되어 오스틴 텍사스 대학교의 E.W. 데이크스트라 아카이브에서 자유롭게 열람할 수 있습니다.¹⁰

이 실천은 철학과 떼어 놓을 수 없었습니다. 되돌리기 없이 천천히 손으로 쓰는 일은 연필과 종이 없이 설계하는 것과 같은 규율을 강제합니다. 분량 뒤에도, 수정 뒤에도 숨을 수 없습니다. 논증은 성립하거나 성립하지 않거나 둘 중 하나이며, 당신은 그것을 잉크로 못 박아야 합니다. EWD는 한 엔지니어가 글쓰기 자체를 명료하게 사고하기 위한 도구로 다루고, 명료함을 전부로 삼을 때 어떤 모습이 되는지를 보여줍니다.

방법

그 방법은 40년에 걸쳐 집요하게 적용된 하나의 신념입니다.

추론할 수 있을 만큼 작게 만들어라. 카페의 알고리즘, 구조적 제어 흐름, 계층화된 THE 시스템, 식사하는 철학자들이라는 정수 – 각각은 인간 정신이 문제 전체를 담아 확인할 수 있을 때까지 문제를 줄이는 행위입니다. 한눈에 살펴볼 수 없는 복잡함은 신뢰할 수 없는 복잡함입니다.

증명하라, 테스트하지 말고. 테스트는 표본을 추출하고, 증명은 보증합니다. 데이크스트라의 술어 변환기 계산법은 증명과 프로그램이 함께 도출되도록 존재하지, 하나를 작성하고 다른 하나를 나중에 덧붙이도록 존재하지 않습니다. “단지 디버깅으로 정확하게 만든 것이 아니라, 애초에 정확하게 작성된 것”이 다섯 단어로 압축된 방법입니다.⁵

우아함을 장식이 아니라 증거로 다루어라. 해법이 추할 때, 그 추함은 대개 문제가 아직 이해되지 않았다는 신호입니다. 우아함이 “성공과 실패를 가르는” 이유는, 우아한 형태가 곧 틀릴 수 있는 자리가 가장 적은 형태이기 때문입니다.³

생각하기 위해 써라. EWD는 작업이 끝난 뒤에 만들어진 문서가 아니었습니다. EWD가 곧 작업이었습니다 – 어물쩍 넘어가기를 용납하지 않는 매체 위에, 추론을 눈에 보이게 드러낸 것이었죠. 연필과 종이 없이 설계한 다음 그 결과를 만년필로 못 박는 것은, 같은 규율을 두 번 적용하는 일입니다.

영향의 사슬

그를 빚어낸 이들

수학자였던 그의 어머니. 데이크스트라는 수학적 우아함에 대한 자신의 감각을 어머니의 공으로 돌렸습니다 – 증명이 단지 타당한 것을 넘어 깔끔할 때를 알아채는, 훈련된 직관 말입니다. 작동하는 논증과 아름다운 논증 사이의 그 구분이 그의 평생을 관통하는 축이 되었습니다. (형성적 영향)

Algol 60 작업. 데이크스트라는 최초의 Algol 60 컴파일러 중 하나를 공동 제작했고, 그 언어의 블록 구조와 재귀는 구조적 프로그래밍의 원재료가 되었습니다. Algol은 프로그래밍 언어가 편의를 위해 덧붙여지는 대신 명료함을 위해 설계될 수 있다는 증거였습니다. (직접적 영향)

증명이라는 수학적 전통. “컴퓨터 과학”이 존재하기 전에 수학자이자 물리학자로 훈련받은 데이크스트라는 증명의 기준을 통째로 들여왔습니다. 그에게 프로그램은 수학적 대상이었고, 질문은 결코 “이게 작동하는 것 같은가?”가 아니라 “반드시 작동한다는 것을 입증할 수 있는가?”였습니다. (형성적 영향)

그가 빚어낸 것들

구조적 코드를 작성하는 모든 프로그래머. 일상적인 프로그래밍에서 goto가 사라진 것, 순차/선택/반복의 보편성, 그리고 동시성의 어휘 전체 – 세마포어, 교착 상태, 상호 배제 – 는 그 이후 작성된 모든 코드베이스에서 보이지 않게 작동하는 그의 유산입니다.

형식적 방법과 프로그램 검증. 술어 변환기 계산법과 “애초에 정확하게 작성한다”는 이상은 현대의 검증, 모델 검사, 증명 동반 코드의 직계 조상입니다. 형식적으로 검증된 시스템 소프트웨어의 현재 부흥은, 그것을 실행할 만큼 빨라진 하드웨어를 마침내 만난 데이크스트라의 논증입니다.

학문이 스스로를 보는 자화상. 어떤 특정한 산물보다도, 데이크스트라는 프로그래밍이 시행착오로 배우는 기능공의 일이 아니라 엄밀함을 마땅히 갖추어야 할 응용 수학의 한 분야라는 생각을 확립했습니다. 좋든 나쁘든, 이 분야의 양심은 여전히 그의 어조로 말합니다.

관통하는 줄기

데이크스트라는 이 시리즈의 나머지가 흘러나오는 원천입니다. 리누스 토르발스의 “좋은 취향” – 특수한 경우가 사라지는 그 재작성 – 은 커널 해커의 어법으로 표현된 데이크스트라의 단순함-곧-정확성입니다. 분기가 적을수록 틀릴 자리도 적다는 것이죠. 존 카맥의 빠르고 단순한 핵심은, 증명 대신 하드웨어의 한계 천장을 겨눈 똑같은 뺄셈입니다. 그리고 안드레이 카파시가 시스템을 진정으로 이해하기 위해 처음부터 다시 만들겠다고 고집하는 것은, 딥러닝의 모자를 쓴 데이크스트라의 “연필과 종이 없이 설계하기”입니다. 이 네 사람은 거의 모든 것에서 의견이 갈리지만, 정작 중요한 한 가지에서는 일치합니다. 우아한 구조는 정확한 해법 위에 덧입혀지는 것이 아닙니다. 우아한 구조가 곧 정확한 해법입니다. (시리즈 연결)

내가 여기서 얻는 것

내가 거듭 돌아가는 문장은 그 뒤집음입니다. 단순함은 신뢰성을 달성한 뒤에 받는 보상이 아니라, 신뢰성의 전제 조건이라는 것. 느리고 깨지기 쉬운 소프트웨어 대부분은 누군가 테스트를 건너뛰어서 느리고 깨지기 쉬운 것이 아닙니다. 누구도 그것을 이해할 만큼 작게 만든 적이 없어서, 그래서 누구도 그것을 추론할 수 없었고, 그래서 유일하게 쓸 수 있는 품질 전략이 보이는 버그가 멈출 때까지 테스트하는 것뿐이었기 때문에 느리고 깨지기 쉬운 것입니다 – 그리고 데이크스트라가 말했듯, 그것은 아무것도 보증하지 못합니다. 이 뒤집음은 품질이 유일한 변수라는 것과 같은 기준입니다. 질문은 결코 “테스트가 통과했는가?”가 아니라 “이것이 정확하다는 것을 알 만큼 충분히 이해하고 있는가?”입니다.

내가 지금 무언가를 만드는 세계에서는 – AI 에이전트, 도구 루프, 어떤 사람이 읽을 수 있는 것보다 빠르게 코드를 생성하는 시스템 – 데이크스트라의 경고가 그 어느 때보다 날카롭습니다. 에이전트가 천 줄을 작성하고 테스트가 초록빛일 때, 그것은 바로 그가 묘사한 상황입니다. 버그의 존재는 입증되지 않았고, 그 부재는 입증될 수 없습니다. 데이크스트라식 수는, 생성이 규모를 키우는 만큼 이해가 규모를 줄이는 일을 거부하는 것입니다 – 누군가 여전히 그것이 옳다고 증명할 수 있도록, 시스템을 충분히 작고, 충분히 계층적이고, 충분히 읽을 수 있게 유지하라고 고집하는 것입니다. 어떤 사람도 코드를 읽지 않을 때조차 내가 검증 계층을 하중을 떠받치는 구조로 다루는 이유가 바로 이것입니다. 테스트는 존재를 보여줄 뿐 부재를 보여주지 못하며, 초록색 체크 표시의 파면은 증명이 아닙니다.

자주 묻는 질문

에츠허르 데이크스트라의 엔지니어링 철학은 무엇인가요?

데이크스트라는 단순함이 신뢰성의 전제 조건이라고 보았습니다. 프로그램은 인간이 완전히 이해할 수 있을 만큼 단순해야 하는데, 이해 가능한 프로그램만이 추론될 수 있고 정확함을 증명받을 수 있기 때문입니다. 그는 프로그램이 “단지 디버깅으로 정확하게 만들어지는 것이 아니라 애초에 정확하게 작성되어야 한다”고, 테스트는 버그의 존재를 보여줄 수 있지만 결코 그 부재를 보여주지는 못한다고, 그리고 우아함은 장식이 아니라 “성공과 실패를 가르는 일이 잦은 요소”라고 주장했습니다. 그가 보기에 영리함은 악덕이었습니다. 인간 정신의 제한된 용량을 넘어서기 때문입니다.³⁵⁸⁹

에츠허르 데이크스트라는 무엇을 발명했나요?

데이크스트라는 자기 이름이 붙은 최단 경로 알고리즘을 발명했고(1956년 착상, 1959년 발표), 동시 실행 프로세스를 조율하기 위한 세마포어와 P/V 연산을 도입했으며, 계층화된 THE 멀티프로그래밍 시스템을 구축했고, 식사하는 철학자들 문제를 정식화했으며, 구조적 프로그래밍을 발전시켰고, 분산 시스템에서 자기 안정화 개념을 창안했으며, 프로그램과 그 정확성 증명을 함께 도출하기 위한 술어 변환기 / 최약 전제 조건 계산법을 개발했습니다(프로그래밍의 규율, 1976년). 그는 1972년 ACM 튜링상을 받았습니다.⁴⁵

“테스트는 버그의 존재를 보여줄 뿐, 부재를 보여주지 못한다”는 무슨 뜻인가요?

테스트는 버그를 발동시킴으로써 그것이 존재한다는 것만 입증할 수 있을 뿐, 버그가 없다는 것은 결코 입증할 수 없다는 뜻입니다. 유한한 테스트 집합으로는 가능한 모든 입력을 다 덮을 수 없기 때문입니다. 데이크스트라는 1969년 NATO 소프트웨어 공학 회의에서 이를 언급했고, “구조적 프로그래밍에 관한 노트”에서 정본에 가까운 더 긴 형태를 제시했습니다. “프로그램 테스트는 버그의 존재를 보여주는 데 쓸 수 있지만, 결코 그 부재를 보여주는 데는 쓸 수 없다!” 그의 결론은, 정확성에 대한 확신은 통과한 테스트를 쌓는 데서가 아니라 증명에서, 그리고 추론할 수 있을 만큼 단순하게 프로그램을 설계하는 데서 나와야 한다는 것이었습니다.²⁹

데이크스트라는 왜 손으로 글을 쓰고 EWD 원고를 복사본으로 회람했나요?

EWD는 데이크스트라가 약 40년에 걸쳐 쓴, 번호가 매겨진 천 편이 넘는 원고 시리즈였습니다. 대부분 만년필로 손수 쓴 다음 복사해서 소수의 무리에게 우편으로 보냈고, 그들이 다시 복사해 전달했습니다. 되돌리기 키 없이 손으로 천천히 쓰는 일은, 연필과 종이 없이 알고리즘을 설계하던 그의 습관과 같은 규율을 강제했습니다. 명료함을 강제하고 어물쩍 넘어가기를 용납하지 않았던 것이죠. 잉크로 못 박은 논증은 실제로 성립해야 했기 때문입니다. 전체 시리즈는 오스틴 텍사스 대학교에 보관되어 자유롭게 열람할 수 있습니다.⁶¹⁰

출처