軟件越來越龐大，日益蠶食世界。但是在計算硬件指數性發(fā)展了幾十年的時間里，軟件的開發(fā)方式卻基本保持不變。隨著軟件變得越來越龐大，對關鍵系統的滲透越來越深入，軟件正在積累著越來越高的風險，我們如何才能排除那些看不見的定時炸彈，避免軟件給世界帶來末日呢？《大西洋月刊》的一篇長文對此進行了分析。本文較長，請保持耐心。

2014年4月10日晚上，整個華盛頓州的911服務斷了6個小時。打電話求助的人聽到的都是忙音。當一個陌生人試圖闖入自己家時一位西雅圖的女性至少撥打了37次911都沒打通。后來那人從窗戶爬進了客廳，她拿起了一把菜刀那人才逃走了。

那次911服務中斷是當時有報道最大的一次，原因后來被追查到科羅拉多Englewood市一臺服務器的軟件上。該服務器由系統提供商Intrado運營，上面保存了一個計數器，記錄的是路由給全美911調度員的呼叫數。Intrado的程序員給這個計數器設置了一個閾值上限。他們選擇的數字是100萬。

4月10日午夜過后不久，該計算器就超過了這個數字從而引發(fā)混亂。因為這個計數器是用來給每個電話生成唯一標識的，所以新的來電都被拒絕了。同時由于這些程序員并沒有預計到會出現這樣的問題，他們并沒有設置告警來喚起注意。沒人知道發(fā)生了什么事情。服務著1100萬的美國人的華盛頓州、加州、佛羅里達州、卡羅萊納州以及明尼蘇達州的調度中心，努力想要弄清楚呼叫者收到忙音究竟是怎么回事。結果直到早上他們才意識到罪魁禍首是Intrado的軟件，而補救措施只需要改變一個數字。

不久前緊急呼叫還是在當地處理的。這樣的話中斷也是小規(guī)模的，而且容易診斷和修復。手機的崛起以及新能力帶來的希望——比如發(fā)短信給911或者發(fā)視頻給調度員等——推動著依賴于互聯網的更復雜系統的開發(fā)。結果就是有史以來第一次出現了全國性的911中斷?，F在這么多年來已經出現過4次了。

有個說法是軟件正在“蠶食世界”。一度由機械或者人工控制的關鍵系統越來越依賴于代碼。也許沒有比2015年的那個夏天更清楚表明這一點的案例了，因為離港系統出了問題，聯合航空公司的飛機被迫停飛；紐約證交所在系統升級后交易被掛起；華爾街日報網站的首頁崩潰；西雅圖的911系統再次宕機，這次是因為另一個路由器出了問題。這么多軟件同時失效讓人一度以為這是一次聯合的網絡攻擊。但更令人感到害怕的是隨后大家才意識到這些都是巧合。

研究軟件安全達35年的MIT航空工程教授Nancy Leveson說：“我們做機電系統的時候往往會想盡一切辦法去進行測試?！币驗檐浖e誤導致6位病人死亡的放療機器Therac-25的報告就是她做的。“我們往往會考慮設備能夠做的所有事情，會進入的所有狀態(tài)。”比方說，控制鐵路平交道列車運動的幾點聯鎖的配置就那么多，幾頁紙就能把整個系統描述清楚，而且你可以把每種配置都實際跑一遍來看看會發(fā)生什么。一旦做好測試好之后，你就可以清楚知道在處置的是什么。

軟件就不同了。只需編輯文件里面某處的文字，同一塊硅晶就可以變成自動駕駛儀或者庫存管理系統。這種靈活性既是軟件的奇跡，也是它的詛咒。因為可以廉價地改變，所以軟件總是在變；同時因為它跟現實的一切都是脫鉤的——所以占據相同空間的程序可以比另一個復雜上千遍——軟件往往會不受束縛地發(fā)展下去。Leveson寫道：“問題在于我們在嘗試建立超過自己管理能力范疇的系統?！?/p>

軟件完全按照我們的指示行事。軟件失敗的原因在于我們告訴它做了錯誤的事情。

關于工程失敗我們標準的思維框架是在二戰(zhàn)后不久形成的（在軟件出現之前，針對機電系統）。其想法是通過把部件做得可靠（比如引擎可承受40000次起飛與降落周期）以及為那些部件故障做好預案（準備2個引擎）來把東西做得可靠。但軟件不會壞掉。Intrado的錯誤閾值不像導致飛機失事的缺損鉚釘。軟件完全是按照人的吩咐行事的。實際上軟件執(zhí)行得非常完美。它失敗的原因在于它被告訴做了錯誤的事。軟件失敗是理解的失敗以及想象的失敗。Intrado其實是有個備份的路由器的，如果能自動切換過去的話，幾乎馬上就能恢復911服務。但“當時發(fā)生的情況是應用邏輯并沒有要執(zhí)行自動修正行動?！?/p>

這就是通過代碼而不是實體做東西的麻煩。如Leveson總結那樣：“復雜性是肉眼看不見的?！?/p>

現在正在進行的改變軟件制作方式的嘗試似乎都始于同一個前提：代碼實在是太難琢磨了。那么在試圖理解這些嘗試之前，弄清楚為什么會這樣是值得的：是什么讓代碼對大腦那么陌生，跟之前的東西那么不一樣呢？

技術進步往往會改變世界的樣子——你可以看著道路鋪設下去，你可以看到天際線的崛起。但在今天你很難說出什么東西進行著了再造，因為這些東西經常是由代碼重構的。比方說，當你踩了汽車油門時，你不再直接控制任何東西；腳踏板與風門之間并沒有機械連接。相反，你只是給軟件提交了一條命令，給引擎補充多少空氣是由后者決定的。汽車就是你可以坐進去的計算機。方向盤和踏板一樣可以是鍵盤的按鍵。

