瓦德勒追随科学巨人

https://iohk.io/en/blog/posts/2023/07/06/professor-philip-wadler-follows-the-giants-of-science-at-the-royal-society/

image

许多 Cardano 用户都知道 Philip Wadler 教授是区块链智能编程语言 Plutus 的联合创始人(与 Manuel Chakravarty 一起)。 他在计算机语言和函数式编程方面的工作为他赢得了教授职位、大量奖项以及爱丁堡皇家学会的研究员资格。 任何使用过 Java、Haskell 或 XQuery(实际上是任何函数式语言)的人都从 Wadler 的工作中受益。

本月,他将与包括牛顿在内的早期科学巨人一起成为世界上最古老的科学院英国皇家学会的会员。 他将成为一名FRS。

这一荣誉证明了他的职业生涯跨越了微处理器时代和数字技术的蓬勃发展。 学术效果用h指数体系来衡量:经过20年的研究,20分为良好,40分为优秀,60分为特殊。 瓦德勒的得分为 73 分,基于他的作品在已发表的论文和书籍中被引用了 26,981 次。

他的传记称他“喜欢将理论引入实践,将实践引入理论”,他确实做到了这一点。 他曾是牛津大学的研究助理,并在格拉斯哥获得了第一个教授职位 - 在那里他是 Haskell 的主要设计师之一。 随后,他在贝尔实验室和 Avaya 实验室工作。 自 2003 年起,Wadler 一直担任爱丁堡大学信息学院理论计算机科学教授。

“我坚信理论和实践相结合,”瓦德勒说。 “同时考虑两者的重要性是整个科学史上的一个主题,从 Blaise Pascal(为概率论奠定了基础的法国数学家和哲学家)到 Robin Milner(帮助设计了 ML 语言,一种 Haskell 的先驱,在爱丁堡]。

他认为学术界的巨大优势是“你可以教书”。 与年轻人一起工作有助于保持年轻的感觉,教学可以提高沟通技巧。

“我很高兴能受邀参加许多行业会议,在那里发言的年轻开发人员都很聪明且富有灵感,但只有其中一些人学会了如何有效沟通。”

当年轻的瓦德勒向美国数学会投稿时,他清楚地意识到了写作的重要性。 那是 1975 年,他在参加了加州大学伯克利分校为高中生开设的课程后写下了这本书。 “我试图以最通用的方式来设置它,但我的导师告诉我,这使它难以理解! 他们让我以更具体的方式重写它,使其更易于理解。

“让我明白让读者轻松阅读这本书是多么重要,这对我来说是一个重要的教训。”

要理解 Wadler 的世界,就要发现 lambda 演算、责任跟踪、渐进类型、类型类和 monad 等词汇。 在这个地方,无精打采比懒惰更好,如果你想偷懒,你应该好好地去做。 大多数人永远不会遇到这些术语,但他遵循了让人们更容易理解想法的建议。 他的许多学术论文中的幽默和他引人入胜的演讲风格都证明了这一点。 诸如“Formlet 成语指南”、“剩下的咖喱和重新加热的披萨”以及“Et tu,XML?”之类的标题很难忘记。 他身着 Lambda Man 服装出席演讲的情景令人难忘。

位于硅谷的中心
瓦德勒在库比蒂诺高中上学,该高中位于加利福尼亚州旧金山湾区,后来成为硅谷。 他认为自己会成为一名数学家,“但找到一份编码工作更容易,而且更赚钱。”他赞扬了三位早期的老师,“尤其是在学校教数学的西蒙斯先生和格罗特先生,以及杰拉尔德·亚历山大森, 他在我参加的圣克拉拉大学教授微积分课程。”

1977 年,他在斯坦福大学获得了数学学位。前一年,史蒂夫·沃兹尼亚克 (Steve Wozniak) 和史蒂夫·乔布斯 (Steve Jobs) 开始营销他们的 Apple I 套件,其中包括 MOS Technology 的 8 位 6502 芯片和 4KB 用户内存。 Donald Knuth 已经完成了他的编程作品的第三卷(最新的部分于去年出版)。 这是 Fortran、Cobol、Lisp 和 Algol 的时代; Forth、Pascal 和 C 是相对较新的成员。 Xerox Parc 正在开发 SmallTalk。 微型计算机尚未到来并普及Basic。 工程师仍然携带计算尺。 两年前,道格拉斯·霍夫施塔特 (Douglas Hofstadter) 的经典著作《哥德尔、埃舍尔、巴赫》(简称 GEB)出版; 比 Acorn 的 BBC Micro 和 IBM 的 PC 早四年。 蒂姆·伯纳斯·李正在牛津大学学习物理学,距离提出万维网还有几十年的时间。

