#编程语言
Daniel P Friedman在编程语言界的贡献

转自微博：https://m.weibo.cn/status/4952639604523552

因为最后一段文字，特地找了王垠的两篇文章：
* 《写小人书的老顽童》
* 《Chez Scheme 的传说》

------ 分割线，以下为原文 ------


绝对是今年计算机专业的一件大事。Daniel P Friedman，79岁高龄，在2023年出版了他的The Little ... 系列的新书，The Little Learner。


老爷子是Lazy Evaluation的发明者，Scheme届一哥，发明Scheme的人都亲口承认这一点；现在还在Scheme届抗梁的人物，除了UBC那个发明Aspect Oriented Programming、MIT肄业、Xerox Parc精英Gregor Kiczales之外，全是Friedman的徒子徒孙；因为Scheme是最接近Lambda的语言，所以Friedman可以理解为能写『顶尖』代码的Church。『顶尖』二字在这里的意思不但指它在学术界的编程能力是顶流，他给Scheme语言留下的诸如Pattern Matching宏代码可以正面刚Kernel里的所有工业代码。


不止Scheme语言教学。Friedman的同事，另一个传奇人物Kent Dybvig，写了工业级的Scheme语言编译器，Chez Scheme，包括Cisco在内的很多大企业都是他的客户。Chez Scheme后来出现了开源的版本，在这个版本里Friedman和Dybvig合作了被称为nanopass的编译器框架；虽然Scheme不是流行的工业语言，但是两个版本的Chez Scheme在编译速度和执行速度上都可以跟任何工业级语言编译器抗衡；而且Chez Scheme自带的解释器，性能高达编译器的1/2.5的水平，想想v8出现时直接把JavaScript速度提高了1000-5000倍，这个名称为Petite Chez Scheme的解释器毫无疑问是性能最好的编程语言解释器。


远不只这些。


The Little Typer，是介绍Dependent Types的入门书籍，提供了仅6000行代码实现的Pie语言；任何人都可以从这里开始了解现代计算机语言的类型系统。


The Little Prover，通过ACL2定理证明器讲解现代定理证明器使用。


The Reasoned Schemer，仍通过Scheme语言讲解relational logic和logic programming。这本书神奇的出到了第二版，令人匪夷所思，因为这实在是非常冷门的领域。该书的第二作者William E. Byrd是Friedman的学生，他在Youtube上有故弄玄虚的视频讲解他当年看到Friedman的代码时，是如何获得了被天打雷劈的感受的。


++++


以上都是符号主义在编程领域的巅峰之作。


我承认我会因为Frank Pfenning（Peter Andrews的学生，Alonzo Church的徒孙），Robert Harper（Robert Constable的学生，Stephen Cole Kleene的徒孙，Alonzo Church的曾徒孙），Steve Awodey（Saunders Mac Lane的学生，Mac Lane是Weyl和Bernays的学生，前者是Hilbert的学生，后者是Landau的学生）等人的学术成就，把他们的学术水平看在Friedman之上，这三个人是cmu三剑客，活跃在youtube上的oplss频道，讲解constructive logic, type theory和category theory。但是如果没有Friedman，你将只会淹没在符号和数学里，远没有现在这样容易只通过一种语言了解计算机科学的如此广阔的领域。


而他在79岁这一年，出版了The Little Learner，关于Deep Learning，给这本书写序的人是MIT的Guy Lewis Steele Jr.（Gerald Jay Sussman的学生）和Peter Norvig（人工智能：一种现代方法的两个作者之一）。


无法表达对老爷子的敬佩之情，不把这些书的习题都做了，都对不起他老人家。


++++


王垠写过不少盛赞Dybvig和Friedman的文字，他是令人羡慕的看见过光的人，但不知道为什么他拿着手电筒离开了印第安纳。