跟一切其他東西一樣，汽車也被計算化以促進新功能。當一個程序負責風門和剎車時，在你距離另一輛車太近時它可以放慢車速，或者控制燃油噴射來幫助你省油。當它控制轉向器時，它可以在你開始漂移時保持在自己車道內，或者引導你進入停車區(qū)。沒有代碼你實現不了這些功能。你可以試試，沒有代碼的汽車就會變成龐大的、重達40000磅但無法移動的發(fā)條裝置。

軟件讓我們做出了有史以來最復雜的機器。但是我們幾乎都沒注意到，因為所有的復雜性都被包裹進小小的芯片里面以及數百萬行的代碼之中。但僅僅因為我們看不見復雜性并不意味著它就沒有了。

著名的荷蘭計算機科學家Edsger Dijkstra在1988年曾經寫到：“必須思考一個頭腦此前從未面臨過的概念層級?！?Dijkstra把這當成一種警示。隨著程序員熱切地想要把軟件植入到關鍵系統當中，軟件日益成為建造世界的關鍵——Dijkstra認為他們已經高估了自己。

軟件工程師并不理解也不關心自己試圖解決的問題。

變成之所以如此困難是因為它需要你像計算機一樣思考。在計算的早期這種陌生感會更加鮮明一點。當時的代碼還是0、1的形式。跟這些枯燥數字打交道的程序員與其實際要解決的問題距離實在是太疏遠了。你不可能看出他們是在計算火炮軌跡還是在模擬井字棋游戲。像Fortran、C這樣的編程語言以及“集成開發(fā)環(huán)境”的引入盡管有所改變，但卻掩蓋了這種基本的異化——事實上程序員并不直接解決問題，而是把時間花在給機器編寫指令上面。

MIT軟件安全專家Leveson說：“問題在于軟件工程師并不理解也不關心自己試圖解決的問題?！痹蛟谟谒麄兲^埋頭于讓自己的代碼可以工作了。她說：“軟件工程師喜歡為編碼錯誤提供各種工具?！彼傅氖荌DE。“但軟件出現的嚴重問題其實跟需求有關，跟編碼錯誤無關?！北确秸f，當你寫代碼控制汽車的風門時，重要的是何時以及如何打開風門打開多大的規(guī)則。但這些系統已經變得太過復雜，任何人腦子里都記不住所有東西。Leveson說：“汽車的代碼現在已經超過了1億行，你無法預料所有的事情?！?/p>

2007年9月，Jean Bookout載上自己最好的朋友開著一項豐田凱美瑞正行駛在高速公路上，突然油門好像被卡住了一樣。她抬腳松開油門，汽車并沒有放緩；她試著踩剎車，但卻似乎失去了動力。當她以50英里的時速轉入匝道時她踩下了緊急剎車。車子劃出了一道150英尺長的滑痕然后撞上路邊的路堤。乘客在這次事故中死亡。Bookout一個月后才從醫(yī)院中醒來。

這次事故是眾多對豐田汽車所謂的突然加速訴訟案中的一起。豐田把事故原因歸咎于墊布的糟糕設計、踏板的“粘性”以及司機錯誤身上，但局外人懷疑該負責的應該是軟件瑕疵。美國國家公路交通安全管理局征召了NASA的軟件專家來對豐田的代碼進行嚴密的審核。在將近10個月后，NASA仍未發(fā)現軟件是事故原因的證據——但同時他們也說自己無法證明軟件不是。

后來有人終于在Bookout事故的訴訟過程中找到了其中令人信服的關聯。原告方的鑒定證人Michael Barr有一個軟件專家團隊花了18個月的時間來研究豐田的代碼，撿起了NASA丟下來的東西。Barr把他們發(fā)現的東西稱為是“面條式代碼（spaghetti code，多頁嵌套的if語句與for循環(huán)，包含大量復制-粘貼的過程代碼，且沒有合適的分割）”。如果代碼一項功能一項功能地堆積起來共生了很多年的話就會變成糾纏不清無法跟蹤，跟不用說進行窮盡測試去追查缺陷了。

如果軟件失靈了也是由同樣一套程序處置的話，則這套程序是無法勝任的。

Barr的團隊利用同款凱美瑞證明了其實車載計算機有超過1000萬種方式導致突然加速事故。他們證明了只需一位的翻轉（從0變成1或者從1變成0）就能讓汽車失去控制。豐田的自動防故障代碼不足以阻止這一點。Barr作證說：“你讓軟件看管軟件。如果這個軟件失靈了還是由同一套程序或者應用來挽救局面的話是難堪此任的，因為它已經失效了?！?/p>

Barr的證詞為Bookout及其朋友的家庭爭取到了300萬美元的賠償。據《紐約時報》，這是針對豐田的訴訟案中首起就電控節(jié)氣門系統進行的審判，也是豐田首次被發(fā)現對突然加速事故負責的案子。后來豐田總共召回了超過900萬輛汽車，賠付金額接近30億美元才了結了相關爭端。

軟件將來還會面臨更多的壞日子。我們今后要更擅長做軟件就變得非常重要，因為如果不行的話，隨著軟件變得越來越復雜以及連接更緊密，隨著軟件控制了更多的關鍵功能——今后的日子會變得更加糟糕。