大多数这些里程碑式的时刻都与瓦德勒的个人历史有关。 他的下一篇论文是在斯坦福大学二年级时写的——为高德纳教授的课程写的。 那是一个性格形成的时期。 “Knuth 的数据结构课程,由他的老师教授tbook,是一次很棒的学习经历。 除此之外,他还给了我们几页关于如何编写数学文本的笔记。 这些笔记是我学术生涯的开始。 直到今天我还提到他们。

这篇题为“实时垃圾收集算法分析”的论文为 Wadler 赢得了众多荣誉中的第一个:来自美国科学协会计算机协会 (ACM) 的 Forsythe 学生论文奖。

斯坦福大学最有影响力的课程是经济学导论。 “我不记得老师的名字了,但网络搜索显示是约翰·格利。 他是卡尔和格劳乔这两个马克思的混合体。 他了解自己的东西,并以一种非常有趣的方式呈现它。 他会教我们直接的经济学。 然后每隔一周左右他就会说“我一直在教你们标准理论,现在我要告诉你们真相”并给我们提供马克思主义的观点。 我从中学到的是公平地提出相反观点的重要性。

“尽管他强烈地认为标准观点是错误的,但他想将其正确地呈现给我们。”

其他讲师包括约翰·麦卡锡(John McCarthy)和互联网创始人之一温特·瑟夫(Vint Cerf)以及高德纳(Knuth)。 “我从这三个人那里学到的一件重要的事情是幽默在你们的工作中的重要性。 Vint 是贝内特·瑟夫(Bennett Cerf)(幽默作家和打油诗收藏家)的侄子,这表明了这一点。 当温特向我解释互联网时,他引用了吉尔伯特和沙利文的歌剧《HMS Pinafore》,唱道“它会丢失任何数据包吗? 绝不。 什么从来没有? 好吧,几乎没有”。

人工智能领域的先驱麦卡锡教瓦德勒“如何用 Lisp 编程”。 也就是说,我学到了函数式编程的本质。”

在斯坦福大学期间,瓦德勒参加了自制计算机俱乐部的会议。 “有一天,一个人带着一块可以连接到电视和键盘的单板出现。 原来是Apple I。向我们展示它的人可能是沃兹尼亚克,但我的注意力集中在电脑上,没有注意到机器后面的人。 我希望从那时起我能变得更加关心别人。”

霍夫施塔特根据尚未出版的 GEB 草案教授了另一门课程。 当这本书于 1979 年出版时,书中称赞瓦德勒与霍夫施塔特产生了“共鸣”。 “我对此感到非常自豪。”瓦德勒的室友、图形艺术家斯科特·金在书中被感谢为“巨大的影响”。

瓦德勒在施乐帕克研究中心担任暑期实习生。 在那里,他在 Smalltalk 的早期版本中实现了一个模拟器,“这是一个微小而优雅的系统”。 “有很多关于“dynabooks”的讨论,虽然当时还不存在,但就是我们现在所说的笔记本电脑”。

在卡内基梅隆大学,瓦德勒正在研究人工智能,诺贝尔奖得主赫伯特·西蒙(Herbert Simon)是瓦德勒头两年的导师。 这导致瓦德勒开始关注编程语言。 “我意识到人工智能最让我感兴趣的部分是如何表示信息,我认为编程语言可以更直接地解决这个问题。 再说一次,我对与我共事的人感到非常幸运,首先是西蒙,然后是比尔·谢里斯、小盖伊·斯蒂尔和尼科·哈伯曼。

瓦德勒从卡内基梅隆大学获得博士学位,他的论文“无精打采比懒惰更好:一种通过改变应用程序来消除中间列表的算法”。斯蒂尔和哈伯曼是他的论文导师。

霍夫施塔特的书; 菲利普·瓦德勒 (Philip Wadler) 由他的儿子亚当 (Adam) 拍摄; 英国皇家学会在伦敦的办事处
工业界和学术界
从 1983 年起,Wadler 成为牛津大学编程研究小组的研究员和成员,发表了多篇论文,其中《如何用一系列成功取代失败》被引用最多。

之后,在格拉斯哥大学,Wadler 担任 Haskell 的主要设计者,Haskell 成为使用最广泛的惰性函数式编程语言。 他贡献了两项主要创新:1989 年与 Stephen Blott 合作的类型类,以及 1993 年与 Simon Peyton Jones 合作的 monad。这些创新帮助他成为最受认可的计算机科学作者之一,并于 1993 年获得了教授职位。 monad 论文 2003年获得ACM过去十年最具影响力论文奖。

