内核恐慌

两位主持人对 web 开发的态度；新闻是 Jeep 车被黑事件（更新：克莱斯勒已经宣布召回一百五十万辆汽车修复漏洞）；主题是微处理器开发板。 相关链接 Jeep 汽车被黑 Arduino Detect Train and Close Window with Arduino and Webcam (YouTube 视频。吴涛的记忆有误，此处并未采用声音探测器，而是摄像头) Raspberry Pi BeagleBoard Banana Pi Raspberry Pi “树莓派”: 概述与优势(上)、(下) 人物简介 Rio：《IT 公论》主播，IPN 联合创始人，Apple4us 程序员。 吴涛：Type is Beautiful 程序员，《内核恐慌》主播。

就着听众反馈，两位主持人介绍了自己管理密码的习惯；新闻包括 Hacking Team 的大泄密、Atom 1.0、以及卡马克在 VR 世界里跑 Racket 的野心。主题是 debugging——程序除错与调试。 相关链接 Lucida 「白板编程浅谈——Why, What, How」 Wired 杂志对于 Hacking Team 泄密案的报道 在浏览器中禁用 Flash 的方法 Atom Editor 1.0 Prediction of the Home Computer (1960’s) 维基百科对于 Debug 一词由来的解释 Quora 上的问题「遇到过最难解的 bug」 Valgrind PyCharm 人物简介 Rio：《IT 公论》主播，IPN 联合创始人，Apple4us 程序员。 吴涛：Type is Beautiful 程序员，《内核恐慌》主播。

「串台」故障的原因终于揭晓；吴涛的莫尔斯码 app 主意看来目前不可行；三封很长的读者反馈；主题是设计模式。两位主持人不约而同地病了，所以没有讲新闻。 节目中提及的读者 Haozhong Zhang 来信节选： 相对的，在 Formal Verification 中，举个例子，我们可以把每条指令的执行形式化表示成 {P}C{Q}，其中 C 是这条指令，P 称为前条件 (Pre-condition) 描述了 C 执行之前机器的状态 (例如某个寄存器的值是什么，某个内存单元的值是什么，通常不需要覆盖所有的寄存器和内存单元，仅需要根据验证的 Specification 选取我们关心的部分), Q 称为后条件 (Post-condition) 描述了 C 执行后的机器状态。注意，这里 Q 同时描述 C 被中断和不被中断的执行后的机器状态。非形式化的，{P}C{Q} 表示在满足前条件 P 的机器上执行指令 C 得到的机器状态满足后条件 Q。这样，对于上述的一个代码片段 C1; C2; …; CN 我们有 {P1}C1{Q1}，{P2}C2{Q2}, …, {PN}CN{QN}。然后，我们证明 Q1 ⇒ P2, …, QN-1 ⇒ PN， 从而可以证明 {P1}C1; C2; …; CN{QN}。 同样的，如果这个代码片段的 Specification 也可以写成，例如， {P}C1; C2; …; CN{Q}， 我们只需要再证明 P ⇒ P1 和 QN ⇒ Q， 即可以证明这个代码片段的确满足了给定的 Specification。因为这里的 P，Q，Pi, Qi 等描述了所有的可能情况，并且只需描述 Specification 关心的部分，所以这里的 Formal Verification 比测试更加完备和简洁。在实际工作中，我们往往会针对验证的程序的特点，设计特定的逻辑系统，以进一步的降低证明的难度和复杂度。 相关链接 读者 Wang Jian 发来的 TDD 实践视频：YouTube、优酷 Design Patterns: Elements of Reusable Object-Oriented Software 艾舍尔《天鹅》 Erich Gamma Design Patterns 15 Years Later: An Interview with Erich Gamma, Richard Helm, and Ralph Johnson Hacker’s Delight 《编程珠玑》 《建筑的永恒之道》 Cocoa Design Patterns C# Delegate/Event Patrick Naughton Python Pattern: “Borg” God Object Golden Hammer The Lone Ranger 人物简介 Rio：《IT 公论》主播，IPN 联合创始人，Apple4us 程序员。 吴涛：Type is Beautiful 程序员，《内核恐慌》主播。

Rio 使用 HHKB 的感想；读者来信；WWDC 短评；主题是软件测试。 相关链接 PFU HHKB 日文版网站 Reverse Polish notation（逆波兰表示法） Rio 关于 Unicode 的笔记 ISO/IEC 2022 编码 对于 Windows 字符串操作的简单介绍 镍过敏 WebObjects Penetration test（穿透测试） Smoke testing（发烟测试） ISO 9000 瀑布模型 敏捷软件开发 测试驱动开发（TDD） Cucumber 恐怖谷理论 使用蒙特卡洛算法的 Zen 围棋程序 Kent Beck 单元测试框架列表 Doctest 人物简介 Rio：《IT 公论》主播，IPN 联合创始人，Apple4us 程序员。 吴涛：Type is Beautiful 程序员，《内核恐慌》主播。