問題是程序員已經很難跟上自己的創(chuàng)造物。自從1980年代以來，程序員的工作方式以及使用的工具幾乎都沒什么變化。大家逐漸開始擔心這種情況難以為繼。微軟的IDE工具Visual Studio首席軟件開發(fā)者Chris Granger說：“即便是非常好的程序員對自己的系統理解起來也很困難?！?Granger在微軟的時候曾經安排過一次對Visual Studio的端到端研究。這是他唯一完成過的一次類似研究。他用了1個月的時間在單面鏡背后觀察大家是怎么寫代碼的?！斑@些人怎么用工具？如何思考？如何坐在計算機前，有沒有碰鼠標？所有這一切都有教條但并沒有經過經驗測試。”

發(fā)現令人吃驚。他說：“Visual Studio是全世界最龐大的單一軟件之一。它的代碼超過了5500萬行。我在研究中發(fā)現其中98%都是不相干的。也就是說大部分的代碼都沒有針對大家面臨的根本問題。我的最大感受是基本上大家就是在腦子里玩計算機?！背绦騿T就像棋手下盲棋一樣——其思維精力都放在想象拼圖在什么地方上了，以至于已經沒有精力再去思考比賽本身。

過去40年計算機每18個月就能力翻番。為什么編程卻一點都沒有改變？

John Resig在自己的學生身上也注意到同樣的事情。Resig是著名的JavaScript（有一半網站都是JS編寫的）程序員，也是在線教育網站可汗學院的技術領導。2012年初的時候，他一直在糾結于網站的計算機科學課程。為什么學編程就這么難呢？根本問題似乎在于代碼太過抽象了。開發(fā)軟件不像用冰棍棒造橋，你可以看清楚冰棍，可以觸摸粘膠。要想“造”程序，你得敲字。當你想改變程序（無論是游戲、網站或者物理仿真）的行為時，你改變的其實是文字。所以程序寫得好的學生是那些可以將代碼在腦子里過一遍，像計算機一樣思考，能跟蹤每一次中間計算的人。Resig像Granger一樣，開始猜測編程是不是就得這樣。過去40年計算機每18個月就把能力翻番。為什么編程卻一點都沒改變？

這兩個人同時在相同情況下思考同一個問題并不是偶然。兩人都看了同一場演講，那是計算機研究學者Bret Victor個軟件工程學生準備的。演講在2012年2月被放到網上之后火了，它做出了兩個大膽的判斷。第一是我們寫軟件的方式基本上已經壞掉了。其二是Victor知道該怎么修正。

Bret Victor不喜歡寫代碼。他說：“這聽起來很怪異。當我想要做東西，尤其是想用軟件做東西時，我得排除這種天生的厭惡感，因為我操縱的不是我想做的東西，我只是在文字編輯器寫一堆的文字?！?/p>

“我有著相當強烈的信念認為這么做是錯的?！?/p>

40歲的Victor思維敏捷但為人害羞，有著David Foster Wallace的風采。盡管他管理著一個研究未來計算的實驗室，但相對于技術他似乎對利用技術的人的腦子更感興趣。就像任何好的工具制造者一樣，他會從技術和人性的角度去審視這個世界。在那次令他一舉成名的演講上，Victor提出了他的發(fā)明原則：“創(chuàng)作者需要跟所創(chuàng)造的東西有直接關聯?！本幊痰膯栴}正是違背了這一原則。所以軟件系統會如此難以琢磨，出現的bug會如此這多：程序員從寫的第一頁文字開始就是跟要做的東西是脫節(jié)的。

他說：“我們當前對計算機程序的概念是直接源自上世紀50年代的Fortran和ALGOL語言。那些語言是針對穿孔卡片設計的?！爆F在C或者Java等語言的代碼都是屏幕上的字符形式而不是一摞打洞卡片，但還是像過去一樣死氣沉沉，還是一樣的不夠直接。

在Victor看來，盯著文字編輯器來理解癌癥的做法是可怕的。

文字處理有一種類比。過去你在編寫文檔程序里面看到的就是文字本身，要想改變布局或者字體、邊距，你得寫特殊的“控制碼”，或者告訴計算機“這部分文字應該是斜體字”這樣的命令。麻煩的是除非你把文檔打印出來否則是看不到效果的。你很難預測自己會得到什么。你必須想象代碼如何被計算機解釋——也就是說，你必須在腦子里運行一遍。

然后就出現了WYSIWYG（所見即所得）。當你把一段文字標記成斜體時，屏幕上的文字也會相應傾斜。如果你希望改變邊距，你可以直接拖動屏幕頂部的標尺——然后看到改變的效果。文字因此感覺就像是真的，可以隨便擺弄的東西。只需要看著你就能知道自己有沒有做錯。任何人只要能在頁面上點擊都能對復雜系統——文檔布局以及格式引擎——進行控制。

Victor的觀點是編程也應該如此。在他看來，像設計自適應巡航控制系統或者試圖理解癌癥這樣的重要工作靠盯著文本編輯器看來完成是可怕的。確保有朝一日不需要這樣做是程序員的恰當工作。

這個并不是什么瘋狂的想法。因為有不少先例。比方說Photoshop把強大的圖像處理算法交到了甚至不知道算法是什么的用戶手中。這是一款非常復雜的軟件，但那種復雜就像合成器式的復雜，上面有開關旋鈕、按鍵、滑塊等，用戶可以像玩樂器一樣去學習。Squarespace做了一款工具讓用戶只需點擊就能建立網站，而不是用HTML和CSS寫代碼。它已經強大到可以做一度只能由專業(yè)web設計師才能完成的工作。

但這只是一小部分例子。壓倒一切的現實是，當有人想要用計算機做點有趣的東西時，他們基本上都必須寫代碼。身為理想主義者的Victor對此的看法是這不是什么機會，而是大多數程序員的道德淪喪。他的演講就是戰(zhàn)斗號角。

