컴퓨터 과학자로서의 삶
로빈 밀너(Arthur John Robin Gorell Milner)는 1934년 1월 13일에 영국 플리머스 근방에서 태어났다. 그의 부친은 군인이었고 그래서 이사를 자주 다녔다.2 13살이 되던 해에 그는 시험을 통해 장학생으로 이튼 칼리지라는 공립학교에 들어갔다. 그리고 1952년에는 장학생으로 케임브리지 대학교에 입학했다.
대학에 입학하자마자 그는 병역 의무를 수행했다. 2년 동안 그는 중장비를 다루는 공병대의 장교로 근무했다. 1954년에 제대한 그는 케임브리지 대학교의 킹스 칼리지에서 수학을 전공했고 1956년에 수학 학사 학위를 받은 후 1957년에는 철학 학사 학위도 받았다.
1956년에 그는 EDSAC에 관한 열흘 짜리 프로그래밍 강좌를 수강했는데 크게 실망했다.
내가 보기에 프로그래밍은 정말로 우아하지 않았습니다. 명령어를 하나씩 이어나가야 했는데 좀 주먹구구식이었습니다. 프로그래밍 작업이 아주 아름다운 일은 아닌 듯 보였습니다. 그래서 나는 내 인생에서 결코 컴퓨터를 가까이 하지 않겠다고 다짐했습니다!2
학문에 별 뜻이 없었던 로빈은 대학을 졸업한 후에 런던에 있는 고등학교에서 임시 교사로 일하다가 페란티에 정식 입사했다. 페란티는 맨체스터 대학교의 Mark I 컴퓨터를 상품화하여 세계 최초로 전자식 컴퓨터를 상용화한 회사였다. 로빈은 페란티가 생산한 컴퓨터를 검사하는 일을 했다.
페란티에서 다시 프로그래밍을 시작하게 된 그는 학교로 돌아가기로 마음먹었다. 그렇지만 학위는 그의 목표가 아니었다. 그는 컴퓨터를 탐구하고 싶었을 뿐이었다. (로빈은 결국 박사 학위를 받지 않았다.)
1963년에 런던의 시티 대학교에서 강사 생활을 시작한 그는, 낮에는 엔지니어들에게 수학을 가르쳤고 남는 시간에는 인공지능에 대해 알아보기 시작했다. 이 과정에서 크리스토퍼 스트레이치의 영향을 받은 언어인 CPL을 알게 되었다.
1968년이 되자 그는 스완지 대학교에서 연구원 자리를 구했다. 그는 데이비드 쿠퍼 교수의 연구 조교로 일했다. 쿠퍼 교수는 프로그램 증명, 자동 이론 증명, 의미론 등에 관심이 많았다. 로빈은 이때 직접 혼자서 자동 이론 증명 프로그램을 작성해보았는데 너무도 어려워서 큰 충격을 받았다고 한다.2
1969년에 데이나 스콧이 옥스퍼드 대학교에서 특별 강연을 했는데, 이 자리에 참석한 로빈은 데이나 스콧의 도메인 이론과 LCF(Logic of Computable Functionals)에 큰 흥미를 느꼈다.
이 시기에 그는 데이비드 쿠퍼 교수와 함께 미국의 카네기 멜런 대학교를 방문했다가 조하 매나Zohar Manna 교수의 소개로 스탠퍼드 대학교의 인공지능 연구실에서 2년 동안 일할 기회를 얻었다. 존 매카시 교수가 이끄는 인공지능 연구실에서 그는 데이나 스콧의 LCF를 구현해 보기로 마음먹었다. 증명해야 할 명제가 주어지면 이를 사용자가 증명해나갈 수 있도록 대화 방식으로 도와주는 시스템이었다.3 그는 이 시스템의 이름을 데이나 스콧의 이론과 동일하게 LCF라고 지었다. 하지만 이 LCF는 Logic for Computable Functions의 약자이다.
1973년에 영국으로 돌아온 그는 에든버러 대학교의 교수로 임용되었다. 그는 스탠퍼드 대학교에서 만들었던 LCF의 단점을 없앤 새로운 버전을 시작했다. 이 과정에서 그는 새로운 프로그래밍 언어를 만들었다. 에든버러 대학교에서 만든 LCF는 에든버러 LCF라고 불렀고, 새롭게 만든 프로그래밍 언어는 ML(Meta Language)이라는 이름을 붙였다. ML은 최초로 다형성polymorphism을 지원하는 함수형 언어이다.4
한편, 로빈은 병렬처리 시스템의 등장을 보고 이를 수학적으로 표현할 방법이 필요함을 직감했다. LCF는 순차적으로 실행되는 프로그램에는 적합했지만 병렬처리 혹은 다중처리 시스템에서 수행되는 프로그램에는 사용하기 어려웠다. 그가 보기에 병렬처리 혹은 다중처리에서 나타나는 동시성concurrency 을 표현하는 일이란, 동시적으로 수행되는 기계(혹은 프로세스) 사이의 상호작용interaction을 표현하는 것과 다르지 않았다. 그래서 그는 이런 상호작용을 수학적으로 표기하기 위한 방법을 고안했고 이것을 CCS(Calculus of Communicating Systems)라고 이름 붙였다.5
CCS는 조금 더 다듬어져서 π-calculus로 발전했다. 순차적인 시스템에서 λ-calculus가 하는 역할을 병렬 시스템에서는 π-calculus가 하는 셈이다.
로빈은 2001년에 은퇴했으나 그의 연구는 멈추지 않았다. 그는 자신의 π-calculus가 모바일 시스템을 모델링하는 데 쓰이는 것을 보고는 유비퀴터스 컴퓨팅을 위한 새로운 모델을 고민했다.
그는 2010년 3월 20일에 영국 케임브리지에서 세상을 떠났다.
답글 남기기