小小才子 通过 Google 阅读器发送给您的内容：
于 12-6-11 通过 当然我在扯淡 作者：王垠
你永远想象不到 Dan Friedman 的思想的极限在哪里。当你认为他是一个函数式语言专家的时候，他发明了 miniKanren，一种逻辑式编程语言 (logic programming language)，并且写出 《The Reasoned Schemer》，用于教授逻辑编程。当你认为他不懂类型系统的时候，他开始捣鼓最尖端的 Martin-Löf 类型理论，并且开始设计机器证明系统。而他做这些，完全是出于自己的兴趣。他从来不在乎别人在这个方向已经做到了什么程度，却经常能出乎意料的简化别人的设计。
有一次系里举办教授们的"闪电式演讲"(lightening talk)，每位教授只有5分钟时间上去介绍自己的研究。轮到 Friedman 的时候，他慢条斯理的走上去，说："我不着急。我只有几句话要说。我不知道我能不能拖够5分钟……"大家都笑了。他接着说："我现在最喜欢的东西是 Curry-Howard correspondence 和定理证明。我觉得现在的机器证明系统太复杂了，比如 Coq 有 nnnnn 行代码。我想在 x 年之内，简化 Coq，得到一个 miniCoq……"
miniCoq... 听到这个词全场都笑翻了。为什么呢？自己去联想，往歪处想 
从此，"Dan Friedman 的 miniCoq" 成为了 IU 的程序语言学生茶余饭后的笑话。
从此，"Dan Friedman 的 miniCoq" 成为了 IU 的程序语言学生茶余饭后的笑话。但是他没有吹牛，他总是说到做到。他已经写出一个简单的定理证明工具叫 JBob（迫于社会舆论压力，不能叫 miniCoq），而且正在写一本书叫 《The Little Prover》，用来教授最重要的定理证明思想。他开始在 C311 上给本科生教授这些内容。我看了那本书的初稿，获益至深，那是很多 Coq 的教材都不涉及的最精华的道理。它不仅教会我如何使用定理证明系统，而且教会了我如何设计一个定理证明系统。我对他说："你总是有新的东西教给我们。每隔两年，我们就得重新上一次你的课！"
青春就应该这样绽放 游戏测试：三国时期谁是你最好的兄弟！！ 你不得不信的星座秘密
可从此处完成的操作：
- 使用 Google 阅读器订阅当然我在扯淡
- 开始使用 Google 阅读器，轻松地与您喜爱的所有网站保持同步更新
没有评论:
发表评论