演講的核心是一系列試圖表明現有針對各種問題（電路設計、計算機動畫、調試算法）的工具究竟有多原始的演示，同時也展現了更好的工具可能的樣子。夠諷刺的是，抓住了每個人的想象的一個演示卻是看起來最為微不足道的一個。演示展示了一個分屏，左邊是類似超級瑪麗的游戲，右邊是控制游戲的代碼。隨著Victor改變代碼，游戲世界里面的東西也會發(fā)生變化：他減少了一個數字，也就是重力的強度，然后馬里奧的角色就漂浮起來了。他增加了另一個數字，也就是玩家速度，然后馬里奧就會疾馳而過。

假設你想給游戲設計一關，讓主角跳上一只烏龜然后反彈出去。過去游戲程序員往往要分兩階段解決這類問題：首先，你盯住控制馬里奧如何跳躍、跑得多快、烏龜彈性如何的代碼，然后在文字編輯器進行一些修改，用你的想象力來預測會是什么效果。然后你重放游戲來看看實際會發(fā)生什么。

Victor希望可以更加直接一點。他說：“如果你有一個及時的流程（指的是馬里奧過關的路徑），并且想馬上看到變化情況，你得把時間映射到空間?！彼c擊了一個按鈕，上面顯示的不僅是馬里奧現在在哪里，而且也會顯示出未來每一刻的位置。此外，這條預測路徑還是反應式的：當Victor改變游戲參數（通過拖拽鼠標完成）時，路徑的形態(tài)也會跟著變。就好像擁有了游戲的上帝視角。整個問題已經簡化為玩弄不同的參數，就好像調整立體收音機的旋鈕一樣，直到你讓馬里奧完成工作。有了合適的界面，你幾乎都不用跟代碼打交道，而是直接操縱游戲的行為。

觀眾第一次看到這個時都贊嘆不已。他們知道自己看到的不是小孩的游戲，而是這個行業(yè)的未來。大多數軟件都牽涉到以復雜的方式展現出來的行為，Victor已經表明如果你想象力足夠的話，就可以開發(fā)出手段來看到那種行為并且改變它，就好像自己動手一樣。一位看過這次演講的程序員隨后寫到：“突然之間我所有的工具都感覺過時了?！?/p>

當John Resig看到這場演講時，他把自己給可汗學院轉變的編程教程給廢棄了。他希望網站的編程練習能夠像Victor的演示一樣工作。左手邊會是代碼，右手邊則是運行的程序：這可以是一幅圖畫，一場游戲，或者一次仿真。如果你改變代碼，它馬上就會改變畫面。Resig這樣描述這個方案：“在一個真正響應式的環(huán)境里，你可以徹底改變學生學習編程的方式……他們可以馬上看到結果，并且在沒有明確解釋的情況下憑直覺了解到底層系統固有的內在運作方式?！笨珊箤W院已經成為全世界最大的計算機編程課，每個月平均有100萬用戶在積極地使用這個程序。

在微軟做Visual Studio的Chris Granger也受到了鼓舞。在看到Victor演講視頻的那段日子里，他開發(fā)了一個新的編程環(huán)境原型。其關鍵能力是可以馬上對程序的行為提供反饋。你可以在控制系統的代碼旁邊看到系統是怎么做的。這就好像是脫掉了眼罩。Granger把這個項目叫做“Light Table”。

2012年，他在Kickstarter上面為Light Table籌集資金。項目在編程界引起了轟動。在一個月的時間里，項目就募集到了20多萬美元。這個想法傳播出去了?，F場感（liveness）的概念，也就是馬上就能看見數據流經程序的情況，隨后變成了Google、蘋果旗艦編程工具的功能。iPhone和Mac的默認開發(fā)語言Swift是蘋果為了支持名為Playground的環(huán)境而從頭開始開發(fā)出來的，這門語言正是直接受到了Light Table的啟發(fā)。

但在看到自己的演講最終產生的影響之后，Bret Victor的希望破滅了。他后來說：“很多東西似乎誤解了我說的話。”當大家邀請他出席會議討論編程工具時，他知道情況不對頭了。他說：“每個人都以為我對編程環(huán)境感興趣?！逼鋵嵥信d趣的是大家如何看待和理解系統——如他所概括那樣，是“動態(tài)行為的直觀表現”。盡管代碼日益成為創(chuàng)建動態(tài)行為的工具選擇，但仍然是理解行為最糟糕的工具之一?！鞍l(fā)明原則”的要點是要表明你可以通過在系統行為與代碼之間建立直接聯系來緩解這一問題。

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

在隨后的兩場演講“停止畫死魚”以及“畫動態(tài)可視化”中，Victor又深入了一步。他演示了兩個自己開發(fā)的程序——第一個是給動畫家準備的，第二個是給試圖可視化自己數據的科學家準備的——這兩個過去都需要寫很多定制代碼但現在被簡化為WYSIWYG（所見即所得）界面。Victor認為同樣的做法幾乎可以應用到編寫代碼解決的每一個問題上面。他說：“我不敢肯定代碼是否有存在的必要?；蛘咧辽佘浖_發(fā)者有存在的必要?！痹谒磥?，軟件開發(fā)者的恰當角色是創(chuàng)建工具來消除對軟件開發(fā)者的需要。只有這樣有著最緊迫計算問題的人才能直接把握這些問題而不需要以代碼為中介。

當然，為了做到這一點，你得讓程序員本身買賬。Victor在最近的一篇論文中懇求專業(yè)軟件開發(fā)者不要再把自己的天才浪費到開發(fā)Snapchat以及Uber這樣的app上。他寫道：“日常生活的便利性不是重大問題。”相反，開發(fā)者應該把關注點放到科學家和工程師身上——“那些人做的工作才是重要的，而且更關鍵的是，他們使用的工具真的非常的糟糕?！彼€寫道，像這類令人激動的工作，尤其是一類“基于模型設計”的工具已經在開發(fā)當中，而且進行了好幾年了，但大多數程序員對此一無所知。

