[서문] 제임스 H. 페처 (James H. Fetzer)의 ACM 투고를 둘러싸고 벌어진 일련의 논쟁

다음 글은 Toyota Technological Institute at Chicago에서 박사 과정을 밟고 있으며, 소프트웨어 컨플릭트 2.0의 핵심 베타리더를 맡았던 채원석(http://people.cs.uchicago.edu/~wchae/) 박사님께서 투고한 내용입니다. 원래 공동 작업 위키에 올라왔던 글인데, 혼자만 읽기가 너무 아까워서 독자 여러분을 위해 소프트웨어 컨플릭트 2.0 1번 타자로 블로그에 소개합니다. 내용이 조금 어렵긴 하지만 조금만 발톱을 내서 읽어보시면 당시 전투(?) 상황을 한눈에 파악할 수 있을 겁니다.

제임스 H. 페처 (James H. Fetzer)의 ACM 투고를 둘러싸고 벌어진 일련의 논쟁

(사진은 음모이론 전문가인 제임스 H. 페처 교수)

1판 서문에서 논쟁이 격해져서 상대를 인격적으로 비난하는 사태까지 야기시켰다고 예로 들어진 이 일을 어찌 그냥 지나칠 수 있겠습니까? 과연 무슨 일이 있었는지 살펴 봅시다.

프롤로그: 1979년

Algol 개발의 공로로 제 1회 (1966년) 튜링상을 수상한 알란 J. 퍼리스 (Alan J. Perlis)를 포함한 일련의 수학자(혹은 초기 컴퓨터 과학자)들은 1979년 ACM 기고(1)를 통해서 수학에서의 이론 증명과 전산학에서의 프로그램 검증은 본질적으로 다르기 때문에 장래에 정형적 검증 분야는 큰 역할을 못 할 것이라고 예측합니다.

수학 증명에서의 실수는 정형적 기법을 통해서 밝혀지는 것이 아니라 동료 수학자들의 검토과정을 통해서 들어나게 내고, 이런 과정을 통해서 살아남은 증명만이 심증적으로 사실이라고 여겨지게 되고, 다른 접근 방법을 통해서 반복적으로 이 이론이 사실이라고 증명되어 질때서야 비로서 이론이 사실로서 받아 들여지고 이런 과정에서 개발된 증명기법들이 정리되어 다른 이론의 증명에 응용되는데 반해서, 프로그램 분야에서는 이런 과정이 있기 어렵다는 것이 이 논문의 요지입니다.

더 나아가 프로그램 검증의 확장성 문제에 대해서 "Babysitting for a sleeping child for one hour does not scale up to raising a familiy of ten"라는 조롱을 겯들여 공격하며 실용성이 없다고 반박합니다.

결론으로 1) 수학자들처럼 같이 검토하는 방식을 취해야 하며 2) 프로그램 검증이 "perfect"한 소프트웨어를 확인(verify)하는 과정이 아니라 소프트웨어의 (현실적 의미에서의) "reliable"함을 확인하는 과정으로 이해되어야 한다고 말합니다.

1988년 가을: 시작

ACM은 철학자인 제임스 H. 페처의 "Programming Verification: The Very Idea"(2)라는 글을 실으면서 "프로그래밍 검증은 이론으로조차도 불가능하다"는 큼직만한 머리말을 답니다.이 논문의 전반적인 내용은 79년의 논문(1)을 재고찰하여 모순점을 지적하면서도 결국은 유사한 결론인 프로그램 검증에 대한 강한 부정을 표현하고 있습니다.

철학자답게 언어에 대한 정의를 내리면서 논제를 발전시키고 있는데, "검증가능하다"는 말을 어떤 경우에도 검증가능한 "절대적 검증가능"(이 경우엔 기본 명제가 존재해서 그 명제를 통해서 현재 프로그램이 검증하다는 결과를 낼 수 있어야하고)과 어떤 상황이 만족해야만 검증가능한 "상대적 검증가능"(이 경우엔 결론을 이끌어 낼 수있는 가정이 있어야함)으로 분류하고 "기본 명제"가 없거나 "가정"이 틀리다면 "검증가능하다"는 개념자체가 잘 못 된것이 아니냐는 주장을 펼칩니다.

그 주장에 기반하여 알고리즘은 검증가능하지만 이를 구현한 프로그램은 실제 반도체 덩어리인 기계 위에서 돌아가기 때문에 이 기계가 완벽히 동작한다는 가정이 필요한데 누가 그것을 확신할 수 있게는가, 따라서 그 가정에 기반한 검증은 의미가 없다(!)고 결론내립니다. 또한, (1)에서 주장하는 것처럼 같이 협동해서 이 난제를 극복해나간다는 것도 의미가 없는데 그것은 소프트웨어 시스템이 너무 복잡하기 때문이랍니다.

1989년 봄: The Gang of Ten

