有一次系里举办教授们的“闪电式演讲”(lightening talk),每位教授只有5分钟时间上去介绍自己的研究。轮到 Friedman 的时候,他慢条斯理的走上去,说:“我不着急。我只有几句话要说。我不知道我能不能拖够5分钟……”大家都笑了。他接着说:“我现在最喜欢的东西是 Curry-Howard correspondence 和定理证明。我觉得现在的机器证明系统太复杂了,比如 Coq 有 nnnnn 行代码。我想在 x 年之内,简化 Coq,得到一个 miniCoq……”
miniCoq... 听到这个词全场都笑翻了。为什么呢?自己去联想吧。从此,“Dan Friedman 的 miniCoq” 成为了 IU 的程序语言学生茶余饭后的笑话。
但是 Firedman 没有吹牛。他总是说到做到。他已经写出一个简单的定理证明工具叫 JBob(迫于社会舆论压力,不能叫 miniCoq),而且正在写一本书叫 《The Little Prover》,用来教授最重要的定理证明思想。他开始在 C311 上给本科生教授这些内容。我看了那本书的初稿,获益至深,那是很多 Coq 的教材都不涉及的最精华的道理。它不仅教会我如何使用定理证明系统,而且教会了我如何设计一个定理证明系统。我对他说:“你总是有新的东西教给我们。每隔两年,我们就得重新上一次你的课!”
C311当我刚从 Cornell 转学到 IU 的时候,Dan Friedman 叫我去上他的研究生程序语言课 B521。我当时以自己在 Cornell 上过程序语言课程为由,想不去上他的课。Friedman 把我叫到他的办公室,和蔼的对我说:“王垠,我知道你在 Cornell 上过这种课。我也知道 Cornell 是比 IU 好很多的学校。可是每个老师的教学方法都是不一样的,你应该来上我的课。我和我的朋友们在这里做教授,不是因为喜欢这个学校,而是因为我们的家人和朋友都在这里。”后来由于跟 Amr Sabry(我现在的导师)的课程 B522 时间重合,他特别安排我坐在本科生的 C311 的课堂上,却拿研究生课程的学分。后来发现,这两门课的内容基本没有区别,只不过研究生的作业要多一些。
在第一堂课上,他说了一句让我记忆至今的话:“《The Little Schemer》和《Essentials of Programming Languages》是这门课的参考教材,但是我上课从来不讲我的书里的内容。”刚一开始,我就发现这门课跟我在 Cornell 学到的东西很不一样。虽然有些概念,比如 closure,CPS,我在 Cornell 都学过,在他的课堂上,我却看到这些概念完全不同的一面,以至于我觉得其实我之前完全不懂这些概念!这是因为在 Cornell 学到这些东西的时候只是用来应付作业,而在 Friedman 的课上,我利用它们来完成有实际意义的目标,所以才真正的体会到这些概念的内涵和价值。
一个例子就是课程进入到没几个星期的时候,我们开始写解释器来执行简单的 Scheme 程序。然后我们把这个解释器进行 CPS 变换,引入全局变量作为"寄存器" (register),把 CPS 产生的 continuation 转换成数据结构(也就是堆栈)。最后我们得到的是一个抽象机 (abstract machine),而这在本质上相当于一个真实机器里的中央处理器(CPU)或者虚拟机(比如 JVM)。所以我们其实从无到有,“发明”了 CPU!从这里,我才真正的理解到寄存器,堆栈等的本质,以及我们为什么需要它们。我才真正的明白了,冯诺依曼体系构架为什么要设计成这个样子。后来他让我们去看一篇他的好朋友 Olivier Danvy 的论文,讲述如何从各种不同的解释器经过 CPS 变换得出不同种类的抽象机模型。这是我第一次感觉到程序语言的理论对于现实世界的巨大威力,也让我理解到,机器并不是计算的本质。机器可以用任何可行的技术实现,比如集成电路,激光,分子,DNA…… 但是无论用什么作为机器的材料,我们所要表达的语义,也就是计算的本质,却是不变的。
miniCoq... 听到这个词全场都笑翻了。为什么呢?自己去联想吧。从此,“Dan Friedman 的 miniCoq” 成为了 IU 的程序语言学生茶余饭后的笑话。
但是 Firedman 没有吹牛。他总是说到做到。他已经写出一个简单的定理证明工具叫 JBob(迫于社会舆论压力,不能叫 miniCoq),而且正在写一本书叫 《The Little Prover》,用来教授最重要的定理证明思想。他开始在 C311 上给本科生教授这些内容。我看了那本书的初稿,获益至深,那是很多 Coq 的教材都不涉及的最精华的道理。它不仅教会我如何使用定理证明系统,而且教会了我如何设计一个定理证明系统。我对他说:“你总是有新的东西教给我们。每隔两年,我们就得重新上一次你的课!”
C311当我刚从 Cornell 转学到 IU 的时候,Dan Friedman 叫我去上他的研究生程序语言课 B521。我当时以自己在 Cornell 上过程序语言课程为由,想不去上他的课。Friedman 把我叫到他的办公室,和蔼的对我说:“王垠,我知道你在 Cornell 上过这种课。我也知道 Cornell 是比 IU 好很多的学校。可是每个老师的教学方法都是不一样的,你应该来上我的课。我和我的朋友们在这里做教授,不是因为喜欢这个学校,而是因为我们的家人和朋友都在这里。”后来由于跟 Amr Sabry(我现在的导师)的课程 B522 时间重合,他特别安排我坐在本科生的 C311 的课堂上,却拿研究生课程的学分。后来发现,这两门课的内容基本没有区别,只不过研究生的作业要多一些。
在第一堂课上,他说了一句让我记忆至今的话:“《The Little Schemer》和《Essentials of Programming Languages》是这门课的参考教材,但是我上课从来不讲我的书里的内容。”刚一开始,我就发现这门课跟我在 Cornell 学到的东西很不一样。虽然有些概念,比如 closure,CPS,我在 Cornell 都学过,在他的课堂上,我却看到这些概念完全不同的一面,以至于我觉得其实我之前完全不懂这些概念!这是因为在 Cornell 学到这些东西的时候只是用来应付作业,而在 Friedman 的课上,我利用它们来完成有实际意义的目标,所以才真正的体会到这些概念的内涵和价值。
一个例子就是课程进入到没几个星期的时候,我们开始写解释器来执行简单的 Scheme 程序。然后我们把这个解释器进行 CPS 变换,引入全局变量作为"寄存器" (register),把 CPS 产生的 continuation 转换成数据结构(也就是堆栈)。最后我们得到的是一个抽象机 (abstract machine),而这在本质上相当于一个真实机器里的中央处理器(CPU)或者虚拟机(比如 JVM)。所以我们其实从无到有,“发明”了 CPU!从这里,我才真正的理解到寄存器,堆栈等的本质,以及我们为什么需要它们。我才真正的明白了,冯诺依曼体系构架为什么要设计成这个样子。后来他让我们去看一篇他的好朋友 Olivier Danvy 的论文,讲述如何从各种不同的解释器经过 CPS 变换得出不同种类的抽象机模型。这是我第一次感觉到程序语言的理论对于现实世界的巨大威力,也让我理解到,机器并不是计算的本质。机器可以用任何可行的技术实现,比如集成电路,激光,分子,DNA…… 但是无论用什么作为机器的材料,我们所要表达的语义,也就是计算的本质,却是不变的。