“如果你看看自己手上所有的工業(yè)用品，包括你自己用的，公司用的，里面唯一不是工業(yè)的東西就是代碼。” Eric Bantégnie是Esterel Technologies的創(chuàng)始人，這家法國公司做的是開發(fā)安全關鍵軟件的工具。像Victor一樣，Bantégnie并不認為工程師應該靠往IDE呼入幾百萬行代碼來開發(fā)大型系統。他說：“沒人想要手工造一輛車。代碼是在很多地方還是手工作坊。如果只是人工敲10000行代碼還可以。但有些系統有3000萬行代碼，比如空客，或者1億行代碼，如Tesla或高端汽車——這些系統就變得非常非常復雜了?！?/p>

Bantégnie的公司是業(yè)界利用基于模型的設計的先驅之一，有了這種工具你不再需要直接編寫代碼。相反，你創(chuàng)建的是一種描述程序應該遵循的規(guī)則的流程圖（“模型”），然后計算機會基于那些規(guī)則替你生成代碼。比方說，如果你要給電梯做控制系統，規(guī)則之一可能是當門打開時，有人按下去大廳的按鈕時，你應該關上門，然后開始移動電梯。在基于模型的設計工具里，你會用一張小小的圖來表示這條規(guī)則，就好像在白板上畫出這條邏輯一樣，做出代表不同狀態(tài)——如“門打開”、“移動”、“門關閉”等的方框，以及定義如何從一個狀態(tài)轉移到另一個狀態(tài)的線段。這種圖解使得系統規(guī)則變得明顯：只需看著它你就能看到讓電梯移動的唯一辦法就是關上電梯門，或者唯一讓門打開的辦法是讓電梯停下來。

大家知道怎么寫代碼。問題是該寫什么代碼。

但這還沒到Photoshop那種效果。當然，Photoshop的魅力在于你在屏幕上操縱的圖畫是最終產品。相比之下，在基于模型的設計中，你在屏幕上的圖畫更像是藍圖。盡管如此，用這種辦法做軟件就定性而言仍然跟傳統編程有著很大的不同。在傳統的編程中，你的任務是將復雜規(guī)則轉換成代碼；你大部分的精力都換在進行這種轉化上，而不是考慮規(guī)則本身。而在基于模型的方法中，你擁有的全部就只有規(guī)則。所以這就是你要花時間考慮的。這樣一來你關注機器就會少一點而把更多的焦點放在試圖讓它解決的問題上。

Bantégnie說：“通常軟件編碼的主要問題——我本人也是編碼者——并不是編碼者的技能。這些人知道如何去編寫代碼。問題在于要編寫什么代碼。因為大多數需求都屬于自然語言，是含糊的，一個需求是永遠也無法做到極端精確的，寫代碼的人往往會有不同的理解?！?/p>

按照這種看法，軟件就變成難以駕馭的了，因為媒體描述軟件應該做的事情——會話、文字描述、在紙上畫畫——這些事情跟媒體描述的軟件能做的事情，也就是代碼本身太不一樣了。從一邊到另一邊中間丟失的東西太多了?；谀Ｐ偷脑O計這一想法的背后就是想填補這一鴻溝。表達自己需要什么的系統設計師以及自動生成代碼的計算機采用的都是同一個模型。

當然，這種辦法想要成功的話，有很多工作都需要在項目甚至還沒開始前就得完成。得有人首先開發(fā)工具來建立大家習慣的模型——那種就像自己平時做的筆記和草圖一樣的模型——但同時計算機理解起來也不會產生歧義。他們必須開發(fā)出一款程序將這些模型變成真正的代碼。最后他們還得證明生成的代碼永遠都會做它們該做的事情。Bantégnie說：“開始20年的后臺工作讓我們受益匪淺?！?/p>

2012年被ANSYS收購的Esterel Technologies誕生于1980年代，當時的法國核工業(yè)和航空業(yè)越來越難以避免bug的問題，因為擔心關鍵性安全代碼復雜性問題膨脹而開始了這方面的研究。達索航空的科研負責人Emmanuel Ledinot說：“我是從1988年開始的。那時候，我在做軍用航電系統。負責系統集成以及調試的人注意到bug的數量在上升?！?980年代機載計算機的數量出現了飆升，每架飛機上的計算機已經由單臺變成了10幾臺，每一臺計算機分別負責控制、導航以及通信相關的、高度專業(yè)化的任務。當來自傳感器的數據涌入以及飛行員輸入指令時協調這些系統控制飛行需要演奏交響樂般的完美反應。Ledinot說：“在合適的時機按照合適的次序處理上百乃至上千的可能事件被認為是bug膨脹的主要原因?！?/p>

Ledinot由此認定手工編寫如此復雜的代碼已經難以為繼。代碼究竟在做什么事情已經太難以理解了，想要驗證它是否正確工作幾乎是不可能的。為此他要尋找新的東西。他在一次演講中說：“你必須理解在像這樣的過程中更換工具是極其昂貴的。除非你已經無路可退，否則是不會做出這種決定的?！?/p>

大多數程序員喜歡代碼。至少他們理解代碼。

