IT 从业者的必读“启示录”：软件开发的世界末日

编者按：软件越来越庞大，日益蚕食世界。但是在计算硬件指数性发展了几十年的时间里，软件的开发方式却基本保持不变。随着软件变得越来越庞大，对关键系统的渗透越来越深入，软件正在积累着越来越高的风险，我们如何才能排除那些看不见的定时炸弹，避免软件给世界带来末日呢？《大西洋月刊》的一篇长文对此进行了分析。本文较长，请保持耐心。

2014年4月10日晚上，整个华盛顿州的911服务断了6个小时。打电话求助的人听到的都是忙音。当一个陌生人试图闯入自己家时一位西雅图的女性至少拨打了37次911都没打通。后来那人从窗户爬进了客厅，她拿起了一把菜刀那人才逃走了。

那次911服务中断是当时有报道最大的一次，原因后来被追查到科罗拉多Englewood市一台服务器的软件上。该服务器由系统提供商Intrado运营，上面保存了一个计数器，记录的是路由给全美911调度员的呼叫数。Intrado的程序员给这个计数器设置了一个阈值上限。他们选择的数字是100万。

4月10日午夜过后不久，该计算器就超过了这个数字从而引发混乱。因为这个计数器是用来给每个电话生成唯一标识的，所以新的来电都被拒绝了。同时由于这些程序员并没有预计到会出现这样的问题，他们并没有设置告警来唤起注意。没人知道发生了什么事情。服务着1100万的美国人的华盛顿州、加州、佛罗里达州、卡罗莱纳州以及明尼苏达州的调度中心，努力想要弄清楚呼叫者收到忙音究竟是怎么回事。结果直到早上他们才意识到罪魁祸首是Intrado的软件，而补救措施只需要改变一个数字。

不久前紧急呼叫还是在当地处理的。这样的话中断也是小规模的，而且容易诊断和修复。手机的崛起以及新能力带来的希望——比如发短信给911或者发视频给调度员等——推动着依赖于互联网的更复杂系统的开发。结果就是有史以来第一次出现了全国性的911中断。现在这么多年来已经出现过4次了。

有个说法是软件正在“蚕食世界”。一度由机械或者人工控制的关键系统越来越依赖于代码。也许没有比2015年的那个夏天更清楚表明这一点的案例了，因为离港系统出了问题，联合航空公司的飞机被迫停飞；纽约证交所在系统升级后交易被挂起；华尔街日报网站的首页崩溃；西雅图的911系统再次宕机，这次是因为另一个路由器出了问题。这么多软件同时失效让人一度以为这是一次联合的网络攻击。但更令人感到害怕的是随后大家才意识到这些都是巧合。

研究软件安全达35年的MIT航空工程教授Nancy Leveson说：“我们做机电系统的时候往往会想尽一切办法去进行测试。”因为软件错误导致6位病人死亡的放疗机器Therac-25的报告就是她做的。“我们往往会考虑设备能够做的所有事情，会进入的所有状态。”比方说，控制铁路平交道列车运动的几点联锁的配置就那么多，几页纸就能把整个系统描述清楚，而且你可以把每种配置都实际跑一遍来看看会发生什么。一旦做好测试好之后，你就可以清楚知道在处置的是什么。

软件就不同了。只需编辑文件里面某处的文字，同一块硅晶就可以变成自动驾驶仪或者库存管理系统。这种灵活性既是软件的奇迹，也是它的诅咒。因为可以廉价地改变，所以软件总是在变；同时因为它跟现实的一切都是脱钩的——所以占据相同空间的程序可以比另一个复杂上千遍——软件往往会不受束缚地发展下去。Leveson写道：“问题在于我们在尝试建立超过自己管理能力范畴的系统。”

软件完全按照我们的指示行事。软件失败的原因在于我们告诉它做了错误的事情。

关于工程失败我们标准的思维框架是在二战后不久形成的（在软件出现之前，针对机电系统）。其想法是通过把部件做得可靠（比如引擎可承受40000次起飞与降落周期）以及为那些部件故障做好预案（准备2个引擎）来把东西做得可靠。但软件不会坏掉。Intrado的错误阈值不像导致飞机失事的缺损铆钉。软件完全是按照人的吩咐行事的。实际上软件执行得非常完美。它失败的原因在于它被告诉做了错误的事。软件失败是理解的失败以及想象的失败。Intrado其实是有个备份的路由器的，如果能自动切换过去的话，几乎马上就能恢复911服务。但“当时发生的情况是应用逻辑并没有要执行自动修正行动。”

这就是通过代码而不是实体做东西的麻烦。如Leveson总结那样：“复杂性是肉眼看不见的。”

现在正在进行的改变软件制作方式的尝试似乎都始于同一个前提：代码实在是太难琢磨了。那么在试图理解这些尝试之前，弄清楚为什么会这样是值得的：是什么让代码对大脑那么陌生，跟之前的东西那么不一样呢？

技术进步往往会改变世界的样子——你可以看着道路铺设下去，你可以看到天际线的崛起。但在今天你很难说出什么东西进行着了再造，因为这些东西经常是由代码重构的。比方说，当你踩了汽车油门时，你不再直接控制任何东西；脚踏板与风门之间并没有机械连接。相反，你只是给软件提交了一条命令，给引擎补充多少空气是由后者决定的。汽车就是你可以坐进去的计算机。方向盘和踏板一样可以是键盘的按键。