吴涛独自主持的一期节目，一小时的内容包括读者反馈和对于计算机编码的简短介绍。 相关链接 Visual Studio Compiler team 在 Build 大会上的演示（可以从 27’20” 开始） William Chen The Talking Machines Chinese Restaurant Process 人物简介 吴涛：Type is Beautiful 程序员，《内核恐慌》主播。

读了几封听众来信，评论了几条新闻之后，虽然嘴上说不要再讲微软，节目还是很诚实地讨论了这次微软开发者大会。 勘误：格里高利历与儒略历实际上是不同的。 相关链接 Snappy 进入 Ubuntu Desktop NoTCP Dart (Sky) for Android Windows 10 versions Visual Studio Code Microsoft Build 2015 Sessions 人物简介 Rio：《IT 公论》主播，IPN 联合创始人，Apple4us 程序员。 吴涛：Type is Beautiful 程序员，《内核恐慌》主播。

Rio 缺席，如一代班。嘉宾四位，六方合谈。软核主题，中文排版。评议标准，臧否规范。谈笑即罢，尽欢而散。 相关链接 中文排版需求（草案） 陈奕钧制作的「汉字标准格式」 Type is Beautiful JIS X 4051 日本語組版処理の要件 Richard Ishida 董福兴：简单做好中文排版 IT 公论 №67: 小林章《西文字体》译者刘庆（Eric Liu）谈字体排印 IT 公论 №88: 思源黑体（Source Han Sans）——史诗级中日韩新字体诞生 IT 公论 №119: 用 activism 的精神做电子出版标准化 人物简介 吴涛：Type is Beautiful 程序员，《内核恐慌》主播。 梁海：字体及语言爱好者，多语言字体技师。 董福兴：Wanderer 创始人，大块文化出版数位内容事业部开发总监。 陈奕钧：「汉字标准格式」作者，专门研究偏门 web 排版 hack。 刘庆：Type is Beautiful 作者，《西文字体》译者、《字体故事》联合译者。 不鸟万如一：《IT 公论》主播，字节社创始人。

多次提及的消极姐和我们一起聊了聊数据可视化与交互设计，当然一如既往地夹杂着许多其他离题万里的讨论，包括建筑师、建筑史、北京城墙、僵尸片、星战观片的最佳次序、设计师怎样编程，以及消极的若干屠龙之技。 相关链接 消极姐的 blog 中国城市空气污染状况 Newman 的美国选举地图 How to Lie with Maps 纽约客封面《View of the World from 9th Avenue》 经济学人封面《How China sees the world》 郎香教堂 关于纽约排字工人罢工的报道 Pruitt–Igoe 项目 天子大酒店 消极姐在 Quora 上对于 Why don’t more desingers code? 问题的回答 Elevator Pitch 《群尸玩过界》，IMDb Machete order Star Wars: The Force Awakens Official Teaser #2 Frank Gehry The Mother of All Demos 人物简介 Rio：《IT 公论》主播，IPN 联合创始人，Apple4us 程序员。 吴涛：Type is Beautiful 程序员，《内核恐慌》主播。 陈晓霁：微软 Xbox 用户体验设计师。

正音班的废除；关于捐款的一些评论；Ducati Scrambler；听众来信选读；I Like Rabbits 网站 的意义；苹果为什么要收购 Foundation DB。 主题是「编程语言中类型系统的概念及作用」。 相关链接 舒克和贝塔历险记 Ducati Diavel 《码头风云》（On the Waterfront） SAS Contract research organization The Incredible Machine Apache Spark FoundationDB Type System 千年虫 2038 问题 闰秒 What Every Computer Scientist Should Know About Floating-Point Arithmetic Operator overloading 诡异的 JavaScript 运算符重载 Strong and weak typing Dynamic programming language 10 Myths of Enterprise Python Boxing Ruby Open Classes 人物简介 Rio：《IT 公论》主播，IPN 联合创始人，Apple4us 程序员。 吴涛：Type is Beautiful 程序员，《内核恐慌》主播。

《内核恐慌》开放了捐款页面。吴涛和 Rio 先是回味了上一期的辉煌（如果还没有听请赶紧先去听），然后聊了包括新 MacBook 在内的其它一些事情，最后讨论了编程之中并发和并行的概念，相关的几种处理模型，以及异步模式。 相关链接 The IT Crowd | 0118 999 881 999 119 7253 REPL iPython Pry Smalltalk 开发环境 Squeak 三进制计算机 Nim USB Typewriter Rob Pike 关于并发的演讲幻灯片：Concurrency is not Parallelism Windows 3.2 Dining philosophers problem Actor Model 编程中的「副作用」 Communicating Sequential Processes libuv Seven Concurrency Models in Seven Weeks 协程 Erlang: The Movie Erlang: The Movie II 人物简介 Rio：《IT 公论》主播，IPN 联合创始人，Apple4us 程序员。 吴涛：Type is Beautiful 程序员，《内核恐慌》主播。