他開始跟法國計算研究中心INRIA的計算機科學家Gerard Berry合作開發(fā)Esterel，這個名字在法語里面是“實時”的合成詞。Esterel背后的想法是傳統編程語言也許擅長描述按照預定次序進行的簡單過程——比如烹飪法——但如果你試圖用到大量事件近乎實時以任何次序并發(fā)的系統（比如飛機駕駛艙）上面時，就會不可避免地陷入混亂。而控制軟件發(fā)生混亂是危險的。Berry在一篇論文中甚至預測“低級編程技巧對于大型關鍵性安全系統來說將是不可接受的，因為它們會導致行為理解和分析幾乎不可行?！?/p>

Esterel的目的是讓計算機替你處理這種復雜性。這就是基于模型的方案的希望所在：你不再需要編寫一般的編程代碼，而是建立系統行為的模型——在這個例子里面，模型關注的是獨立事件應該如何處置，如何確定事件的優(yōu)先次序，哪一個事件依賴于其他的事件等等。模型變成了計算機用來進行實際編程的詳細藍圖。

Ledinot和Berry用了整整10年的時間晚上Esterel使之可用于生產。說：“2002年我們有了第一個可自動生成代碼的操作型軟件建模環(huán)境，并且為陣風戰(zhàn)斗機生成了第一個嵌入式模塊?！苯裉欤珹NSYS SCADE產品族已經被廣泛應用到航空、國防、核電、交通、重工業(yè)、醫(yī)療設備等行業(yè)的代碼生成當中。Esterel Technologies創(chuàng)始人Bantégnie說：“我最初的夢想是讓SCADE生成的代碼遍布全世界每一架飛機上，現在我們距離這個目標已經不太遠了?！卑刂骑w機飛行操縱面的系統在內，空客A380幾乎所有的關鍵性安全代碼都是由SCADE生成的。

我們早已經知道如何讓負責軟件變得可靠，但在太多的地方我們都選擇不這么做。

就像Bantégnie解釋那樣，讓計算機而不是人把你的需求變成代碼的美妙之處在于你可以確保生成的代碼滿足那些需求（其實你可以用數學證明這一點）?；谀Ｐ偷姆桨复蟛糠趾锰巵碜杂谠谀軌驅崟r添加需求的同時確保原有需求得到滿足；每一次變更計算機都能驗證程序仍然有效。你可以隨便調整藍圖而不怕引入新的bug。用FAA的話來說，你的代碼是可以“在建構的時候修正的”。

盡管如此，大多數軟件都用傳統的方式開發(fā)的，甚至在癡迷于安全的航空界也是如此，工程師要寫好自己的需求，然后再由程序員用C這樣的語言寫成代碼。正如Bret Victor在論文中表明那樣，相對而言基于模型的設計是不同尋常的。Shivappa說：“FAA的很多人認為代碼生成是魔術，因此要求進行更嚴格的審查?！?/p>

大多數程序員也是這種想法。他們喜歡代碼。至少他們理解代碼。替你寫代碼并驗證其正確性的工具利用的是數學的“有限狀態(tài)機”以及“遞歸系統”，這些東西如果說不是好得令人難以置信的話，那就是晦澀難懂且很難使用。

這種事情以前也發(fā)生過。只要編程稍微遠離寫0、1一步，反對聲音最響亮的都是程序員。參與阿波羅計劃的著名軟件工程師Margaret Hamilton（“軟件工程”這個術語就是她發(fā)明的）說，1964年在MIT的Draper實驗室的第一年時，她記得有一次會上一個派別的人跟另一派就從“非常低級的機器語言”過渡到更高級的匯編語言的事情吵個不停?！白畹讓拥娜似疵胍Ａ暨@種語言。他們的觀點都很相似：‘誰知道匯編語言能不能做好啊？’”

她說：“一邊的家伙吵得面紅耳赤，開始大喊大叫起來?！北硎咀约簩Α斑@幫人情緒化如此嚴重感到吃驚?！?/p>

你可以不停地做測試，但永遠也無法找完所有的bug。

達索航空的Emmanuel Ledinot指出，在匯編語言被至今仍流行的語言如C等逐步淘汰的時候，持懷疑態(tài)度的卻變成了使用匯編語言的那幫人。毫不奇怪，“朝著基于模型的軟件開發(fā)轉變并不容易：他們感覺可能這會又一次失去控制，甚至比已經發(fā)生的情況還要糟糕?！?/p>

基于模型的設計有時候又被稱為模型驅動工程（MDE），面前仍面臨著根深蒂固的偏見，據一篇最近的論文，“一些人甚至認為調查大家對MDE的看法甚至比研究新的MDE技術的需求還要強烈。”

這聽起來似乎是個笑話，但對于基于模型方案的支持者來說，這是很重要的一點：我們已經知道如何讓復雜軟件變得可靠，但為什么在那么多地方我們都選擇不這么做呢？

2011年的時候，Chris Newcombe已經在Amazon工作了將近7年，并且已經晉升為首席工程師。公司的一些最關鍵的系統，包括零售產品目錄以及管理全世界每一臺Kindle設備的基礎設施等他都有參與。他是備受贊譽的AWS（Netflix、Pinterest、Reddit等都在上面托管）團隊的一名領導。在Amazon之前，他幫助建立了全球最大在線游戲服務Stream的骨干。他是悄悄維持互聯網運轉的工程師之一。他做過的產品被認為取得了大規(guī)模的成功。但他一直都在擔心那些系統的設計會成為一顆顆帶來災難的定時炸彈。

他在一篇論文中說：“在估計規(guī)模達每秒數百萬請求的系統‘極其罕見’的事件組合的可能性方面，人類的直覺非常糟糕。人類的易錯性意味著其中一些更微妙、更危險的bug原來是設計過程犯的錯；代碼只是忠實地履行設計想讓它干的事情，但設計未能正確地處理一種特別“罕見的場景”。