89년 3월호에 페처에 의해서 The Gang of Ten이라고 불리게 되는 열명의 학자들이 공동으로 보낸 편지(3)가 공개됩니다. 이 편지는 페처의 논문이 "검증에 대한 심각한 연구가 아니였다"고 포문을 열면서 페처는 프로그램 검증의 목적을 "절대적으로 검증"하는 것으로 오해하고 있고, 어떻게 논문의 참고문헌에 프로그램 검증에 관한 논문이 하나도 없을 수 있으며, 이 분야에 문외한으로 밖에 생각할 수가 없다고 반박하고 더나아가 이런 잘못된 내용이 포함된 논문을 어떻게 게재할 수 있었는지 편집자에게 그 책임을 묻고 있습니다.

이에 대한 대꾸로 페처는 자기가 주장한 것은 "프로그램 검증이 완벽하다는 환상을 깨자"는 것이었다고 말하면서 자기가 말한 소프트웨어 시스템은 "크루즈 미사일 항법 시스템"인데 자신있으면 미사일과 같이 날아가면서 검증해보라고 맞서며 소프트웨어 컨플릭트 2.0에도 언급되었던 "참기 어려울 만큼 잘난 체하며..종교적인 광신자와 이상 숭배자"라고 응수합니다.

또한, 발등에 불이 떨어진 편집장(4)도 이 논문이 실리게 된 배경을 간단히 언급하는데, 이 논문이 기술적이라기보다는 철학적 고찰이 담겨있어서 기술담당자가 아닌 인문학담장자에게 이 논문을 맡겼고 잘 알려진 컴퓨터 학자로 부터 자문도 받았다고 말하면서 논문 검토과정에는 전혀 문제가 없었음을 강조하며 이제 프로그램 검증에 대해 진지하게 토론해보자고 제안합니다.

The Gang of Ten외에도 많이 사람들이 공격적인 질문을 던졌는데 이에 대한 내용은 같은 3월호(5)에 실려있습니다. 주요 내용은

• 실제 컴퓨터에서 동작하는 프로그램의 검증을 신뢰할 수 없다는 당연한 내용을 확대해석했다.
• 페처의 주장은 프로그램의 검증이 완벽하지 않기때문에 무의미하다는 것인데, 그는 이런 검증기술이 (실제 프로그램이 아닌) 설계 단계에서의 오류를 잡아준다는 사실을 간과하고 있다.
• 페처는 프로그램 검증 기술의 수준과 목적을 오해하고 있다.

이에 대해 페처 역시 답변(5)을 합니다만 논문의 내용을 크게 벗어나지는 않습니다.

1989년 4월: 분석

ACM의 편집장은 쇄도하는 부정적인 편지에 놀라 두명의 학자에게 이 사태를 분석하도록 합니다. 분석기고(6)에서 두 사람은 페처의 논문을 "프로그램 검증의 이론적 한계에 대한 독특하며 흥미로운 글이었다"고 시작하면서 자신들도 수많은 부정적인 분위기에 놀라서 다시 논문을 읽어야 했다고 말합니다. 그들은 이런 논쟁의 일정부분은 페처의 논문을 읽는 비전문가들, 특별히 연구자금에 관련된 비전문가들이 페처의 논문을 통해서 잘못된 생각을 갖게될 것에 대한 학자들의 두려움에서 기인한다고 봤습니다. 하지만 가장 큰 문제는 프로그램 검증 연구가들과 페처와의 시각차에서 기인한다고 결론을 내립니다. 그들이 보기에 페처는 검증연구가들이 프로그램의 정확성(correctness or why-it-is-so)를 검증해왔다고 주장하는 것으로 생각하는 반면에, 검증연구가들은 꾸준히 자신들은 증거(evidential reason or why-we-hold-it-to-be-so)를 제시해 오고 있다고 설명하며 이같은 시각의 차가 그들간의 돌이킬 수 없는 논쟁을 낳았다고 설명합니다. 즉, 과대광고된 검증 연구 결과를 페처가 공격했고, 공격을 받은 검증 연구가들은 그것은 자신들이 하는 일(혹은 할 수 있다고 말했던 일)이 아니라고 억울해 한다는 의미죠. 결론은 페처는 좀더 정확한 조사가 필요했으며 검증 연구가들은 자신들의 한계에 대해서 좀더 분명히 언급할 필요성이 있었다라는 것입니다.

1989년 4월계속: 계속되는 논쟁

위의 분석기사와 같은 4월호 ACM에 또다른 독자편지들과 페처의 반응(7)이 실립니다.

• 프로그램의 일정 부분만을 검증하는 것도 의미가 있다는 반응
• 실제 컴퓨터는 검증이 불가능하다는 페처의 주장에 "기차 신호기"를 예로 들면서 하드웨어라고 검증이 불가능한 것은 아니라는 주장
• 물리적 현상에서는 정확하다 틀리다는 관측의 결과만이 중요하지만, 소프트웨어에서는 수정이라는 특별한 작업이 있는데 이를 페처는 언급하지 않았다는 반박

1989년 7월: 호의적인 편지들

7월호 ACM에는 편집자의 배려(?)인지 페처의 글에 호의적인 편지들(8)도 소개가 되기 시작합니다. 한 편지는 ACM의 목적중의 하나는 잘 정리된 논쟁을 장려하는 것이라면서 편집자들의 결정을 지지합니다.