跟一切其他东西一样，汽车也被计算化以促进新功能。当一个程序负责风门和刹车时，在你距离另一辆车太近时它可以放慢车速，或者控制燃油喷射来帮助你省油。当它控制转向器时，它可以在你开始漂移时保持在自己车道内，或者引导你进入停车区。没有代码你实现不了这些功能。你可以试试，没有代码的汽车就会变成庞大的、重达40000磅但无法移动的发条装置。

软件让我们做出了有史以来最复杂的机器。但是我们几乎都没注意到，因为所有的复杂性都被包裹进小小的芯片里面以及数百万行的代码之中。但仅仅因为我们看不见复杂性并不意味着它就没有了。

著名的荷兰计算机科学家Edsger Dijkstra在1988年曾经写到：“必须思考一个头脑此前从未面临过的概念层级。” Dijkstra把这当成一种警示。随着程序员热切地想要把软件植入到关键系统当中，软件日益成为建造世界的关键——Dijkstra认为他们已经高估了自己。

软件工程师并不理解也不关心自己试图解决的问题。

变成之所以如此困难是因为它需要你像计算机一样思考。在计算的早期这种陌生感会更加鲜明一点。当时的代码还是0、1的形式。跟这些枯燥数字打交道的程序员与其实际要解决的问题距离实在是太疏远了。你不可能看出他们是在计算火炮轨迹还是在模拟井字棋游戏。像Fortran、C这样的编程语言以及“集成开发环境”的引入尽管有所改变，但却掩盖了这种基本的异化——事实上程序员并不直接解决问题，而是把时间花在给机器编写指令上面。

MIT软件安全专家Leveson说：“问题在于软件工程师并不理解也不关心自己试图解决的问题。”原因在于他们太过埋头于让自己的代码可以工作了。她说：“软件工程师喜欢为编码错误提供各种工具。”她指的是IDE。“但软件出现的严重问题其实跟需求有关，跟编码错误无关。”比方说，当你写代码控制汽车的风门时，重要的是何时以及如何打开风门打开多大的规则。但这些系统已经变得太过复杂，任何人脑子里都记不住所有东西。Leveson说：“汽车的代码现在已经超过了1亿行，你无法预料所有的事情。”

2007年9月，Jean Bookout载上自己最好的朋友开着一项丰田凯美瑞正行驶在高速公路上，突然油门好像被卡住了一样。她抬脚松开油门，汽车并没有放缓；她试着踩刹车，但却似乎失去了动力。当她以50英里的时速转入匝道时她踩下了紧急刹车。车子划出了一道150英尺长的滑痕然后撞上路边的路堤。乘客在这次事故中死亡。Bookout一个月后才从医院中醒来。

这次事故是众多对丰田汽车所谓的突然加速诉讼案中的一起。丰田把事故原因归咎于垫布的糟糕设计、踏板的“粘性”以及司机错误身上，但局外人怀疑该负责的应该是软件瑕疵。美国国家公路交通安全管理局征召了NASA的软件专家来对丰田的代码进行严密的审核。在将近10个月后，NASA仍未发现软件是事故原因的证据——但同时他们也说自己无法证明软件不是。

后来有人终于在Bookout事故的诉讼过程中找到了其中令人信服的关联。原告方的鉴定证人Michael Barr有一个软件专家团队花了18个月的时间来研究丰田的代码，捡起了NASA丢下来的东西。Barr把他们发现的东西称为是“面条式代码（spaghetti code，多页嵌套的if语句与for循环，包含大量复制-粘贴的过程代码，且没有合适的分割）”。如果代码一项功能一项功能地堆积起来共生了很多年的话就会变成纠缠不清无法跟踪，跟不用说进行穷尽测试去追查缺陷了。

如果软件失灵了也是由同样一套程序处置的话，则这套程序是无法胜任的。

Barr的团队利用同款凯美瑞证明了其实车载计算机有超过1000万种方式导致突然加速事故。他们证明了只需一位的翻转（从0变成1或者从1变成0）就能让汽车失去控制。丰田的自动防故障代码不足以阻止这一点。Barr作证说：“你让软件看管软件。如果这个软件失灵了还是由同一套程序或者应用来挽救局面的话是难堪此任的，因为它已经失效了。”

Barr的证词为Bookout及其朋友的家庭争取到了300万美元的赔偿。据《纽约时报》，这是针对丰田的诉讼案中首起就电控节气门系统进行的审判，也是丰田首次被发现对突然加速事故负责的案子。后来丰田总共召回了超过900万辆汽车，赔付金额接近30亿美元才了结了相关争端。

软件将来还会面临更多的坏日子。我们今后要更擅长做软件就变得非常重要，因为如果不行的话，随着软件变得越来越复杂以及连接更紧密，随着软件控制了更多的关键功能——今后的日子会变得更加糟糕。