Newcombe確信，真正關鍵系統——比方說存儲很大一部分web數據的系統——背后的算法應該不僅僅要好，而且要做到完美。哪怕一個細微的bug有可能是災難性的。但他知道找到bug有多困難，尤其是當算法變得越來越復雜的時候。你可以把想做的測試都給做了，但永遠也無法把所有的bug找完。

很少有程序員在開始編碼前繪制自己程序要做什么的草圖。

這就是他會對一種數學與代碼的奇怪混合感到如此著迷的原因。這個東西看起來跟代碼很像，它會把算法用“TLA+”來進行描述。令人感到驚奇的地方在于這種描述據說在數學上是精確的：用TLA+編寫的算法正確與否原則上是可以證明的。實際上，它可以讓你建立問題的現實模型，而且進行的測試不僅是徹底的，甚至可以說是窮盡的。這就是他一直在尋找的東西：一種能寫出完美算法的語言。

TLA+的意思是“行為時序邏輯（Temporal Logic of Actions）”，其內涵跟基于模型的設計類似：這是一門記錄需求的語言——TLA+稱之為計算機程序的“規(guī)范”。這些規(guī)范然后可以由計算機進行完全驗證。也就是說，在編寫任何代碼之前，你就先寫出了程序邏輯的簡版大綱，以及需要它滿足的約束（比方說你要給ATM編程，約束可能是永遠也不能撤銷賬戶的同一筆錢超過2次。）。TLA+然后再窮盡檢查邏輯的所有可能性是否均滿足那些約束。如果不能滿足，它會展示違背約束的情況究竟是什么樣的。

這門語言是由圖靈獎得主Leslie Lamport發(fā)明的。現在微軟研究院就職的他是“分布式系統”理論的先驅之一。其工作為現代web的眾多系統奠定了基礎。

在Lamport看來，今天的軟件bug那么多的一個主要原因是程序員直接就跳到寫代碼這一步了。他在一篇文章中寫道：“架構師在砌第一塊磚，釘第一顆釘子之前要先畫好詳細規(guī)劃圖。但很少有程序員會在寫代碼之前畫程序應該做什么事情的草圖?！背绦騿T著迷于編碼的具體細節(jié)，因為代碼才是讓程序變活的關鍵；把時間花在任何其他地方似乎都屬于分心。而且苦思冥想代碼的微觀力學還能帶來耐心的愉悅，一種沉思的滿足感。但Lamport認為，代碼永遠都無法成為思想的媒介。他說：“當你用編程語言進行思考時，你的思維能力其實是受限的。代碼會讓你只見樹木不見森林：它把你的注意力吸引到單個組件上面，而不是程序拼湊出來的更大圖景，或者它應該要做的事情——以及它是否按照你的想法做?！彼訪amport才要創(chuàng)建TLA+。就像基于模型的設計一樣，TLA+把你的注意力集中在相同的高級結構、基本邏輯上面，而不是實現那些東西的代碼上。

Newcombe極其在Amazon的同事還將繼續(xù)用YLA+來尋找重要系統里面細微但關鍵的bug，包括被認為是全球最可靠的存儲引擎S3背后核心算法里面的bug。現在它已經在這家公司內部得到廣泛使用。在這個曾經使用過TLA+的人組成的微小世界里，他們的成功算不上不同尋常。微軟的一位實習生用TLA+找到一個可能會導致每一臺Xbox在使用數小時后崩潰的bug。歐洲太空總署的工程師用它來重寫了一個人類首次軟著陸彗星的探測設備的操作系統，而且代碼量還只是原來的1/10。英特爾用它來定期校驗自己的芯片。

不過TLA+只占據了遠離主流的小小一個角落，如果說它的確有一席之地的話。即便對于像Newcombe這樣經驗豐富的工程師而言，這門語言一開始讀起來也是非常的離奇難懂——這完全就是符號的大雜燴。在Lamport看來，這是教育的失敗。盡管編程誕生自數學，但此后基本上已經與之分道揚鑣。大多數程序員對那種數學——邏輯和集合論都不是很熟悉，而這正是TLA+所需要的。Lamport說：“很少有程序員理解非?；镜母拍钜约斑@些概念如何應用到實踐中，甚至連教編程的老師也是如此。要用比編碼更高級的思維去精確思考，而數學其實可以讓你的思考更家精確，這種想法完全屬于異類。因為他們從來都沒學過這個?！?/p>

我希望如果這些簡單的事情都不理解的話就不允許他們寫程序。

Lamport這種數學思維的失敗視為現代軟件開發(fā)的問題：其風險在不斷攀高，但程序員卻沒有相應提升自己——他們還沒有武裝到牙齒，無法應對日益復雜的問題。他說：“在15世紀，大家往往在不知道微積分的情況下建教堂，但現在我并不認為不懂微積分的人還可以去建教堂。我希望經過適當長的一段時間之后，那些不理解這種簡單事情的人是不允許寫程序的?！?/p>

Newcombe就不是很確定程序員應該承擔這種責任。他說：“我從Leslie那里了解到他認為程序員害怕數學。我的發(fā)現是程序員并沒有意識到——或者并不認為——數學可以幫助他們處理復雜性。發(fā)砸星是程序員最大的挑戰(zhàn)?！彼J為讓大家使用TLA+的正在問題在于要說服這幫人這不會浪費他們的時間。就一個物種而言，程序員是徹底的實用主義。像TLA+這樣的工具散發(fā)著象牙塔的臭氣。當程序員遭遇“形式化方法”（之所以這么叫是因為涉及到對程序的數學性的、“形式化”的精確描述）時，其根深蒂固的直覺就是退避三舍。