Glasgow Haskell 编译器 (GHC) 在格拉斯哥开发,Peyton Jones 和 Simon Marlow 作为其创建者于 2011 年获得了 ACM 软件奖。 Wadler 于 2016 年获得了杰出服务奖。他的 Plutus 联合创始人 Chakravarty 补充道:“不久之后,他使用 monad 的分类概念提供了一种处理数据输入和输出的函数式方法,而通用命令式编程的贡献已经 再次产生巨大的影响。 类型类和 monad 一起在很大程度上决定了软件架构师如何在 Haskell 中设计程序。 这两个概念都被其他语言所采用。

除了实施卡尔达诺的核心之外,我在 Haskell 中,Wadler 列举了众多著名应用程序中最受欢迎的三个。 首先,Facebook 使用 Simon Marlow 创建的 HAXL 库来过滤其发布的每条消息,以查找垃圾邮件和虚假信息。 其次,使用 Haskell 的银行数量,其影响力鼓励大多数金融公司以这样或那样的方式使用功能性语言。 SeL4,一款高度安全的手机最小操作系统,是他的最终选择。 为此,用 Haskell 编写了一个原型。 该原型构成了 Isabelle 证明助手中正式模型的基础,然后是生产实现的基础,为了速度,将其从 Haskell 翻译为 C 语言。 该翻译已根据伊莎贝尔的正式模型进行了验证。

他来自格拉斯哥,在贝尔实验室(朗讯科技)和 Avaya 实验室工作了七年; Peyton Jones 曾就职于微软研究院,现在就职于 Epic Games。 当时的两个产品是 GJ(通用 Java)——Sun Microsystems 设计的基础——和 FJ(Featherweight Java)。 后者于 1999 年推出,是可以在一张纸上编写的 Java 正式模型。 这是瓦德勒被引用最多的论文之一。 正如他所说。 “GJ 将理论付诸实践; FJ 将实践带入理论。

在 Avaya,Wadler 发表了有关 XQuery 的论文,XQuery 是一种用于查询 XML 和组合数据(无论是文档、数据库还是网页)的语言,由万维网联盟 (W3C) 开发。 它使得其他语言的复杂程序可以被几行代码替换。

随后,2003 年,他获得了爱丁堡理论计算机科学系主任的职位。对于瓦德勒来说,担任该职位是一个轻松的决定,因为他能够接替他心目中最伟大的科学英雄之一罗宾·米尔纳 (Robin Milner) 的职位。 (另一个是托尼·霍尔,快速排序算法的发明者)。 “当我在爱丁堡获得这个职位时,我无法拒绝,因为这个职位最初是为罗宾·米尔纳设立的。”

将 lambda 印在 T 恤上的人
高德纳、麦卡锡和瑟夫向瓦德勒灌输了学术论文和演讲中幽默的重要性。 他的博士论文是“无精打采比懒惰好”,他发表的第一篇论文是“如何用一系列成功取代失败”。 “在那之后,”他说,“就没有回头路了”。 他很高兴自己的论文标题出现在 Helen Sword 的教科书《时尚学术写作》中。

听过瓦德勒讲座的人都会看到他变身为 Lambda Man,一位盛装打扮的超级英雄。 Lambda 演算——λ-演算——是数学逻辑中的一个形式系统,是 Haskell 的基础。 当瓦德勒开始在 T 恤上画公式,然后“撕下我的外衣以揭示公式”,从而为学术会议上的讲座增添趣味时,超级英雄的转变就开始了。 为此,他有一件特殊的衬衫,上面有按扣而不是纽扣。 “一件 T 恤展示了 RAG Seely 对线性逻辑的明确描述——他好心地同意与这件 T 恤一起作为“Seely 模特”合影。”

在另一次会议上,一位同事坐在酒吧里,将瓦德勒的滑稽动作与超人进行了类比; 然后‘一个灯泡灭了。 我委托 Matija 和 Mojca Pretnar 制作了 lambda 设计,并将其印在我购买的超人服装的正面。

同行评审使 IOG 变得“独一无二”
六年前,瓦德勒遇到了 Input Output Global (IOG) 首席执行官兼联合创始人查尔斯·霍斯金森 (Charles Hoskinson),之后开始为 Input Output 工作。 霍斯金森正在拜访该公司首席科学家兼爱丁堡区块链技术实验室创始人 Aggelos Kiayias 教授。 “查尔斯要求与我见面。 我刚刚认识了万达,她住在里约热内卢,最终成为我的妻子。 考虑到飞往巴西的许多航班的费用,我向查尔斯请求一份咨询工作。 这对我来说很大胆,但这是我做过的最好的选择之一!”

他们对学术界对工业界重要性的共同看法立即显而易见。 “我最欣赏 Charles 的一点是,他坚持认为 IOG 所做的一切都应该基于同行评审的研究。 正如他指出的,这是科学的基础。