하지만, "No matter how perfect your cookie recipe is, if the oven thermostat fails, you may burn the cookies"라며 페처의 호들갑을 나무라는 편지도 빠지지 않았습니다. 또한, 이 모든 논쟁의 시작은 용어 선택의 잘못에서 기인한다는 지적도 있습니다. 컴퓨터 학자들 사이에서는 프로그램 검증이 "상대적인 보장" 정도로 이해되는 와중에 외부의 학자(페처를 말합니다)가 검증이라는 말을 글자 그대로 해석하고서는 그건 불가능하지요라고 떠들었다는 입장입니다. 이에 대해서 페처는 컴퓨터 학자들에게 그들만의 가상세계에서 나와 실제세상에서 무엇을 할 지를 걱정하라고 조언합니다. 어차피 완벽한 검증이 안되니 다른 수라도 찾아야 할 것이 아니냐는 것이죠.

1989년 8월: 또 다른 시작

8월호 ACM에는 4월호에 실린 분석기사에 대해서 페처(!)가 저자들이 자신의 논지를 잘못 이해하고 있다고 반박 편지(9)를 보냅니다. 자신의 주장은 "프로그램 검증기가 쏟아내는 것들은 불완전할 수 밖에 없다"는 것이라고 못을 박으면서 다시한번 "프로그래밍 검증은 이론으로조차도 불가능하다"를 되뇌입니다.

그끝은?

이후로도 또 얼마간 독자편지가 오고 갔겠죠. 암튼, 이 사건을 페처가 정리한 글이 (10)입니다만 역시 페처의 글은 읽기가 쉽지 않습니다. 인터넷 여기저기에 이 사건에 관련되어서 글들(예로 11)이 보입니다만 이 정도에서 끝을 내야겠군요.

에필로그: 2006년

지난 1월에 있었던 POPL (Principle on Programming Languages 12)에서 컴파일러를 검증하는 기술이 발표되었습니다. 컴파일러가 잘못된 프로그램을 생성할 경우를 상상해 보셨나요? 비행기에 들어갈 소프트웨어를 위한 C 컴파일러에 적용된 이 기술은 컴파일러가 잘못된 코드를 생성하지 못하도록 하는 방법에 대한 것이었습니다.

지난 6월에 있었던 ICFP(International Conference on Functional Programmgin 13)에서는 반도체의 결함에도 불구하고 제대로 동작할 수 있는 소프트웨어를 생성하는 컴파일러에 대한 논문이 있었지요. 이제 시작단계이지만, 페처의 중요한 논지였던 물리적 컴퓨터의 불완전성을 극복해보려는 첫 시도로 여겨집니다.

또한 요새 유행하는 프로그래밍 언어 연구의 큰 주제 중의 하나는 자동화된 검증 기법입니다. 현재의 수준은 100만점에 30점 정도의 수준이라고 합니다. 예를 들면, (하드웨어에 결함이 없다는 가정하에) 우리가 작성하는 코드가 실행될 때 core dump를 내지 않으리라고 보장할 수 있다는 것이죠.

지난 20세기에는 상상도 하지 못할 정도의 프로그래밍 기술과 정형 검증 기법들이 쏟아져 오고 있는 지금도 페처의 주장은 유효할까요? 아니면 앞으로도 계속 유효할까요? 지금은 음모이론가가 되어 JFK를 쫒는 페처를 보면서 제가 지금하고 있는 일이 페처가 그리도 안된다고 했던 일이 아닐지 걱정이 됩니다. ^_^ ws

• www - http://www.d.umn.edu/~jfetzer/
• 관련 자료 - 위키피디아 http://en.wikipedia.org/wiki/James_H._Fetzer
• 참고문헌
  1. Richard A. De Millo, Richard J. Lipton and Alan J. Perlis, Social Processes and Proofs of Theorems and Programs, Communications of the ACM (May 1979), pp. 271-280
  2. James H. Fetzer, Program Verification: The Very Idea, Communications of the ACM (September 1988), pp. 1048-1063.
  3. ACM Forum: Editoral Process Verification , Communications of the ACM (March 1989), pp. 287-289.
  4. ACM Forum: Reply from the Editor in Chief, Communications of the ACM (March 1989), pp. 289-290.
  5. Technical Correspondence: The Author's Response, Communications of the ACM (March 1989), pp. 374-381.
  6. Viewpoint: Program Verification:Public Image and Private Reality, Communications of the ACM (April 1989), pp. 420-422.
  7. Technical Correspondence: The Author's Response, Communications of the ACM (April 1989), pp. 510-512.
  8. ACM Forum: More on Verification, Communications of the ACM (July 1989), pp. 790-792.
  9. ACM Forum: Another Point of View, Communications of the ACM (August 1989), pp. 920-921.
  10. James H. Fetzer, Philosophical Aspects of Program Verification, Minds and Machines (May 1991), pp. 197-216.
  11. Can Programs Be Verified? http://www.cse.buffalo.edu/~rapaport/510/canprogsbeverified.html
  12. POPL'06 http://www.cs.princeton.edu/~dpw/popl/06/
  13. ICFP'06 http://icfp06.cs.uchicago.edu/