大多數在大學上計算機科學課程的程序員都曾粗略碰到過一些形式化方法。通常會在一些無足輕重的場合進行演示，比如從0開始計數的程序，學生的工作是從數學上證明程序的確是從0開始計數的。

Newcombe說：“我得改變大家對形式化方法的看法。”甚至Lamport本人似乎也沒有完全把握住這一點：形式化方法存在著形象問題。解決這一點的辦法不在于乞求程序員做出改變——要改變的是你自己。Newcombe意識到要想讓TLA+這樣的工具成為編程主流，你得開始講他們的語言。

首先，他說當他向Amazon的同事介紹TLA+時，會避免告訴對方它代表著什么，因為他害怕TLA+的名字會讓他們望而生畏：“行為時序邏輯”恰恰就彌漫著學術界的那股自大的光環(huán)，但卻令大多數程序員感到反感。他還盡量不用“形式化”、“驗證”或者“證明”這樣的術語，因為這會讓程序員想到乏味的課堂練習。相反，他把TLA+包裝成了一種新型的“偽代碼”，是邁向真正代碼的墊腳石，可以讓你對算法進行窮盡測試——而這又讓你可以在設計過程盡早進行精確地思考。他寫道：“工程師是用調試而不是‘驗證’的思路進行思考”，所以他把面向Amazon內部進行的講座題目叫做《調試設計》。Newcombe不是惋惜程序員用代碼來看世界的事實，而是主動去擁抱它。他知道否則的話自己就會失去他們。Newcombe說：“我已經看到一堆人說，‘現在我理解了?！?/p>

代碼已經制造了一種全新水平的復雜性。同時也讓一種新型的失效成為可能。

此后他離開Amazon去了Oracle，在那里接著說服新同事給TLA+一個機會。在他看來，使用這些工具現在已經成為了一種責任。他說：“我們需要更擅長這個。”

“我是自學的，從9歲開始我就開始寫代碼，所以我的本能是開始寫代碼。這是我唯一的思考方式：勾勒輪廓，嘗試，然后有組織地演變。”在他看來，這是許多程序員至今仍然采用的方式。“他們google，上Stack Overflow”（Stack Overflow是一個流行的編程相關問答網站），“他們尋找解決其戰(zhàn)術性關切的代碼片段，然后拼湊起來，不斷迭代。”

“這種做法無可厚非直到你遇到大麻煩。”

2015年夏，美國的兩位安全研究人員Charlie Miller和Chris Valasek認為汽車制造商對軟件缺陷并未給予足夠的重視，于是他們證明一輛2014款的吉普切諾基可以被黑客遠程控制。他們利用了擁有無線連接的車載娛樂系統實際上跟更多的中心系統（比如控制雨刮器、油門、剎車的系統）也有連接這一事實。他們利用業(yè)余的時間做出了攻擊系統，并且黑掉了記者駕駛的一輛切諾基，讓車子失去控制，導致那位記者陷入恐慌。

盡管他們沒有動手，但卻表明了寫出一款更好的軟件是有可能的，所謂“汽車蠕蟲”可以利用被黑的切諾基車載計算機去掃描和攻擊其他的切諾基；如果他們愿意的話，他們可以同時訪問全美有漏洞的汽車和SUV。有朝一日可以讓所有那些車輛突然把方向盤打左或者在高速行駛時切斷引擎。

Valasek說：“我們需要換種思路來審視軟件?！逼嚻髽I(yè)一直以來都是將成百上千不同供應商生產的零件組裝成最終產品。但這些過去一度是純粹機械化的零件，現在往往都帶著好幾百萬行的代碼。盡管其中一些代碼——比如自適應巡航控制，自動剎車以及車道保持等的——的確讓車輛變得更安全了—，但也制造了全新水平的復雜性。并且使得一種新型的失效變成可能。

在無人車的世界里，軟件不能成為事后想法。

Esterel背后的法國研究人員Gerard Berry說：“汽車存在著大量的bug。它不像航空電子，航空電子對待bug非常認真。并且承認軟件不同于機械。”汽車業(yè)可能跟很多行業(yè)一樣尚未意識到自己其實也身處軟件業(yè)。

在豐田案作證的軟件安全專家Michael Barr說：“汽車業(yè)缺乏了解軟件在做什么的軟件安全監(jiān)管者?！彼fNHTSA“只有有限的軟件專業(yè)知識?！笔沟没谀Ｐ偷脑O計與代碼生成對航空業(yè)產生吸引力的相同監(jiān)管壓力降臨到汽車業(yè)身上要慢一些。但達索航空的Emmanuel Ledinot認為這種差異也許還有經濟方面的原因。汽車根本無法接受零件成本的增加，哪怕幾美分都不行，因為乘上幾百萬就是個大數字；因此嵌入到汽車的計算機必須縮減到最少水平，這幾乎不給尚未調整到精益水平的代碼太多的運行空間?！拔艺J為過去10年引入基于模型的軟件設計對他們來說代價太高了?！?/p>

Ledinot懷疑其誘因也在改變：“我覺得汽車業(yè)可能會推進。ISO 26262和汽車業(yè)可能會慢慢推進關鍵部件采用這種方案。”（ISO 26262是2011年發(fā)布的汽車安全標準）。Barr的觀點也基本一樣：在無人車的世界里，軟件不能成為事后想法。它不能像今天的機票預訂系統或者911系統或者股票交易系統一樣搭建。那些代碼要對道路上的數億個生命負責，它必須有效。這可不是小事情。

Gerard Berry在演講中說：“計算基本上是不可見的。當你的輪胎沒氣時，你會看見它是癟的。當你的軟件出問題了，你看著軟件卻什么也看不到?！?/p>

“所以這是一個大問題?！?/p>