问题是程序员已经很难跟上自己的创造物。自从1980年代以来，程序员的工作方式以及使用的工具几乎都没什么变化。大家逐渐开始担心这种情况难以为继。微软的IDE工具Visual Studio首席软件开发者Chris Granger说：“即便是非常好的程序员对自己的系统理解起来也很困难。” Granger在微软的时候曾经安排过一次对Visual Studio的端到端研究。这是他唯一完成过的一次类似研究。他用了1个月的时间在单面镜背后观察大家是怎么写代码的。“这些人怎么用工具？如何思考？如何坐在计算机前，有没有碰鼠标？所有这一切都有教条但并没有经过经验测试。”

发现令人吃惊。他说：“Visual Studio是全世界最庞大的单一软件之一。它的代码超过了5500万行。我在研究中发现其中98%都是不相干的。也就是说大部分的代码都没有针对大家面临的根本问题。我的最大感受是基本上大家就是在脑子里玩计算机。”程序员就像棋手下盲棋一样——其思维精力都放在想象拼图在什么地方上了，以至于已经没有精力再去思考比赛本身。

过去40年计算机每18个月就能力翻番。为什么编程却一点都没有改变？

John Resig在自己的学生身上也注意到同样的事情。Resig是著名的JavaScript（有一半网站都是JS编写的）程序员，也是在线教育网站可汗学院的技术领导。2012年初的时候，他一直在纠结于网站的计算机科学课程。为什么学编程就这么难呢？根本问题似乎在于代码太过抽象了。开发软件不像用冰棍棒造桥，你可以看清楚冰棍，可以触摸粘胶。要想“造”程序，你得敲字。当你想改变程序（无论是游戏、网站或者物理仿真）的行为时，你改变的其实是文字。所以程序写得好的学生是那些可以将代码在脑子里过一遍，像计算机一样思考，能跟踪每一次中间计算的人。Resig像Granger一样，开始猜测编程是不是就得这样。过去40年计算机每18个月就把能力翻番。为什么编程却一点都没改变？

这两个人同时在相同情况下思考同一个问题并不是偶然。两人都看了同一场演讲，那是计算机研究学者Bret Victor个软件工程学生准备的。演讲在2012年2月被放到网上之后火了，它做出了两个大胆的判断。第一是我们写软件的方式基本上已经坏掉了。其二是Victor知道该怎么修正。

Bret Victor不喜欢写代码。他说：“这听起来很怪异。当我想要做东西，尤其是想用软件做东西时，我得排除这种天生的厌恶感，因为我操纵的不是我想做的东西，我只是在文字编辑器写一堆的文字。”

“我有着相当强烈的信念认为这么做是错的。”

40岁的Victor思维敏捷但为人害羞，有着David Foster Wallace的风采。尽管他管理着一个研究未来计算的实验室，但相对于技术他似乎对利用技术的人的脑子更感兴趣。就像任何好的工具制造者一样，他会从技术和人性的角度去审视这个世界。在那次令他一举成名的演讲上，Victor提出了他的发明原则：“创作者需要跟所创造的东西有直接关联。”编程的问题正是违背了这一原则。所以软件系统会如此难以琢磨，出现的bug会如此这多：程序员从写的第一页文字开始就是跟要做的东西是脱节的。

他说：“我们当前对计算机程序的概念是直接源自上世纪50年代的Fortran和ALGOL语言。那些语言是针对穿孔卡片设计的。”现在C或者Java等语言的代码都是屏幕上的字符形式而不是一摞打洞卡片，但还是像过去一样死气沉沉，还是一样的不够直接。

在Victor看来，盯着文字编辑器来理解癌症的做法是可怕的。

文字处理有一种类比。过去你在编写文档程序里面看到的就是文字本身，要想改变布局或者字体、边距，你得写特殊的“控制码”，或者告诉计算机“这部分文字应该是斜体字”这样的命令。麻烦的是除非你把文档打印出来否则是看不到效果的。你很难预测自己会得到什么。你必须想象代码如何被计算机解释——也就是说，你必须在脑子里运行一遍。

然后就出现了WYSIWYG（所见即所得）。当你把一段文字标记成斜体时，屏幕上的文字也会相应倾斜。如果你希望改变边距，你可以直接拖动屏幕顶部的标尺——然后看到改变的效果。文字因此感觉就像是真的，可以随便摆弄的东西。只需要看着你就能知道自己有没有做错。任何人只要能在页面上点击都能对复杂系统——文档布局以及格式引擎——进行控制。

Victor的观点是编程也应该如此。在他看来，像设计自适应巡航控制系统或者试图理解癌症这样的重要工作靠盯着文本编辑器看来完成是可怕的。确保有朝一日不需要这样做是程序员的恰当工作。

这个并不是什么疯狂的想法。因为有不少先例。比方说Photoshop把强大的图像处理算法交到了甚至不知道算法是什么的用户手中。这是一款非常复杂的软件，但那种复杂就像合成器式的复杂，上面有开关旋钮、按键、滑块等，用户可以像玩乐器一样去学习。Squarespace做了一款工具让用户只需点击就能建立网站，而不是用HTML和CSS写代码。它已经强大到可以做一度只能由专业web设计师才能完成的工作。

但这只是一小部分例子。压倒一切的现实是，当有人想要用计算机做点有趣的东西时，他们基本上都必须写代码。身为理想主义者的Victor对此的看法是这不是什么机会，而是大多数程序员的道德沦丧。他的演讲就是战斗号角。

