缅怀大师
罗宾·米尔纳
2010年3月20日，图灵奖得主罗宾•米尔纳（Robin Milner）辞世，享年76岁。米尔纳是第四位获此殊荣的英国科学家，由于在LCF可计算函数逻辑、ML和CCS并发理论等计算机程序设计语言方面的贡献荣获1991年图灵奖。
从中学教师到计算机学家
1934年，米尔纳生于英国普利茅斯的一个军人家庭，曾加入过英国皇家工程兵部队，获得少尉军衔。米尔纳先后就读于伊顿公学及剑桥大学国王学院，接受了全英国最顶级的学校教育。大学期间，米尔纳曾在世界上第一台存储程序式电子计算机EDSAC上面编写过程序，只是当时他在计算机方面并没多大兴趣。1957年，他获得剑桥大学数学学士学位，然后成为一名中学数学教师。
1960年，米尔纳开始重新规划自己的未来，成为伦敦著名的Ferranti公司的计算机编程人员，决定重返这个领域，并“把一生都献给计算机”。又过了三年，米尔纳转入大学从事教学与研究，先后在伦敦城市大学、斯旺西大学以及斯坦福大学任职。
在爱丁堡大学的学术人生
1973年，米尔纳回到英国爱丁堡大学，在这里做出了许多有价值的研究，对整个计算机科学产生了重要影响。
LCF（Logic for Computable Functions）是米尔纳提出的形式化逻辑系统的一个数学模型，最早的自动定理证明工具之一。LCF不仅可以有效建模，还可以方便地验证计算机程序的正确性，受到学术界的高度评价。20世纪70年代初，米尔纳在斯坦福大学的人工智能实验室做访问学者时，曾用LCF证明了一个很复杂的编译器的正确性，受到1971年图灵奖获得者、有“人工智能之父”之称的麦卡锡的高度赞扬。
米尔纳主持开发了ML（Metalan-guage）并使之标准化，是另一重大贡献。ML是一种用来描述、表达与验证其它语言的语言，比LCF具有更强的推理能力。这种结构优美而又短小精悍的语言，被誉为是定义得最完善、最无懈可击的语言之一，也是Haskell和F#等语言的先祖。无论工作生活，米尔纳都谦虚严谨，完全没有大师架子。ML从最早时仅是专用语言到现在被用作通用语言的发展过程，和他从善如流、吸纳合作者意见有着不小的关系。其中标准ML允许设计“大模块”程序的功能，就是根据贝尔实验室的麦克奎因（D．MacQueen）所提出的构思实现的。
CCS是米尔纳提出的一种利用代数方法创造的计算模型，在交叠式并发概念的基础上，建立并发与并行计算的概念框架。作为目前最典型的两个描述性并发模型之一，CCS已经成功地用来解释用于书写通信协议规约的国际标准语言Lotos，极大地推动并促进了并发与并行计算的发展。
米尔纳在爱丁堡大学任教20多年，做出了不少贡献。该校的计算机科学基础实验室就是他在1986年一手创建的。米尔纳还曾向爱丁堡大学现在的信息学院提供了一笔捐款，成立了以他名字命名的罗宾•米尔纳演讲，每年举行一次，邀请计算机科学领域最杰出的学者来作报告。
重返剑桥，一生的归属
1995年，61岁的罗宾•米尔纳回到母校剑桥大学，担任剑桥大学计算机实验室主任。人生的最后15年，仍作为剑桥大学计算机实验室教授从事科学研究，主要研究模型在普适计算中的系统应用。他临终还在研究Bigraph（这是一种包含CCS和Pi演算的普适计算形式）。
米尔纳在大学期间兴趣广泛，喜欢罗素的分析哲学和音乐。米尔纳的双簧管演奏非常出色，当时他梦想成为一名音乐家，大学时的主要精力都放在这上面。也许是当时一堂EDSAC编程课让他对编程产生厌恶，因此尽管大学毕业时很多人劝他留校，他还是走了，跑去当了一名中学数学教师。然而人生兜兜转，米尔纳依然毕生情牵计算机。
从剑桥开始，又在剑桥结束。2010年3月20日，在妻子葬礼后的第三天，罗宾•米尔纳在英国剑桥辞世。他的故事和成就，将永远留在历史中，留在人们的心里。
（本文来自《程序员》10年05期杂志，更多精彩内容敬请关注10年05期杂志）
原文地址：http://www.programmer.com.cn/3032/#more-3032