IOG 为爱丁堡实验室和其他几所大学的研究中心提供资金,这一策略在科技公司中并不罕见。 然而,Wadler 认为 IOG 走得更远:“对于复杂的加密协议,同行评审的研究是确保其正确性的最佳方式。” 然而,据我所知,IOG 的这种坚持是独一无二的。 不仅在加密领域,而且在所有计算领域。 谷歌或微软将允许他们的开发者发布内容,但他们并不认为这是迈向可靠性的关键一步。

Wadler 为 IOG 论文做出了贡献,内容包括:扩展 UTXO,Cardano 使用的账本模型; System F,Haskell 和 ML 等语言理论基础的重要元素; 和区块链合约。

Wadler 简洁优雅的方法,如 Featherweight Java 论文中所见,再次问世2018 年 Plutus 发布时。在爱丁堡的 PlutusFest 活动上,团队分发了黑色餐巾纸,上面用金色墨水印有 Plutus 的语言规范。 这是霍斯金森首先提到的一个想法,但正如查克拉瓦蒂补充道,“这实际上可以追溯到菲尔从一开始就坚持让普利托斯核心尽可能小”。 后来,查尔斯提出了餐巾纸的评论,但菲尔同意了这个想法,这就是我们最终得到爱丁堡餐巾纸的原因。

简单性、安全性和保密性是 Plutus 的核心,这一切都是通过函数式编程和 Haskell 实现的。

证明 Plutus 的核心语义可以放在餐巾纸上
数学的力量
贯穿瓦德勒著作的一条主线是数学的价值。 “许多人害怕数学,”他说,因为“他们认为数学对他们来说太难了。” 如果熟悉 Javascript 的老练开发人员看到幻灯片上用斜体写的内容,他们会尖叫着跑出房间,因为它看起来像正式的数学。

然而,数学是理解我们周围世界的极其强大的工具,并且已经被使用了数千年。 每一代人都将自己的发现传授给下一代。 瓦德勒最喜欢的引言之一是苏格兰博学者约翰·阿布斯诺特 (John Arbuthnot) 于 1692 年出版的《机会法则》一书中所说的:

我们所知道的事情很少不能被简化为数学推理; 当他们不能时,就表明我们对他们的了解非常少且混乱; 当可以进行数学推理时,利用任何其他推理就如同在黑暗中摸索一样,当你身边有一根蜡烛时。

这种理解链是他向年轻同事强调的。 “只有当你所做的工作能够激励他人做得更好时,它才重要。 我为自己写的论文感到自豪,也为其他人在我的工作基础上撰写的论文感到自豪。

他再次强调简单性。 “推论就是简单性的重要性。 你必须以一种其他人可以接受和借鉴的方式来展示你的作品。 我的很多同事都太聪明了! 他们足够聪明,可以处理大量的复杂性,但这使得他们所做的事情更难吸收。 请针对像我这样的傻瓜来写。 与最初的发现一样重要的是简化和完善的努力。

世界上最伟大的签名书
7 月 14 日,Wadler 将于伦敦 Carlton House Terrace 亮相。 在那里,作为 80 名杰出研究人员、创新者和传播者之一,他将成为英国皇家学会会员。 这个学术团体的历史可以追溯到 1660 年——创始人之一是 Christopher Wren 和 Robert Boyle。 该建筑俯瞰着购物中心,这是连接特拉法加广场和白金汉宫的盛大游行路线。 正如此后的每一位君主一样,建造了The Mall 的查理二世也对协会给予了赞助。 查理三世国王自 1978 年以来一直是皇家院士。

瓦德勒将在一本账本上签下自己的名字,该账本以查理二世的签名开头,其中充满了科学史上最聪明的名字。 现任和前任研究员包括查尔斯·巴贝奇(Charles Babbage),他的差分机是第一个数字计算设备; 人工智能先驱、战时密码破译英雄艾伦·图灵; 霍尔; 米尔纳; 伯纳斯-李; David Deutsch,量子计算之父; Sophie Wilson,BBC Micro 联合架构师,帮助开发了为全球智能手机提供动力的 ARM 芯片架构; 和佩顿·琼斯。 Knuth 和 Cerf 是外籍成员。

两个早期的研究员是艾萨克·牛顿和罗伯特·胡克。 牛顿以其万有引力定律理论而闻名,他的《数学原理》及其三大运动定律极大地影响了欧洲的启蒙运动。 胡克发现了微生物并创造了“细胞”一词,尽管他最为几代学童所熟知的可能是胡克定律,该定律描述了力对金属弹簧的影响。 1675年,两人书信通信。 牛顿写道:“如果说我看得更远,那是因为我站在了巨人的肩膀上。”7月14日之后,瓦德勒的名字将与这些巨人的签名并列,他将期待着与他的研究员合作的机会。