演讲的核心是一系列试图表明现有针对各种问题（电路设计、计算机动画、调试算法）的工具究竟有多原始的演示，同时也展现了更好的工具可能的样子。够讽刺的是，抓住了每个人的想象的一个演示却是看起来最为微不足道的一个。演示展示了一个分屏，左边是类似超级玛丽的游戏，右边是控制游戏的代码。随着Victor改变代码，游戏世界里面的东西也会发生变化：他减少了一个数字，也就是重力的强度，然后马里奥的角色就漂浮起来了。他增加了另一个数字，也就是玩家速度，然后马里奥就会疾驰而过。

假设你想给游戏设计一关，让主角跳上一只乌龟然后反弹出去。过去游戏程序员往往要分两阶段解决这类问题：首先，你盯住控制马里奥如何跳跃、跑得多快、乌龟弹性如何的代码，然后在文字编辑器进行一些修改，用你的想象力来预测会是什么效果。然后你重放游戏来看看实际会发生什么。

Victor希望可以更加直接一点。他说：“如果你有一个及时的流程（指的是马里奥过关的路径），并且想马上看到变化情况，你得把时间映射到空间。”他点击了一个按钮，上面显示的不仅是马里奥现在在哪里，而且也会显示出未来每一刻的位置。此外，这条预测路径还是反应式的：当Victor改变游戏参数（通过拖拽鼠标完成）时，路径的形态也会跟着变。就好像拥有了游戏的上帝视角。整个问题已经简化为玩弄不同的参数，就好像调整立体收音机的旋钮一样，直到你让马里奥完成工作。有了合适的界面，你几乎都不用跟代码打交道，而是直接操纵游戏的行为。

观众第一次看到这个时都赞叹不已。他们知道自己看到的不是小孩的游戏，而是这个行业的未来。大多数软件都牵涉到以复杂的方式展现出来的行为，Victor已经表明如果你想象力足够的话，就可以开发出手段来看到那种行为并且改变它，就好像自己动手一样。一位看过这次演讲的程序员随后写到：“突然之间我所有的工具都感觉过时了。”

当John Resig看到这场演讲时，他把自己给可汗学院转变的编程教程给废弃了。他希望网站的编程练习能够像Victor的演示一样工作。左手边会是代码，右手边则是运行的程序：这可以是一幅图画，一场游戏，或者一次仿真。如果你改变代码，它马上就会改变画面。Resig这样描述这个方案：“在一个真正响应式的环境里，你可以彻底改变学生学习编程的方式……他们可以马上看到结果，并且在没有明确解释的情况下凭直觉了解到底层系统固有的内在运作方式。”可汗学院已经成为全世界最大的计算机编程课，每个月平均有100万用户在积极地使用这个程序。

在微软做Visual Studio的Chris Granger也受到了鼓舞。在看到Victor演讲视频的那段日子里，他开发了一个新的编程环境原型。其关键能力是可以马上对程序的行为提供反馈。你可以在控制系统的代码旁边看到系统是怎么做的。这就好像是脱掉了眼罩。Granger把这个项目叫做“Light Table”。

2012年，他在Kickstarter上面为Light Table筹集资金。项目在编程界引起了轰动。在一个月的时间里，项目就募集到了20多万美元。这个想法传播出去了。现场感（liveness）的概念，也就是马上就能看见数据流经程序的情况，随后变成了Google、苹果旗舰编程工具的功能。iPhone和Mac的默认开发语言Swift是苹果为了支持名为Playground的环境而从头开始开发出来的，这门语言正是直接受到了Light Table的启发。

但在看到自己的演讲最终产生的影响之后，Bret Victor的希望破灭了。他后来说：“很多东西似乎误解了我说的话。”当大家邀请他出席会议讨论编程工具时，他知道情况不对头了。他说：“每个人都以为我对编程环境感兴趣。”其实他感兴趣的是大家如何看待和理解系统——如他所概括那样，是“动态行为的直观表现”。尽管代码日益成为创建动态行为的工具选择，但仍然是理解行为最糟糕的工具之一。“发明原则”的要点是要表明你可以通过在系统行为与代码之间建立直接联系来缓解这一问题。

我不敢肯定代码是否一定要存在。

在随后的两场演讲“停止画死鱼”以及“画动态可视化”中，Victor又深入了一步。他演示了两个自己开发的程序——第一个是给动画家准备的，第二个是给试图可视化自己数据的科学家准备的——这两个过去都需要写很多定制代码但现在被简化为WYSIWYG（所见即所得）界面。Victor认为同样的做法几乎可以应用到编写代码解决的每一个问题上面。他说：“我不敢肯定代码是否有存在的必要。或者至少软件开发者有存在的必要。”在他看来，软件开发者的恰当角色是创建工具来消除对软件开发者的需要。只有这样有着最紧迫计算问题的人才能直接把握这些问题而不需要以代码为中介。

