수학에서 증명, 지식, 이해, 믿음이 어떻게 상보적으로 작동하는지 비유를 통해 살피고, 프로그래밍에서의 Curry–Howard 대응과 ‘증명으로서의 프로그램’이 초래하는 함정을 논한다.
2017년에 ZuriHac에서 하스켈 교육에 관한 발표를 했습니다. 그때 제목을 “이해를 위한 하스켈 가르치기(Teaching Haskell for Understanding)”라고 붙였던 것 같은데, 사실은 “믿음을 위한 하스켈 가르치기(Teaching Haskell for Belief)”라고 했어야 했는지도 모르겠습니다. 다만 그랬다면 여기서 논의할 이유들로 인해 널리 오해를 샀을 것이고, 교사로서 목표로 삼기엔 너무 야심 찬 구호였을 겁니다.
그 발표의 한 부분은 제가 말한 _이해(understanding)_가 무엇을 뜻하는지에 초점을 맞췄고, 여기서는 그 부분을 다시 요약하고 조금 더 확장해 보려 합니다. “지식, 이해, 믿음”이라는 특정한 용어 선택은 유제니아 청(Eugenia Cheng)의 훌륭한 책 ‘How to Bake π’에서 빌려온 것입니다. 청은 특히 수학적 소통에서 _증명_이 맡는 역할에 관심을 갖지만, 여기서의 제 관심사는 약간 다릅니다. 다만 명료함을 위해 그녀의 설명에서 출발하는 것이 좋을 듯하니, 거기서부터 시작하겠습니다.
숲 가장자리에 가이드와 함께 있다고 상상해 보세요. 가이드는 당신을 숲 건너편까지 이끌어 주겠다고 말합니다. 그녀는 이 숲을 예전에 지나가 본 적이 있어서 그렇게 할 수 있다고도 말합니다. 그녀는 당신을 한 걸음 한 걸음 이끌어 주지만, 여행 전체에 대한 조망이나, 당신 혼자서 길을 찾을 수 있게 해 줄 이정표나 랜드마크 같은 건 전혀 주지 않습니다(그녀가 중간에 당신을 버리고 가더라도, 스스로 반대편으로 가거나 되돌아갈 수 있을 만큼의 정보는 없습니다).
당신은 몇 가지를 안다(know): 지금 숲속에 있다는 것, (적어도 현재로서는) 가이드가 함께 있다는 것, 그리고 당신이 스스로 볼 수 있는 현재 위치에 대한 상세한 정보들.
또한 당신은 몇 가지를 믿는다(believe): 가이드는 지식이 있다(그녀가 그렇게 말했다!), 그리고 그녀는 당신을 반대편으로 이끌 의도이며 실제로 그렇게 할 것이다(빙빙 돌리거나 생강 과자 집으로 데려가 당신을 잡아먹으려는 것이 아니라), 숲에는 끝이 있다(즉, 도달해야 할 “다른 쪽”이 있다). 이런 것들을 믿을 만한 충분한 이유가 있을 수도 있고, 단지 그녀의 말을 곧이곧대로 받아들이는 것일 수도 있습니다. 숲에는 끝이 있고 “반대편”이 있다는 믿음은, 지구상에는 끝나지 않는 숲이 없다는 당신의 경험과 지식에서 나온 추정입니다.
하지만 여행 전체의 조망, 혹은 지도, 혹은 랜드마크를 알아볼 수 있는 능력이 없다면, 당신에게는 결정적으로 _이해_가 결여되어 있습니다. 가이드가 매번 다음 발을 어디에 디뎌야 하는지 알려 주지 않는다면, 당신은 숲의 반대편으로 가거나 출발점으로 돌아갈 수 없습니다.
실제로 이러한 이해의 결여는 당신의 믿음을 갉아먹을 수도 있습니다. 체력보다 더 오래 걷게 된 적이 있다면, 진짜로 이 산책은 끝나지 않을 것이고, 당신은 여기서 죽을 거라는 느낌을 알지도 모릅니다. 하지만 전체 경로가 그려진 지도가 손에 있었다면, 사실 지금 바로 끝에서 몇 미터밖에 떨어져 있지 않다는 것을 볼 수 있었을 겁니다. 당신의 어떤 부분은 분명 글자 그대로 죽지는 않으리라 알고 있었지만… 그런데도 이 길에 당신의 몸이 굴복할 것이라는 느낌, 즉 _도저히 끝까지 못 갈 것_이라는 느낌이 점점 더 설득력을 얻어, 숲에는 항상 끝이 있다는 믿음과 가이드의 선의와 능력에 대한 믿음을 압도해 버릴 수 있습니다. 저도 하이킹 중에 지구 자체가 제게 등을 돌린 것 같은 순간이 있었고, 적어도 그 순간만큼은 진심으로 그렇게 확신했습니다.
만약 전체 여정의 지도를 볼 수 있었다면, 지금 거의 다 왔다는 사실을 보고 그런 의심을 하지 않았을 겁니다. 그래서 _이해_는 지식과 믿음 사이를 매개하는 데 결정적인 역할을 합니다.
사실, 우리가 알고 믿기는 하지만 제대로 이해하지는 못하는 것들도 있습니다. 많은 사람들은 물이 얼면 팽창한다는 것을 알고 믿지만, 왜 그런지는 이해하지 못합니다. 많은 사람들은 식물이 “광합성”이라는 것을 한다는 것을 믿고(과학 시간에 배운) 몇 가지 사실(식물은 이산화탄소를 흡수하고 산소를 배출한다 — 멋지죠!)을 알지만, 그 모든 과정이 어떻게 작동하는지는 이해하지 못합니다. 대부분의 영어 화자들은 “colorless green ideas sleep furiously”가 좋은 영어가 아니라고 믿는 동시에 문법적으로는 맞다는 것을 알지만, 그런 문장이 주는 불편한 느낌에 대해 그것 이상의 설명을 이해하는 사람은 드뭅니다.
청에게서, 증명은 당신이 그 의도와 지식을 완전히 믿을 수 있는 가이드와 같습니다. 그녀는 당신을 숲을 통해 한 걸음씩 이끌지만, 그 과정의 고수준 개요는 제공하지 않습니다. 증명의 각 전제는 가이드가 숲에서 내게 하는 각 걸음과 같습니다. 각 걸음에 대해 읽을 수 있는(납득할 수 있는) 것들이 있고, 그 모든 걸음이 합쳐져 어떤 수학적 명제가 _참이라는 것_이 보이는 곳까지 당신을 데려갈 수는 있지만, 왜 참인지까지 알려 주지는 못합니다. 이해가 없다면, 당신이 이미 믿고 있지 않은 것을 _설득_하지 못할 수도 있습니다. 그것은 지식이며 이해나 심지어 믿음으로 이끌 수 있지만, 동시에 당신을 길 잃게 만들 수도 있습니다.
우리는 일상에서 “믿음(belief)”이라는 단어를 아주 다양한 뜻으로 씁니다. 확실히 아는 것은 아니지만 믿는 것, 이해하지 못해도 믿는 것, 혹은 알고 이해하기 때문에 믿는 것에 대해 이야기할 수 있습니다. 종교적 믿음이나 외계인에 대한 믿음을 말하기도 하고, 과학적 권위를 믿는다거나 배중률(law of the excluded middle)을 믿는다거나, 눈으로 보는 것의 절반만 믿으라든가, 들리는 건 아예 믿지 말라는 속담을 말하기도 합니다.
어떤 믿음은 지식과 이해에 근거하고, 또 어떤 믿음은 신앙이나 흔히 “직관”이라고 부르는 것들에 근거합니다.
그리고 어떤 믿음은 상상력에 근거하기도 하는데, 여기서 우리는 청이 수학에서 “믿음”이 하는 역할이라고 보는 것에 더 가까워집니다. 즉 어떤 맥락에서는, 아직 확실히 알지도, 증명할 방법도 없지만 뭔가가 참일 수밖에 없다는 강한 직관이나 확신을 갖게 될 수 있습니다. 때로는 그 확신이 틀리기도 하지만, 수학자가 하는 일을 한 가지로 생각해 보자면, 그들은 어떤 것을 상상하거나 그것을 믿게 되고, 왜 그것이 참일 수 있는지 이해하는 방법을 모색하고, 그 다음에야(그리고 항상 그런 것도 아닙니다) 그것을 증명하는 작업을 한다는 것입니다. 특정 분야의 수학자들이 어떤 것이 참임에 폭넓게 동의하지만, 그것을 뒷받침하는 증명은 아직 전혀 없는 경우도 있습니다.
이것이 청이 말하는 “믿음”이며, 그것이 지식과 이해와 상보적이라는 뜻입니다. 종종 믿음이 이해에 앞서 오기도 합니다(물론 다른 이해들에 기반하여), 그리고 증명은 지식을 밀도 있게 소통하는 역할을 주로 합니다. 하지만 그녀가 지적하듯, 증명은 사람을 잘 설득하지 못하고, 대체로 독자가 이미 충분한 지식(과 호의)을 쌓아, 증명이 보통 생략하는 이해를 스스로 재구성해 내기를 기대합니다. 증명이 잘 전달하지 못하는 이해를 독자가 스스로 재구성함으로써, 그 증명이 증명하고자 하는 명제의 진실을 스스로 납득하게 되는 것입니다. 하지만 해박한 수학자라면 종종 증명 없이도 그 믿음에 도달할 수 있습니다.
그러나 응축된 증명 없이, 이해를 곧장 전달하는 일은 단순히 더 어렵습니다. 여기서 지식을 대표하는 것이 바로 문자로 쓰인 증명이며, 그것은 한 사람의 마음속 이해(그리고 바람직하게는 믿음)를 다른 사람의 마음으로 옮기는 이 중요한 역할을 수행합니다.
제가 여기서 청의 구성을 따르는 것은, 그가 이 과정을 이야기하는 방식이 특히 설득력이 있다고 생각하기 때문입니다. 하지만 수년에 걸쳐, 다른 수학자들도 수학자란 무엇을 의미하는지 매우 비슷한 방식으로 말한다는 것에 감명을 받아 왔습니다. 록하트(Lockhart)를 보세요. 혹은 서스턴(Thurston). 바디우(Badiou)! Quanta에서 봤던 그 다른 사람도요 lol. 수학은 중요한 어떤 의미에서 지식이 아니라 이해와 믿음에 관한 것이고, 그러한 믿음을 응축된 문자 지식의 형태인 증명으로 옮겨 놓는 작업은 많은
그리고 어떤 면에서 많은 분야들은, 수학이 지식을 전달하기 위해 가진 밀도 높은 기호 체계를 갖고 있지 않기 때문에 더 어렵습니다. 그래서 우리는 직관과 이해를 전달해야 하는데, 그러려면 말이 훨씬 더 많이 필요하고, 그만큼 부정확함, 오해, 오소통의 여지가 더 많이 열립니다. 수학자들이 지적하듯, 이해 같은 것을 직접 전달하는 일은 매우 어렵습니다. 그 공백을 메우는 것이 증명의 역할이지만(청이 말하듯, 그것만으로 충분한 이해가 전해지는 것도 아니며, 그걸 위해서는 증명 바깥의 소통에 의존합니다).
당신은 이미 많은 지식과 이해, 수많은 관찰을 갖고 있고, 그러다 영감을 받습니다
수학만의 이야기도 아니라고 생각합니다. 이 과정은 일반적으로 많은 인간 활동이 작동하는 방식이기도 합니다. 어떤 것의 전문가가 되면 수많은 사실을 알고 이해하게 되고, 그러고 나면 _영감_과 직관, 그리고 말하자면 _믿음_에 사로잡히게 됩니다.
“수학에서의 증명과 진보(On Proof and Progress in Mathematics)”에서, 윌리엄 서스턴은 컴퓨터 프로그래밍이 수학보다 훨씬 더 어렵다고 말합니다. 수학을 잘 못한다고 생각하는 많은 프로그래머들에게는 놀라운 주장일 겁니다. 그는 그 이유 중 일부를 나열하는데, 예컨대 서로 다른 운영체제와 끊임없이 업데이트되는 다른 소프트웨어의 버전들과 소프트웨어를 호환되게 만드는 데 따르는 수많은 어려움 같은 것들입니다.
하지만 여기서 더 깊은 요점은, 프로그래밍이 수학자들이 의지하는 이해나 믿음이 아니라 오로지 증명에 관한 일이라는 것입니다. 증명은 프로젝트의 전부입니다. 속담에 이르길, 당신이 한 번이라도 프로그램을 작성해 봤다면 당신은 프로그래머입니다. 그런데 프로그램이란 무엇인가요? 기계가 실행할 수 있는 텍스트 조각입니다.
커리–하워드 대응(Curry–Howard correspondence)에 따르면, 프로그램은 수학적 의미에서의 증명입니다. 그리고 증명인 만큼, 수학에서 증명이 갖는 문제들을 그대로 겪습니다. 그것들은 밀도가 높고 이해하기 어렵고, 읽기 즐겁지 않은 경우가 많습니다. 그것들은 지식만 전달할 뿐, 그 안에(어쩌면) 들어 있었을 아름다운 이해와 영감은 전달하지 못합니다.
실제로 프로그래머들이 어떤 코드가 동작하긴 하는데 왜 동작하는지는 모르겠다고 말하는 것을 자주 봅니다. 이 과정은 수학자들이 하는 일과 정확히 반대입니다. 수학자들은 아직 이해하지 못한 아이디어에 대해 증명을 쓰려고 하지 않습니다! 하지만 프로그래머들은 늘 그렇게 합니다. 그것이 컴퓨터 프로그래밍의 본질입니다. 항상 반드시 그래야 하는 것은 아니라고 생각합니다. 아마 그래서 어떤 컴퓨터 과학 교사는 알고리즘 설계나 자료구조 설계를 가르치려 했을 것입니다. 프로그래머들에게 수학자들이 갖는 종류의 영감으로 이끌 수 있는 이해의 기반을 제공하려는 것이죠.
그리고 때때로 라이브러리 설계에서 이런 과정을 볼 수 있다고 생각합니다. 예를 들어 에드워드 크메트(Edward Kmett)는 수학자처럼 이 과정을 밟고 있는 것이 분명해 보입니다. 믿음, 이해, 그리고 lens 라이브러리를 쓰고 나서 한동안은 아무도 그가 써 놓은 멋진 증명을 이해하지 못했지만, 점차 그것이 사람들을 설득했고 하스켈 커뮤니티의 기본적인 이해와 믿음을 바꾸어 놓았습니다. 비슷한 과정을 언어 개발에서도 때로 볼 수 있다고 생각합니다. 저는 PureScript와 Unison 등에서 벌어지는 압도적인 _확신(conviction)_의 전개를 지켜보고 있습니다.
하지만 컴퓨터 프로그래밍의 일상 업무는 증명을 쓰는 일입니다. 그것도 반드시 우아하고 아름다운 증명이 아니라, 인간의 이해를 위해 설계된 증명도 아니라, 기계가, 많은 기계가, 반복해서 실행하는 엄격함을 견뎌야 하는 증명입니다. 그리고 나서 벤치마크를 돌리고, 프로파일링하고, CI 테스트를 돌립니다.
그렇지만 프로그래머들은 서스턴이 말하는 수학의 진보라는 의미에서, 이 분야에서 진전을 만들 수는 없습니다. 학계의 컴퓨터 과학은(혹은 예컨대 크메트 같은 이는) 그럴 수 있고, 어쩌면 이것이 사람들이 당신에게 CS 학위를 요구하는 이유 중 하나일 것입니다. 이해를 발전시키는 과정을 통해서만 컴퓨터 프로그래밍이라는 분야가 진보할 수 있기 때문입니다.
제 글이 마음에 드신다면 커피 한 잔 사주기를 고려해 주세요. 혹은 제가 하스켈과 닉스(Nix)에 관해 가르치고 글 쓰는 곳인 Type Classes를 확인해 보세요.