当然，为了做到这一点，你得让程序员本身买账。Victor在最近的一篇论文中恳求专业软件开发者不要再把自己的天才浪费到开发Snapchat以及Uber这样的app上。他写道：“日常生活的便利性不是重大问题。”相反，开发者应该把关注点放到科学家和工程师身上——“那些人做的工作才是重要的，而且更关键的是，他们使用的工具真的非常的糟糕。”他还写道，像这类令人激动的工作，尤其是一类“基于模型设计”的工具已经在开发当中，而且进行了好几年了，但大多数程序员对此一无所知。

“如果你看看自己手上所有的工业用品，包括你自己用的，公司用的，里面唯一不是工业的东西就是代码。” Eric Bantégnie 是Esterel Technologies的创始人，这家法国公司做的是开发安全关键软件的工具。像Victor一样，Bantégnie并不认为工程师应该靠往IDE呼入几百万行代码来开发大型系统。他说：“没人想要手工造一辆车。代码是在很多地方还是手工作坊。如果只是人工敲10000行代码还可以。但有些系统有3000万行代码，比如空客，或者1亿行代码，如Tesla或高端汽车——这些系统就变得非常非常复杂了。”

Bantégnie的公司是业界利用基于模型的设计的先驱之一，有了这种工具你不再需要直接编写代码。相反，你创建的是一种描述程序应该遵循的规则的流程图（“模型”），然后计算机会基于那些规则替你生成代码。比方说，如果你要给电梯做控制系统，规则之一可能是当门打开时，有人按下去大厅的按钮时，你应该关上门，然后开始移动电梯。在基于模型的设计工具里，你会用一张小小的图来表示这条规则，就好像在白板上画出这条逻辑一样，做出代表不同状态——如“门打开”、“移动”、“门关闭”等的方框，以及定义如何从一个状态转移到另一个状态的线段。这种图解使得系统规则变得明显：只需看着它你就能看到让电梯移动的唯一办法就是关上电梯门，或者唯一让门打开的办法是让电梯停下来。

大家知道怎么写代码。问题是该写什么代码。

但这还没到Photoshop那种效果。当然，Photoshop的魅力在于你在屏幕上操纵的图画是最终产品。相比之下，在基于模型的设计中，你在屏幕上的图画更像是蓝图。尽管如此，用这种办法做软件就定性而言仍然跟传统编程有着很大的不同。在传统的编程中，你的任务是将复杂规则转换成代码；你大部分的精力都换在进行这种转化上，而不是考虑规则本身。而在基于模型的方法中，你拥有的全部就只有规则。所以这就是你要花时间考虑的。这样一来你关注机器就会少一点而把更多的焦点放在试图让它解决的问题上。

Bantégnie说：“通常软件编码的主要问题——我本人也是编码者——并不是编码者的技能。这些人知道如何去编写代码。问题在于要编写什么代码。因为大多数需求都属于自然语言，是含糊的，一个需求是永远也无法做到极端精确的，写代码的人往往会有不同的理解。”

按照这种看法，软件就变成难以驾驭的了，因为媒体描述软件应该做的事情——会话、文字描述、在纸上画画——这些事情跟媒体描述的软件能做的事情，也就是代码本身太不一样了。从一边到另一边中间丢失的东西太多了。基于模型的设计这一想法的背后就是想填补这一鸿沟。表达自己需要什么的系统设计师以及自动生成代码的计算机采用的都是同一个模型。

当然，这种办法想要成功的话，有很多工作都需要在项目甚至还没开始前就得完成。得有人首先开发工具来建立大家习惯的模型——那种就像自己平时做的笔记和草图一样的模型——但同时计算机理解起来也不会产生歧义。他们必须开发出一款程序将这些模型变成真正的代码。最后他们还得证明生成的代码永远都会做它们该做的事情。Bantégnie说：“开始20年的后台工作让我们受益匪浅。”

2012年被ANSYS收购的Esterel Technologies诞生于1980年代，当时的法国核工业和航空业越来越难以避免bug的问题，因为担心关键性安全代码复杂性问题膨胀而开始了这方面的研究。达索航空的科研负责人Emmanuel Ledinot说：“我是从1988年开始的。那时候，我在做军用航电系统。负责系统集成以及调试的人注意到bug的数量在上升。”1980年代机载计算机的数量出现了飙升，每架飞机上的计算机已经由单台变成了10几台，每一台计算机分别负责控制、导航以及通信相关的、高度专业化的任务。当来自传感器的数据涌入以及飞行员输入指令时协调这些系统控制飞行需要演奏交响乐般的完美反应。Ledinot说：“在合适的时机按照合适的次序处理上百乃至上千的可能事件被认为是bug膨胀的主要原因。”

Ledinot由此认定手工编写如此复杂的代码已经难以为继。代码究竟在做什么事情已经太难以理解了，想要验证它是否正确工作几乎是不可能的。为此他要寻找新的东西。他在一次演讲中说：“你必须理解在像这样的过程中更换工具是极其昂贵的。除非你已经无路可退，否则是不会做出这种决定的。”

大多数程序员喜欢代码。至少他们理解代码。

他开始跟法国计算研究中心INRIA的计算机科学家Gerard Berry合作开发Esterel，这个名字在法语里面是“实时”的合成词。Esterel背后的想法是传统编程语言也许擅长描述按照预定次序进行的简单过程——比如烹饪法——但如果你试图用到大量事件近乎实时以任何次序并发的系统（比如飞机驾驶舱）上面时，就会不可避免地陷入混乱。而控制软件发生混乱是危险的。Berry在一篇论文中甚至预测“低级编程技巧对于大型关键性安全系统来说将是不可接受的，因为它们会导致行为理解和分析几乎不可行。”

Esterel的目的是让计算机替你处理这种复杂性。这就是基于模型的方案的希望所在：你不再需要编写一般的编程代码，而是建立系统行为的模型——在这个例子里面，模型关注的是独立事件应该如何处置，如何确定事件的优先次序，哪一个事件依赖于其他的事件等等。模型变成了计算机用来进行实际编程的详细蓝图。

Ledinot和Berry 用了整整10年的时间晚上Esterel使之可用于生产。说：“2002年我们有了第一个可自动生成代码的操作型软件建模环境，并且为阵风战斗机生成了第一个嵌入式模块。”今天，ANSYS SCADE产品族已经被广泛应用到航空、国防、核电、交通、重工业、医疗设备等行业的代码生成当中。Esterel Technologies创始人Bantégnie说：“我最初的梦想是让SCADE生成的代码遍布全世界每一架飞机上，现在我们距离这个目标已经不太远了。”包括控制飞机飞行操纵面的系统在内，空客A380几乎所有的关键性安全代码都是由SCADE生成的。

我们早已经知道如何让负责软件变得可靠，但在太多的地方我们都选择不这么做。

就像Bantégnie解释那样，让计算机而不是人把你的需求变成代码的美妙之处在于你可以确保生成的代码满足那些需求（其实你可以用数学证明这一点）。基于模型的方案大部分好处来自于在能够实时添加需求的同时确保原有需求得到满足；每一次变更计算机都能验证程序仍然有效。你可以随便调整蓝图而不怕引入新的bug。用FAA的话来说，你的代码是可以“在建构的时候修正的”。

尽管如此，大多数软件都用传统的方式开发的，甚至在痴迷于安全的航空界也是如此，工程师要写好自己的需求，然后再由程序员用C这样的语言写成代码。正如Bret Victor在论文中表明那样，相对而言基于模型的设计是不同寻常的。Shivappa说：“FAA的很多人认为代码生成是魔术，因此要求进行更严格的审查。”

大多数程序员也是这种想法。他们喜欢代码。至少他们理解代码。替你写代码并验证其正确性的工具利用的是数学的“有限状态机”以及“递归系统”，这些东西如果说不是好得令人难以置信的话，那就是晦涩难懂且很难使用。

这种事情以前也发生过。只要编程稍微远离写0、1一步，反对声音最响亮的都是程序员。参与阿波罗计划的著名软件工程师Margaret Hamilton（“软件工程”这个术语就是她发明的）说，1964年在MIT的Draper实验室的第一年时，她记得有一次会上一个派别的人跟另一派就从“非常低级的机器语言”过渡到更高级的汇编语言的事情吵个不停。“最底层的人拼命想要保留这种语言。他们的观点都很相似：‘谁知道汇编语言能不能做好啊？’”

她说：“一边的家伙吵得面红耳赤，开始大喊大叫起来。”表示自己对“这帮人情绪化如此严重感到吃惊。”

你可以不停地做测试，但永远也无法找完所有的bug。

达索航空的Emmanuel Ledinot指出，在汇编语言被至今仍流行的语言如C等逐步淘汰的时候，持怀疑态度的却变成了使用汇编语言的那帮人。毫不奇怪，“朝着基于模型的软件开发转变并不容易：他们感觉可能这会又一次失去控制，甚至比已经发生的情况还要糟糕。”

基于模型的设计有时候又被称为模型驱动工程（MDE），面前仍面临着根深蒂固的偏见，据一篇最近的论文，“一些人甚至认为调查大家对MDE的看法甚至比研究新的MDE技术的需求还要强烈。”

这听起来似乎是个笑话，但对于基于模型方案的支持者来说，这是很重要的一点：我们已经知道如何让复杂软件变得可靠，但为什么在那么多地方我们都选择不这么做呢？

2011年的时候，Chris Newcombe已经在Amazon工作了将近7年，并且已经晋升为首席工程师。公司的一些最关键的系统，包括零售产品目录以及管理全世界每一台Kindle设备的基础设施等他都有参与。他是备受赞誉的AWS（Netflix、Pinterest、Reddit等都在上面托管）团队的一名领导。在Amazon之前，他帮助建立了全球最大在线游戏服务Stream的骨干。他是悄悄维持互联网运转的工程师之一。他做过的产品被认为取得了大规模的成功。但他一直都在担心那些系统的设计会成为一颗颗带来灾难的定时炸弹。

他在一篇论文中说：“在估计规模达每秒数百万请求的系统‘极其罕见’的事件组合的可能性方面，人类的直觉非常糟糕。人类的易错性意味着其中一些更微妙、更危险的bug原来是设计过程犯的错；代码只是忠实地履行设计想让它干的事情，但设计未能正确地处理一种特别“罕见的场景”。

Newcombe确信，真正关键系统——比方说存储很大一部分web数据的系统——背后的算法应该不仅仅要好，而且要做到完美。哪怕一个细微的bug有可能是灾难性的。但他知道找到bug有多困难，尤其是当算法变得越来越复杂的时候。你可以把想做的测试都给做了，但永远也无法把所有的bug找完。

很少有程序员在开始编码前绘制自己程序要做什么的草图。

这就是他会对一种数学与代码的奇怪混合感到如此着迷的原因。这个东西看起来跟代码很像，它会把算法用“TLA+”来进行描述。令人感到惊奇的地方在于这种描述据说在数学上是精确的：用TLA+编写的算法正确与否原则上是可以证明的。实际上，它可以让你建立问题的现实模型，而且进行的测试不仅是彻底的，甚至可以说是穷尽的。这就是他一直在寻找的东西：一种能写出完美算法的语言。

TLA+的意思是“行为时序逻辑（Temporal Logic of Actions）”，其内涵跟基于模型的设计类似：这是一门记录需求的语言——TLA+称之为计算机程序的“规范”。这些规范然后可以由计算机进行完全验证。也就是说，在编写任何代码之前，你就先写出了程序逻辑的简版大纲，以及需要它满足的约束（比方说你要给ATM编程，约束可能是永远也不能撤销账户的同一笔钱超过2次。）。TLA+然后再穷尽检查逻辑的所有可能性是否均满足那些约束。如果不能满足，它会展示违背约束的情况究竟是什么样的。

这门语言是由图灵奖得主Leslie Lamport发明的。现在微软研究院就职的他是“分布式系统”理论的先驱之一。其工作为现代web的众多系统奠定了基础。

在Lamport看来，今天的软件bug那么多的一个主要原因是程序员直接就跳到写代码这一步了。他在一篇文章中写道：“架构师在砌第一块砖，钉第一颗钉子之前要先画好详细规划图。但很少有程序员会在写代码之前画程序应该做什么事情的草图。”程序员着迷于编码的具体细节，因为代码才是让程序变活的关键；把时间花在任何其他地方似乎都属于分心。而且苦思冥想代码的微观力学还能带来耐心的愉悦，一种沉思的满足感。但Lamport认为，代码永远都无法成为思想的媒介。他说：“当你用编程语言进行思考时，你的思维能力其实是受限的。代码会让你只见树木不见森林：它把你的注意力吸引到单个组件上面，而不是程序拼凑出来的更大图景，或者它应该要做的事情——以及它是否按照你的想法做。”所以Lamport才要创建TLA+。就像基于模型的设计一样，TLA+把你的注意力集中在相同的高级结构、基本逻辑上面，而不是实现那些东西的代码上。

Newcombe极其在Amazon的同事还将继续用YLA+来寻找重要系统里面细微但关键的bug，包括被认为是全球最可靠的存储引擎S3背后核心算法里面的bug。现在它已经在这家公司内部得到广泛使用。在这个曾经使用过TLA+的人组成的微小世界里，他们的成功算不上不同寻常。微软的一位实习生用TLA+找到一个可能会导致每一台Xbox在使用数小时后崩溃的bug。欧洲太空总署的工程师用它来重写了一个人类首次软着陆彗星的探测设备的操作系统，而且代码量还只是原来的1/10。英特尔用它来定期校验自己的芯片。

不过TLA+只占据了远离主流的小小一个角落，如果说它的确有一席之地的话。即便对于像Newcombe这样经验丰富的工程师而言，这门语言一开始读起来也是非常的离奇难懂——这完全就是符号的大杂烩。在Lamport看来，这是教育的失败。尽管编程诞生自数学，但此后基本上已经与之分道扬镳。大多数程序员对那种数学——逻辑和集合论都不是很熟悉，而这正是TLA+所需要的。Lamport说：“很少有程序员理解非常基本的概念以及这些概念如何应用到实践中，甚至连教编程的老师也是如此。要用比编码更高级的思维去精确思考，而数学其实可以让你的思考更家精确，这种想法完全属于异类。因为他们从来都没学过这个。”

我希望如果这些简单的事情都不理解的话就不允许他们写程序。

Lamport这种数学思维的失败视为现代软件开发的问题：其风险在不断攀高，但程序员却没有相应提升自己——他们还没有武装到牙齿，无法应对日益复杂的问题。他说：“在15世纪，大家往往在不知道微积分的情况下建教堂，但现在我并不认为不懂微积分的人还可以去建教堂。我希望经过适当长的一段时间之后，那些不理解这种简单事情的人是不允许写程序的。”

Newcombe就不是很确定程序员应该承担这种责任。他说：“我从Leslie那里了解到他认为程序员害怕数学。我的发现是程序员并没有意识到——或者并不认为——数学可以帮助他们处理复杂性。发砸星是程序员最大的挑战。”他认为让大家使用TLA+的正在问题在于要说服这帮人这不会浪费他们的时间。就一个物种而言，程序员是彻底的实用主义。像TLA+这样的工具散发着象牙塔的臭气。当程序员遭遇“形式化方法”（之所以这么叫是因为涉及到对程序的数学性的、“形式化”的精确描述）时，其根深蒂固的直觉就是退避三舍。

大多数在大学上计算机科学课程的程序员都曾粗略碰到过一些形式化方法。通常会在一些无足轻重的场合进行演示，比如从0开始计数的程序，学生的工作是从数学上证明程序的确是从0开始计数的。

Newcombe说：“我得改变大家对形式化方法的看法。”甚至Lamport本人似乎也没有完全把握住这一点：形式化方法存在着形象问题。解决这一点的办法不在于乞求程序员做出改变——要改变的是你自己。Newcombe意识到要想让TLA+这样的工具成为编程主流，你得开始讲他们的语言。

首先，他说当他向Amazon的同事介绍TLA+时，会避免告诉对方它代表着什么，因为他害怕TLA+的名字会让他们望而生畏：“行为时序逻辑”恰恰就弥漫着学术界的那股自大的光环，但却令大多数程序员感到反感。他还尽量不用“形式化”、“验证”或者“证明”这样的术语，因为这会让程序员想到乏味的课堂练习。相反，他把TLA+包装成了一种新型的“伪代码”，是迈向真正代码的垫脚石，可以让你对算法进行穷尽测试——而这又让你可以在设计过程尽早进行精确地思考。他写道：“工程师是用调试而不是‘验证’的思路进行思考”，所以他把面向Amazon内部进行的讲座题目叫做《调试设计》。Newcombe不是惋惜程序员用代码来看世界的事实，而是主动去拥抱它。他知道否则的话自己就会失去他们。Newcombe说：“我已经看到一堆人说，‘现在我理解了。’”

代码已经制造了一种全新水平的复杂性。同时也让一种新型的失效成为可能。

此后他离开Amazon去了Oracle，在那里接着说服新同事给TLA+一个机会。在他看来，使用这些工具现在已经成为了一种责任。他说：“我们需要更擅长这个。”

“我是自学的，从9岁开始我就开始写代码，所以我的本能是开始写代码。这是我唯一的思考方式：勾勒轮廓，尝试，然后有组织地演变。”在他看来，这是许多程序员至今仍然采用的方式。“他们google，上Stack Overflow”（Stack Overflow是一个流行的编程相关问答网站），“他们寻找解决其战术性关切的代码片段，然后拼凑起来，不断迭代。”

“这种做法无可厚非直到你遇到大麻烦。”

2015年夏，美国的两位安全研究人员Charlie Miller和Chris Valasek认为汽车制造商对软件缺陷并未给予足够的重视，于是他们证明一辆2014款的吉普切诺基可以被黑客远程控制。他们利用了拥有无线连接的车载娱乐系统实际上跟更多的中心系统（比如控制雨刮器、油门、刹车的系统）也有连接这一事实。他们利用业余的时间做出了攻击系统，并且黑掉了记者驾驶的一辆切诺基，让车子失去控制，导致那位记者陷入恐慌。

尽管他们没有动手，但却表明了写出一款更好的软件是有可能的，所谓“汽车蠕虫”可以利用被黑的切诺基车载计算机去扫描和攻击其他的切诺基；如果他们愿意的话，他们可以同时访问全美有漏洞的汽车和SUV。有朝一日可以让所有那些车辆突然把方向盘打左或者在高速行驶时切断引擎。

Valasek说：“我们需要换种思路来审视软件。”汽车企业一直以来都是将成百上千不同供应商生产的零件组装成最终产品。但这些过去一度是纯粹机械化的零件，现在往往都带着好几百万行的代码。尽管其中一些代码——比如自适应巡航控制，自动刹车以及车道保持等的——的确让车辆变得更安全了—，但也制造了全新水平的复杂性。并且使得一种新型的失效变成可能。

在无人车的世界里，软件不能成为事后想法。

Esterel 背后的法国研究人员Gerard Berry说：“汽车存在着大量的bug。它不像航空电子，航空电子对待bug非常认真。并且承认软件不同于机械。”汽车业可能跟很多行业一样尚未意识到自己其实也身处软件业。

在丰田案作证的软件安全专家Michael Barr说：“汽车业缺乏了解软件在做什么的软件安全监管者。”他说NHTSA“只有有限的软件专业知识。”使得基于模型的设计与代码生成对航空业产生吸引力的相同监管压力降临到汽车业身上要慢一些。但达索航空的Emmanuel Ledinot认为这种差异也许还有经济方面的原因。汽车根本无法接受零件成本的增加，哪怕几美分都不行，因为乘上几百万就是个大数字；因此嵌入到汽车的计算机必须缩减到最少水平，这几乎不给尚未调整到精益水平的代码太多的运行空间。“我认为过去10年引入基于模型的软件设计对他们来说代价太高了。”

Ledinot怀疑其诱因也在改变：“我觉得汽车业可能会推进。ISO 26262和汽车业可能会慢慢推进关键部件采用这种方案。”（ISO 26262是2011年发布的汽车安全标准）。Barr的观点也基本一样：在无人车的世界里，软件不能成为事后想法。它不能像今天的机票预订系统或者911系统或者股票交易系统一样搭建。那些代码要对道路上的数亿个生命负责，它必须有效。这可不是小事情。

Gerard Berry在演讲中说：“计算基本上是不可见的。当你的轮胎没气时，你会看见它是瘪的。当你的软件出问题了，你看着软件却什么也看不到。”

“所以这是一个大问题。”

原文链接：https://www.theatlantic.com/technology/archive/2017/09/saving-the-world-from-code/540393/

编译组出品。编辑：郝鹏程。