在2014年4月10日，在華盛頓州的全部人口沒有911服務的晚上這里是六個小時怨喘。呼救的人得到了一個忙碌的信號锉走。一名西雅圖女子至少37次撥打911载荔，而一名陌生人試圖闖入她的房子荆永。當他終于從窗戶爬進她的起居室時缀磕，她拿起一把菜刀藐握。那個男人逃走了额各。

在有史以來最大的報道中晶疼，911中斷被追溯到科羅拉多州恩格爾伍德的服務器上運行的軟件酒贬。由一個名為Intrado的系統(tǒng)提供商運營，該服務器保持了一個運行計數(shù)器翠霍，它已經(jīng)向全國各地的911調(diào)度員發(fā)送了多少呼叫同衣。Intrado程序員已經(jīng)設定了計數(shù)器可以達到的高度的閾值。他們選擇了數(shù)百萬的數(shù)字壶运。

在4月10日午夜前不久耐齐，柜臺超過了這個數(shù)字，導致混亂。由于計數(shù)器用于為每個呼叫生成唯一標識符埠况，因此拒絕新呼叫耸携。而且由于程序員沒有預料到這個問題，他們沒有創(chuàng)建警報來引起注意辕翰。沒有人知道發(fā)生了什么夺衍。華盛頓州，加利福尼亞州喜命，佛羅里達州沟沙，卡羅來納州和明尼蘇達州的調(diào)度中心為1100萬美國人提供服務，他們很難理解有關呼叫者忙碌信號的報道壁榕。直到早上才意識到恩格爾伍德的Intrado軟件是負責任的矛紫，并且修復是為了改變一個數(shù)字。

不久前牌里，緊急呼叫在當?shù)靥幚砑找АＭｋ姾苄。苋菀自\斷和修復牡辽。手機的興起和新功能的承諾 - 如果你能發(fā)短信911怎么辦喳篇？或發(fā)送視頻給調(diào)度員？ - 推動了依賴互聯(lián)網(wǎng)的更復雜系統(tǒng)的發(fā)展态辛。這是第一次出現(xiàn)國家911停電這樣的事情◆锢剑現(xiàn)在已經(jīng)有四年了。

據(jù)說軟件“正在吞噬世界奏黑〈栋睿”越來越多的機械或人員控制的關鍵系統(tǒng)將依賴于代碼。這可能永遠不會比2015年夏天更加清晰攀涵，因為在一天之內(nèi)铣耘，由于其離港管理系統(tǒng)存在問題，聯(lián)合航空公司將其機隊停飛; 升級后以故，交易在紐約證券交易所暫停; 華爾街日報網(wǎng)站的頭版崩潰了; 西雅圖的911系統(tǒng)再次出現(xiàn)故障蜗细，這次是因為另一臺路由器出現(xiàn)故障。這么多軟件系統(tǒng)的同時失敗首先是在協(xié)調(diào)的網(wǎng)絡攻擊中聞到的怒详。幾乎更可怕的是炉媒，當天晚些時候認識到，這只是一個巧合昆烁。

“當我們有機電系統(tǒng)時吊骤，我們過去常常能夠?qū)λ鼈冞M行詳盡的測試“麻省理工學院航空航天學教授Nancy Leveson說，他一直在研究軟件安全35年静尼。她因有關Therac-25的報告而聞名白粉，該放射治療機由于軟件錯誤導致六名病人死亡传泊。“我們曾經(jīng)能夠思考它可以做的所有事情鸭巴，它可以進入的所有狀態(tài)眷细。”例如鹃祖，控制鐵路交叉口列車運動的機電聯(lián)鎖只有很多配置; 幾張紙可以描述整個系統(tǒng)溪椎，你可以針對每個配置運行物理列車，看看它的行為方式恬口。一旦你構建并測試它校读，你就知道你正在處理什么。

軟件不同祖能。只需在某處編輯文件中的文本歉秫，相同的硅片就可以成為自動駕駛儀或庫存控制系統(tǒng)。這種靈活性是軟件的奇跡芯杀，也是它的詛咒端考。因為它可以廉價地改變雅潭，軟件會不斷變化; 因為它不受任何物理攻擊 - 一個比另一個更復雜的程序占用相同的實際空間 - 它往往會無限制地增長揭厚。<mark class="nk nl ex" style="box-sizing: inherit; cursor: pointer; background-color: rgb(255, 213, 194); color: currentcolor;">“這個問題，”Leveson在一本書中寫道扶供，“我們正試圖構建超出我們智力管理能力的系統(tǒng)筛圆。”</mark>

我們用于思考工程故障的標準框架（例如椿浓，在醫(yī)療設備法規(guī)中得到反映）是在第二次世界大戰(zhàn)后不久太援，軟件出現(xiàn)之前為機電系統(tǒng)開發(fā)的。我們的想法是扳碍，通過使其部件可靠（例如提岔，您構建發(fā)動機以承受40,000次起飛和著陸循環(huán)）并通過計劃這些部件的故障（您有兩個發(fā)動機）來制造可靠的東西。但軟件并沒有破解笋敞。Intrado的故障閾值不像導致客機墜毀的故障鉚釘碱蒙。該軟件完全按照它所做的去做。事實上它完美地做到了夯巷。失敗的原因是它被告知要做錯事赛惩。軟件失敗是理解和想象的失敗。Intrado實際上有一個備份路由器趁餐，如果它已經(jīng)自動切換喷兼，幾乎可以立即恢復911服務。但是后雷，正如聯(lián)邦通信委員會的一份報告中所描述的那樣季惯，“情況發(fā)生在應用程序邏輯中的一個點上吠各，該點并非旨在執(zhí)行任何自動糾正措施∶阕ィ”

這是用代碼制作東西的麻煩走孽，而不是物理的東西。正如Leveson所說琳状，“復雜性”是“看不見的”磕瓷。

[圖片上傳失敗...(image-9c7141-1565709376163)]

[圖片上傳失敗...(image-551527-1565709376163)]

?他試圖現(xiàn)在正在進行改變我們?nèi)绾问管浖坪醵寂c同一個前提：代碼是太難思考的問題。在嘗試理解這些嘗試本身之前念逞，值得理解為什么這可能是：代碼使它對思想如此陌生困食，以及與之前的任何東西不同。

技術進步曾經(jīng)改變了世界的樣子 - 你可以看到鋪好的道路; 你可以看到天際線上升翎承。今天你幾乎無法分辨什么東西被重制硕盹，因為它經(jīng)常被代碼重新制作。例如叨咖，當你用腳踩下汽車的加速器時瘩例，你就不再直接控制任何東西; 從踏板到油門沒有機械連接。相反甸各，您正在向一個軟件發(fā)出命令垛贤，該軟件決定給發(fā)動機提供多少空氣。這輛車是你可以坐在里面的電腦趣倾。方向盤和踏板也可能是鍵盤鍵聘惦。

與其他所有產(chǎn)品一樣，該車已經(jīng)過計算機化以實現(xiàn)新功能儒恋。當一個程序負責油門和制動時善绎，當你離另一輛車太近時它可以減慢你的速度，或者精確地控制燃油噴射以幫助你節(jié)省燃氣诫尽。當它控制轉向時禀酱，它可以讓您在開始漂移時保持在您的車道上，或引導您進入停車位牧嫉。沒有代碼剂跟，您無法構建這些功能。如果你試過驹止，一輛汽車可能重達40,000磅浩聋，這是一支不可移動的發(fā)條。

軟件使我們能夠制造出迄今為止最復雜的機器臊恋。然而衣洁，我們幾乎沒有注意到，因為所有這些復雜性都被包含在微小的硅芯片中抖仅，成千上萬行代碼坊夫。但僅僅因為我們看不到復雜性并不意味著它已經(jīng)消失了砖第。

這位程序員，著名的荷蘭計算機科學家埃德斯·迪克斯特拉（Edsger Dijkstra）在1988年寫道环凿，“必須能夠思考比以前需要面對的單一思想更深刻的概念層次梧兼。”Dijkstra將此視為警告智听。隨著程序員急切地將軟件傾注到關鍵系統(tǒng)中羽杰，他們越來越成為建筑世界的關鍵 - 而Dijkstra認為他們可能已經(jīng)高估了自己。

使編程如此困難的原因是它需要你像計算機一樣思考到推。在計算的早期階段考赛，當代碼采用文字和零的形式時，它的陌生感在某種意義上更加生動莉测。任何看過程序員肩膀的人都會看到程序員與他們試圖解決的實際問題有多么疏遠颜骤，因為他們會像“100001010011”和“000010011110”一樣仔細思考。我們無法判斷他們是在試圖計算炮兵軌跡還是模擬一個井字游戲捣卤。引入類似于英語的Fortran和C等編程語言忍抽，以及稱為“集成開發(fā)環(huán)境”的工具，或稱為幫助糾正簡單錯誤的工具（如Microsoft Word的語法檢查程序董朝，但代碼）鸠项，模糊不清，

“問題是益涧，軟件工程師不懂的問題锈锤，他們正在試圖解決驯鳖，并不在乎闲询，” Leveson，麻省理工學院軟件安全專家說浅辙。原因是它們太過于無法讓代碼工作扭弧。“軟件工程師喜歡提供各種工具和編碼錯誤的東西记舆，”她說鸽捻，指的是IDE≡笕“軟件發(fā)生的嚴重問題與需求有關御蒲，而不是編碼錯誤≌锷蓿”例如厚满，當您編寫控制汽車油門的代碼時，重要的是關于何時碧磅，如何以及打開多少的規(guī)則它碘箍。但是這些系統(tǒng)變得如此復雜遵馆，以至于幾乎沒有人能夠?qū)⑺鼈冎苯臃旁谀X中》崃瘢“現(xiàn)在汽車中有1億行代碼货邓，”Leveson說∷谋簦“你無法預料到所有這些事情换况。”

2007年9月盗蟆，當加速器似乎被卡住時复隆，Jean Bookout和她最好的朋友在豐田凱美瑞一起駕駛高速公路。當她從踏板上踩下腳時姆涩，車子沒有減速挽拂。她試過剎車但似乎失去了力量。當她轉向一個每小時50英里的匝道時骨饿，她拉緊急剎車亏栈。這輛車在跑到路邊的路堤之前留下了150英尺長的防滑標記。這名乘客遇難宏赘。一個月后绒北，預約在醫(yī)院醒來。

這項事件是近十年來對豐田汽車所謂的意外加速聲稱的調(diào)查中的眾多事件之一察署。豐田將事故歸咎于設計不良的地板墊闷游，“粘性”踏板和駕駛員錯誤，但外界懷疑有缺陷的軟件可能是負責任的贴汪。美國國家公路交通安全管理局邀請美國宇航局的軟件專家對豐田的代碼進行深入審查脐往。在將近10個月后，NASA團隊沒有找到證據(jù)證明軟件是原因 - 但他們說不能證明它不是扳埂。

正是在Bookout事故的訴訟中业簿，有人終于找到了令人信服的聯(lián)系。原告的專家證人邁克爾·巴爾（Michael Barr）有一個軟件專家團隊用豐田代碼花了18個月的時間阳懂，在美國宇航局停止工作的地方梅尤。Barr描述了他們發(fā)現(xiàn)的“意大利面條代碼”，程序員語言的軟件已成為一個混亂的混亂岩调。代碼變成了意大利面條巷燥，當它累積多年時，功能堆疊在上面号枕，并編織在周圍缰揪，已經(jīng)存在的東西; 最終代碼變得無法遵循，更不用說徹底檢查缺陷了堕澄。

Barr的團隊使用與事故中涉及的凱美瑞相同的模型邀跃，證明車載計算機實際上有超過1000萬種方式會導致意外加速霉咨。他們表明，只需一個位翻轉 - 計算機內(nèi)存中的一個變?yōu)榱慊蚍粗嗳?- 可能會使汽車失控拍屑。豐田實施的故障安全代碼還不足以阻止它途戒。“你有軟件看軟件僵驰，”巴爾作證說喷斋。“如果軟件發(fā)生故障并且同一個程序或同一個崩潰的應用程序應該可以節(jié)省一天的時間蒜茴，那么它就無法保存星爪，因為它無法正常工作》鬯剑”

Barr的證詞為原告提起訴訟顽腾，導致Bookout和她朋友的家人損失300萬美元。據(jù)“紐約時報”報道诺核，這是針對豐田的許多類似案件中第一起引發(fā)電子節(jié)氣門控制系統(tǒng)試驗問題的案例抄肖，也是豐田首次因涉及意外加速的事故而被陪審團負責。雙方?jīng)Q定解決案件窖杀，然后才能判給懲罰性賠償金漓摩。總而言之入客，豐田召回了超過900萬輛汽車管毙，并支付了近30億美元的定居費和與意外加速相關的罰款。

[圖片上傳失敗...(image-d1b6a1-1565709376163)]

[圖片上傳失敗...(image-b5d33b-1565709376163)]

?這里會更壞天軟件桌硫。重要的是我們要做得更好夭咬，因為如果我們不這樣做，并且隨著軟件變得更加復雜和連接 - 因為它控制了更多關鍵功能 - 那些日子可能會變得更糟鞍泉。

問題是程序員很難跟上他們自己的創(chuàng)作皱埠。自20世紀80年代以來，程序員的工作方式和他們使用的工具變化非常小咖驮。有一個小但不斷增長的合唱，擔心現(xiàn)狀是不可持續(xù)的训枢⊥行蓿“即使是非常優(yōu)秀的程序員也在努力理解他們正在使用的系統(tǒng)，”作為微軟Visual Studio工作的軟件開發(fā)人員Chris Granger說道恒界，這個IDE每年花費1199美元睦刃，幾乎被使用三分之一的專業(yè)程序員。他告訴我十酣，當他在微軟時涩拙，他安排了Visual Studio的端到端研究际长，這是迄今為止唯一的研究。在一個半月的時間里兴泥，當人們編寫代碼時工育，他在單向鏡子后面觀看〈瓿梗“他們?nèi)绾问褂霉ぞ呷绯瘢克麄冊趺聪耄俊八f旭贬≌樱“他們怎么樣？坐在電腦前稀轨，他們觸摸鼠標扼脐，不觸摸鼠標嗎？所有這些我們都有教條的事情奋刽，我們實際上并沒有憑經(jīng)驗進行測試谎势。“

調(diào)查結果令他驚訝杨名≡嘤埽“Visual Studio是世界上最大的軟件之一，”他說台谍⌒胛梗“這是超過5500萬行代碼。我在這項研究中發(fā)現(xiàn)的其中一件事超過98％完全無關緊要趁蕊。所有這些工作都已付諸實踐坞生，但它錯過了人們面臨的根本問題。我從中拿走的最大的一個就是人們正在腦子里玩電腦掷伙∈羌海“程序員就像是試圖用眼罩玩耍的國際象棋選手 - 他們的大部分心理能量都花在試圖描繪出來的地方是否幾乎沒有任何遺留下來考慮游戲本身。

John Resig在他的學生中注意到了同樣的事情任柜。Resig是一位著名的JavaScript程序員 - 他在所有網(wǎng)站中占據(jù)了一半以上的軟件 - 以及在線教育網(wǎng)站Khan Academy的技術主管卒废。2012年初，他一直在努力學習該網(wǎng)站的計算機科學課程宙地。為什么學習編程這么難摔认？基本問題似乎是代碼是如此抽象。編寫軟件并不像用冰棍棒制作橋梁宅粥，在那里你可以看到木棍并觸摸膠水参袱。要“制作”一個程序，你輸入單詞。當你想改變程序的行為時抹蚀，無論是游戲剿牺，網(wǎng)站，還是物理模擬环壤，你實際改變的是文本晒来。因此，表現(xiàn)良好的學生 - 實際上是唯一幸存下來的學生 - 是那些能夠一步一步地通過該文本的人镐捧，思考計算機的方式潜索，試圖跟蹤每個中間計算。像格蘭杰一樣懂酱，雷吉格開始懷疑它是否必須如此竹习。在過去的40年中，計算機每18個月的功率增加一倍列牺。為什么沒有改變編程整陌？

事實上，他們兩個同時以同樣的方式思考同一個問題并不是巧合瞎领。他們剛剛在蒙特利爾一家名為Bret Victor的計算機研究人員那里泌辫，向一群軟件工程學生發(fā)表了同樣精彩的演講。談話在2012年2月在網(wǎng)上發(fā)布時傳播開來九默，似乎有兩個大膽的主張震放。首先，我們制作軟件的方式從根本上被打破了驼修。第二個是Victor知道如何解決它殿遂。

[圖片上傳失敗...(image-ac7b10-1565709376163)]

[圖片上傳失敗...(image-f11e73-1565709376163)]

Bret victor不喜歡編寫代碼∫腋鳎“聽起來很奇怪墨礁，”他說《停“當我想做一件事恩静，特別是當我想用軟件創(chuàng)造一些東西時，我必須要完成這個最初的厭惡層蹲坷，在那里我不會操縱我想做的東西驶乾，我正在寫一堆文字進入文本編輯器」诰洌“

“有一種非常強烈的信念轻掩，認為這是錯誤的做事方式∨车祝”

維克多擁有大衛(wèi)·福斯特·華萊士（David Foster Wallace）的風采，閃電般的智慧縈繞在一片羞澀的羞澀之下。他今年40歲聚唐，身上留著灰色的痕跡丐重，還有一絲瘦弱的胡須。他的聲音很溫柔杆查，幾乎是悲傷的扮惦，但是他想要分享他腦袋里的東西，當他開始滾動時亲桦，他似乎會跳過音節(jié)崖蜜，仿佛超越了他自己的聲樂機器。

雖然他經(jīng)營著一個研究計算未來的實驗室客峭，但他似乎對技術本身的興趣不如對使用它的人的頭腦感興趣豫领。像任何優(yōu)秀的工具制造商一樣，他有辦法看待技術和人性相等的世界舔琅。他畢業(yè)于加州理工學院電氣工程專業(yè)等恐，并在加州大學伯克利分校畢業(yè)后繼續(xù)在一家開發(fā)音樂合成器的公司工作。這是一個與他的雙重人格完美匹配的問題：他可以花多少時間思考表演者用鍵盤制作音樂的方式 - 它成為他們手的延伸的方式 - 因為他可以考慮數(shù)字信號處理的數(shù)學备蚓。

當他給出了他的名字的演講時课蔬，就像Resig和Granger在2012年初看到的那樣，Victor終于找到了似乎貫穿他所有工作的原則郊尝。（他實際上稱之為“發(fā)明原則”二跋。）原則是：“創(chuàng)作者需要立即與他們正在創(chuàng)造的東西聯(lián)系起來×骰瑁”編程的問題在于它違反了原則扎即。這就是為什么軟件系統(tǒng)如此難以思考，以及如此充滿錯誤的原因：程序員横缔，盯著一頁文本铺遂，從他們實際制作的任何內(nèi)容中抽象出來。

“我們目前關于計算機程序的概念茎刚，”他說襟锐，“直接來自Fortran和ALGOL，在50年代后期膛锭。這些語言是專為打卡而設計的粮坞。“該代碼現(xiàn)在采用C或Java（Fortran和ALGOL的衍生物）等語言在屏幕上的字母形式初狰，而不是一堆帶孔的卡片莫杈，而不是它不會死，也不會間接的奢入。

有一個類似于文字處理筝闹。過去，您在編寫文檔的程序中看到的只是文本本身，要更改布局或字體或邊距关顷，您必須編寫特殊的“控制代碼”或命令糊秆，告訴計算機，例如议双，“文本的這一部分應該用斜體字表示痘番》姹撸”問題是叁执，在打印文檔之前，您無法看到這些代碼的效果隆夯。很難預測你會得到什么宗雇。您必須想象計算機將如何解釋代碼 - 也就是說昂芜，您必須在腦中玩電腦。

然后WYSIWYG（發(fā)音為“wizzywig”）出現(xiàn)了逾礁。它代表“所見即所得”说铃。當你用一條斜體標記一段時，字母就會在屏幕上傾斜嘹履。如果要更改邊距腻扇，可以在屏幕頂部拖動標尺 - 并查看該更改的效果。因此砾嫉，該文件變得像真實的東西幼苛，你可以戳戳和刺激的東西。只是通過觀察你可以判斷你是否做錯了什么焕刮。任何可以在頁面上點擊的人都可以訪問復雜系統(tǒng)的控制 - 文檔的布局和格式化引擎舶沿。

Victor的觀點是編程本身應該是這樣的。對他來說配并，通過盯著文本編輯器括荡，人們正在做重要工作的想法，比如設計自適應巡航控制系統(tǒng)或試圖了解癌癥溉旋，這是令人震驚的畸冲。程序員的正確工作是確保有一天他們不必這樣做。

有先例足以表明這不是一個瘋狂的想法观腊。例如邑闲，Photoshop將強大的圖像處理算法交給那些可能甚至不知道算法是什么的人。這是一個復雜的軟件梧油，但復雜的合成器很復雜苫耸，用戶可以像儀器一樣學習旋鈕，按鈕和滑塊儡陨。Squarespace是一家以播客廣告而聞名的公司褪子，它提供了一種工具量淌，可以讓用戶通過指向和點擊來構建網(wǎng)站，而不是通過在HTML和CSS中編寫代碼褐筛。它足夠強大类少，可以完成曾經(jīng)由專業(yè)網(wǎng)頁設計師完成的工作叙身。

但這些只是少數(shù)幾個例子渔扎。壓倒性的現(xiàn)實是，當有人想用計算機做一些有趣的事情時信轿，他們不得不編寫代碼晃痴。維克多是一個理想主義者，他認為這不僅僅是一個機會财忽，而是一個程序員的道德失敗倘核。他的講話是對武器的呼喚。

其中的核心是一系列演示即彪，試圖展示可用工具對各種問題的原始性 - 電路設計紧唱，計算機動畫，調(diào)試算法 - 以及更好的工具隶校。他的演示是精湛的漏益。諷刺的是，那個俘獲每個人想象力的那個人深胳，其表面上最瑣碎的是那個绰疤。它顯示了一個分屏，其中一側的游戲看起來像馬里奧舞终，而另一側則是控制它的代碼轻庆。隨著維克多改變了代碼，游戲世界中的事物發(fā)生了變化：他減少了一個數(shù)字敛劝，引力的強度余爆，以及馬里奧角色的浮動; 他增加了另一個，球員的速度夸盟，馬里奧在屏幕上比賽蛾方。

假設你想設計一個水平，馬里奧满俗，跳躍反彈烏龜?shù)淖叮瑢?em>只是使之成為一個小通道。游戲程序員習慣于分兩個階段來解決這類問題：首先唆垃，你盯著你的代碼 - 控制馬里奧跳得多高的代碼五芝，他跑得多快，烏龜?shù)谋巢坑卸嗝磸椥?- 并在你的代碼中做了一些修改文本編輯器辕万，用你的想象力來預測它們會產(chǎn)生什么樣的影響枢步。然后沉删，你重播游戲，看看究竟發(fā)生了什么醉途。

CUSEC / Vimeo

維克多想要更直接的東西矾瑰。“如果你有一個及時的過程隘擎，”他說殴穴，指的是馬里奧穿過關卡的路徑，“你想立即看到變化货葬，你必須把時間映射到太空采幌。”他按了一個按鈕震桶，顯示的不僅僅是馬里奧的位置現(xiàn)在休傍，但他將來會在未來的每個時刻：一個影子Marios的曲線延伸到遠處。更重要的是蹲姐，這個投射路徑是被動的：當Victor改變游戲的參數(shù)時磨取，現(xiàn)在通過快速拖動鼠標來控制，路徑的形狀發(fā)生了變化柴墩。這就像是對游戲有一個神奇的看法忙厌。整個問題已經(jīng)減少到使用不同的參數(shù)，就好像調(diào)整立體聲接收器上的水平拐邪，直到你讓馬里奧穿針慰毅。使用正確的界面，幾乎就像你根本不使用代碼一樣;

當觀眾第一次看到這一點時扎阶，他們真的喘不過氣來汹胃。他們知道他們不是在看孩子的游戲，而是他們的行業(yè)未來东臀。大多數(shù)軟件涉及的行為隨著時間的推移以復雜的方式展開着饥，而且Victor已經(jīng)表明，如果你有足夠的想象力惰赋，你可以開發(fā)出看待這種行為并改變它的方法宰掉，就像在你手中玩它一樣。一位看過這個演講的程序員后來寫道：“突然之間赁濒，我的所有工具都過時了轨奄。”

[圖片上傳失敗...(image-80f0c6-1565709376163)]

[圖片上傳失敗...(image-eb21ce-1565709376163)]

當John Resig看到“發(fā)明原則”的談話時拒炎，他取消了他對可汗學院編程課程的計劃挪拟。他希望網(wǎng)站的編程練習能像Victor的演示一樣工作。在左側击你，你有代碼玉组，右邊是正在運行的程序：圖片或游戲或模擬谎柄。如果您更改了代碼，它會立即更改圖片惯雳〕祝“在一個真正響應的環(huán)境中，”Resig寫道石景，“你可以徹底改變學生如何學習的模型...... [他們]現(xiàn)在可以立即看到結果并直觀地了解底層系統(tǒng)如何在沒有明確遵循的情況下工作“可汗學院已成為世界上最大的計算機編程課程劈猿，平均每個月有100萬學生積極使用該計劃。

曾在微軟Visual Studio工作過的Chris Granger同樣受到啟發(fā)鸵钝。在看到Victor的演講視頻后的幾天內(nèi)糙臼，他在2012年1月建立了一個新編程環(huán)境的原型。它的關鍵功能是它可以為您提供有關您的程序行為的即時反饋恩商。您可以在控制它的代碼旁邊看到您的系統(tǒng)正在做什么。這就像脫掉眼罩一樣必逆。格蘭杰稱這個項目為“光桌”怠堪。

2012年4月，他在Kickstarter上尋求Light Table的資金名眉。在編程界粟矿，這是一種感覺。在一個月內(nèi)损拢，該項目籌集了超過20萬美元陌粹。思想傳播開來。活躍的概念福压，即能夠立即看到流經(jīng)您程序的數(shù)據(jù)掏秩，已經(jīng)成為Google和Apple提供的旗艦編程工具。制作新的iPhone和Mac應用程序的默認語言荆姆，稱為Swift蒙幻，由Apple開發(fā)，以支持一個名為Playgrounds的環(huán)境胆筒，該環(huán)境直接受Light Table的啟發(fā)邮破。

但看到他的談話最終產(chǎn)生的影響，布雷特維克多失望了仆救∈愫停“很多事情似乎都是對我所說的錯誤解釋，”他后來說道彤蔽。當人們開始邀請他參加會議討論編程工具時摧莽，他知道出了什么問題∶螅“每個人都認為我對編程環(huán)境很感興趣范嘱，”他說送膳。他真的對人們?nèi)绾慰创屠斫庀到y(tǒng)感興趣 - 正如他所說的那樣，在“動態(tài)行為的可視化表示”中丑蛤。雖然代碼越來越成為創(chuàng)建動態(tài)行為的首選工具叠聋，但它仍然是理解最糟糕的工具之一。它受裹÷挡梗“基于原理的發(fā)明”的觀點是，通過在系統(tǒng)的行為與其代碼之間立即建立連接棉饶，可以緩解這個問題厦章。

在一對后來的談話中，“停止繪制死魚”和“繪制動態(tài)可視化”照藻，維克多進一步說袜啃。他演示了他構建的兩個程序 - 第一個用于動畫師的程序，第二個用于科學家試圖可視化他們的數(shù)據(jù) - 每個程序都采用了一個過程幸缕，過去曾經(jīng)涉及編寫大量自定義代碼并將其縮小為在WYSIWYG界面中玩游戲群发。Victor建議，對于今天編寫代碼的幾乎所有問題发乔，都可以采用相同的技巧熟妓。“我不確定編程必須存在栏尚，”他告訴我起愈。“或者至少是軟件開發(fā)人員译仗√洌”在他看來，軟件開發(fā)人員的正確角色是創(chuàng)建工具古劲，消除對軟件開發(fā)人員的需求斥赋。只有這樣，具有最緊急計算問題的人才能夠直接掌握這些問題产艾，而不需要中間代碼疤剑。

當然，要做到這一點闷堡，你必須讓程序員自己參與進來隘膘。在最近的一篇文章中，維克托懇求專業(yè)軟件開發(fā)人員停止將他們的才能投入到構建Snapchat和Uber等應用程序的工具中杠览⊥渚眨“日常生活的不便不是重大問題，”他寫道踱阿。相反管钳，他們應該把重點放在科學家和工程師身上 - 正如他向我所說的那樣钦铁，“這些人正在做的工作實際上很重要，而且非常重要才漆，并且使用真正非常糟糕的工具牛曹。”這類令人興奮的工作醇滥，特別是他寫道黎比，“基于模型的設計”的工具類已經(jīng)在進行中，并且已經(jīng)存在多年鸳玩，但大多數(shù)程序員對此一無所知阅虫。

[圖片上傳失敗...(image-23dfb1-1565709376163)]

[圖片上傳失敗...(image-8e5d95-1565709376163)]

“你真的很看重你所擁有的所有工業(yè)產(chǎn)品，你正在使用的不跟，公司正在使用的產(chǎn)品颓帝，你所擁有的唯一非工業(yè)產(chǎn)品是代碼」＃”EricBantégnie是Esterel Technologies（現(xiàn)為AN??SYS所有）的創(chuàng)始人躲履，這是一家法國公司，生產(chǎn)用于構建安全關鍵軟件的工具聊闯。像Victor一樣，Bantégnie并不認為工程師應該通過在IDE中鍵入數(shù)百萬行代碼來開發(fā)大型系統(tǒng)米诉×馐撸“沒有人會手工制造汽車，”他說史侣∷┟冢“在許多地方，守則仍然是手工藝品惊橱。當您手動編寫10,000行代碼時蚪腐，這沒關系。但是你的系統(tǒng)擁有3000萬行代碼税朴，比如空中客車回季，或者有1億行代碼，比如你的特斯拉或高端汽車 - 這些都變得非常非常復雜正林。

Bantégnie的公司是基于模型設計的工業(yè)應用的先驅(qū)之一泡一，您不再直接編寫代碼。相反觅廓，您創(chuàng)建了一種描述程序應遵循的規(guī)則（“模型”）的流程圖鼻忠，并且計算機根據(jù)這些規(guī)則為您生成代碼。例如杈绸，如果您正在為電梯制作控制系統(tǒng)帖蔓，一條規(guī)則可能是當門打開時矮瘟，有人按下大廳按鈕時，您應關閉門并開始移動汽車塑娇。在基于模型的設計工具中澈侠，您可以用一個小圖表示這個規(guī)則，就像在白板上繪制邏輯一樣钝吮，由表示不同狀態(tài)的框組成 - 如“門打開”埋涧，“移動”和“門”關閉“ - 以及定義如何從一個州到另一個州的行。圖表使系統(tǒng)的規(guī)則變得明顯：

這不是Photoshop奇瘦。當然棘催，Photoshop的美妙之處在于，您在屏幕上操作的圖片是最終產(chǎn)品耳标。相比之下醇坝，在基于模型的設計中，屏幕上的圖片更像是藍圖次坡。盡管如此呼猪，以這種方式制作軟件在質(zhì)量上與傳統(tǒng)節(jié)目不同。在傳統(tǒng)編程中砸琅，您的任務是采用復雜的規(guī)則并將其轉換為代碼; 你的大部分精力花在翻譯上宋距，而不是考慮規(guī)則本身。在基于模型的方法中症脂，您擁有的就是規(guī)則谚赎。這就是你花時間思考的問題。這是一種不太關注機器的方式诱篷，更多的是關注你試圖解決它的問題壶唤。

“通常軟件編碼的主要問題 - 我自己也是編碼器，”Bantégnie說棕所，“這不是編碼員的技能闸盔。人們知道如何編碼。問題是如何編碼琳省。因為大多數(shù)要求都是一種自然語言迎吵，含糊不清，而且要求從來都不是非常精確岛啸，所以應該對那些應該編碼的人有不同的理解钓觉。“

根據(jù)這種觀點坚踩，因為用于描述軟件什么媒體軟件變得不守規(guī)矩應該對話荡灾，文字描述，圖紙上的一張紙- -從描述什么軟件媒體太不一樣了做不會做的，即代碼本身批幌。從一個到另一個失去了太多础锐。基于模型的設計背后的想法是縮小差距荧缘。系統(tǒng)設計人員使用相同的模型來表達他們想要的內(nèi)容皆警，并通過計算機自動生成代碼。

當然截粗，要使這種方法取得成功信姓，大部分工作必須在項目開始之前完成。首先绸罗，有人必須構建一個工具來開發(fā)對人們來說很自然的模型 - 感覺就像他們自己制作的筆記和繪圖一樣 - 同時仍然足以讓計算機理解意推。他們必須制作一個程序，將這些模型轉化為真實的代碼珊蟀。最后菊值，他們必須證明生成的代碼將始終按照預期執(zhí)行∮模“幸運的是腻窒，我們已經(jīng)從20年的初期背景工作中受益，”Bantégnie說道磅崭。

Esterel Technologies于2012年被ANSYS收購儿子，源于法國核能和航空航天業(yè)在20世紀80年代開始的研究，他們擔心隨著安全關鍵代碼的復雜性不斷增加砸喻，越來越難以保持其自由典徊。錯誤《鞴唬“我從1988年開始，”法國戰(zhàn)斗機和商用飛機制造商達索航空公司科學研究負責人Emmanuel Ledinot說羡铲》渫埃“那時，我正在研究軍事航空電子系統(tǒng)也切。負責集成系統(tǒng)和調(diào)試它們的人已經(jīng)注意到錯誤的數(shù)量正在增加扑媚。“80年代雷恃，飛機上的機載計算機數(shù)量激增〗桑現(xiàn)在有幾十個，而不是單個飛行計算機倒槐，每個都負責與控制旬痹，導航和通信相關的高度專業(yè)化的任務。當傳感器輸入數(shù)據(jù)并且飛行員輸入命令時，協(xié)調(diào)這些系統(tǒng)飛行飛機需要一個完美定時反應的交響樂两残∮酪悖“在正確的時間以正確的順序處理這些數(shù)百甚至數(shù)千個可能發(fā)生的事件，”Ledinot說人弓，“被診斷為導致臭蟲膨脹的主要原因沼死。”

Ledinot決定手工編寫這樣復雜的代碼不再具有可持續(xù)性崔赌。很難理解它在做什么意蛀，幾乎不可能驗證它能否正常工作。他去尋找新的東西健芭∠卦浚“你必須明白，在這樣的過程中改變工具是非常昂貴的吟榴，”他在一次談話中說魁蒜。“除非你的背靠墻吩翻，否則你不會采取這種決定兜看。”

他開始與法國計算機研究中心INRIA的計算機科學家Gerard Berry合作開發(fā)一個名為Esterel的工具 - 一個法語的“實時”.Eteterel背后的想法是狭瞎，傳統(tǒng)的編程語言可能是適合描述以預定順序發(fā)生的簡單程序 - 比如食譜 - 如果你試圖在幾乎任何時候都可能發(fā)生很多事件的系統(tǒng)中使用它們细移，幾乎任何順序 - 比如飛機的駕駛艙 - 你不可避免地弄得一團糟 而控制軟件的混亂是危險的。在一篇論文中熊锭，Berry甚至預測“低級編程技術不會被大型安全關鍵程序所接受弧轧，因為它們使行為理解和分析幾乎不可行⊥胍螅”

Esterel旨在讓計算機為您處理這種復雜性精绎。這就是基于模型的方法的承諾：您不是編寫正常的編程代碼，而是創(chuàng)建了系統(tǒng)行為的模型 - 在這種情況下锌妻，模型側重于如何處理單個事件代乃，如何確定事件的優(yōu)先級，依賴于哪些事件其他人仿粹，等等搁吓。該模型成為計算機用于進行實際編程的詳細藍圖。

Ledinot和Berry工作了將近10年吭历，以使Esterel達到可以用于生產(chǎn)的程度堕仔。“在2002年晌区，我們擁有了第一個具有自動代碼生成功能的操作軟件建模環(huán)境摩骨，”Ledinot告訴我通贞，“并且是陣風飛機中的第一個嵌入式模塊》峦蹋”今天滑频，ANSYS SCADE產(chǎn)品系列（用于“安全”） - 關鍵應用程序開發(fā)環(huán)境“）用于生成航空航天和國防工業(yè)，核電站唤冈，運輸系統(tǒng)峡迷，重工業(yè)和醫(yī)療設備中的公司的代碼∧愫纾“我最初的夢想是在世界各個平面上都有SCADE生成的代碼绘搞，”Esterel Technologies的創(chuàng)始人Bantégnie表示，“我們離這個目標并不太遠傅物『幌剑”幾乎所有的安全關鍵代碼都在空中客車A380，包括控制飛機飛行表面的系統(tǒng)董饰，

對于客戶蒿褂，尤其是航空客戶而言，部分吸引力在于盡管可以手工構建高度可靠的軟件卒暂，但這可能是一項艱巨的任務啄栓。Meggitt PLC集團軟件工程副總裁Ravi Shivappa是ANSYS客戶，負責制造飛機部件也祠，如發(fā)動機氣動火災探測器昙楚，他解釋說，傳統(tǒng)項目以英文版的大量需求文件開頭诈嘿，該文件規(guī)定了軟件應該做的所有事情堪旧。（要求可能類似于，“當本節(jié)中的壓力超過閾值時奖亚，打開安全閥淳梦，除非手動超控開關打開∥糇郑”）以這種方式描述要求的問題在于谭跨，當您實施時他們在代碼中，你必須煞費苦心地檢查每個人是否滿意李滴。當客戶改變要求時，

嚴格的監(jiān)管標準加劇了成本蛮瞄。美國聯(lián)邦航空局對軟件安全感到狂熱所坯。該機構要求對安全關鍵軟件的每個要求都可追溯到實現(xiàn)它的代碼行，反之亦然挂捅。因此芹助，每當一行代碼發(fā)生變化時，必須將其回溯到設計文檔中的相應要求，并且您必須能夠證明代碼實際滿足要求状土。這個想法是无蜂，如果出現(xiàn)問題，你就能弄明白為什么; 這種做法為大型代碼庫帶來了秩序和責任蒙谓。但是斥季，Shivappa說，“這是一個非常勞動密集型的過程累驮『ㄇ悖”他估計，在使用基于模型的設計之前谤专，在一個為期兩年的項目中躁锡，只花了兩到三個月的時間來編寫代碼 - 剩下的就花在了文件。

正如Bantégnie所解釋的那樣置侍，讓計算機將你的需求轉化為代碼而不是人類的美妙之處在于你可以確定 - 實際上你可以在數(shù)學上證明 - 生成的代碼實際上滿足了這些要求映之。基于模型的方法的許多好處來自于能夠動態(tài)添加需求蜡坊，同時仍然確保滿足現(xiàn)有需求; 每次更改杠输，計算機都可以驗證您的程序是否仍然有效。您可以自由地調(diào)整您的藍圖算色，而不必擔心會引入新的錯誤抬伺。按照美國聯(lián)邦航空局的說法，您的代碼“通過施工來糾正”灾梦。

盡管如此峡钓，大多數(shù)軟件，即使是在安全癡迷的航空世界中若河，都是以老式的方式制作能岩，工程師在散文中編寫他們的要求，程序員用像C這樣的編程語言對它們進行編碼萧福。正如Bret Victor在他的論文中明確指出的那樣拉鹃。 ，基于模型的設計相對不常見鲫忍「嘌啵“美國聯(lián)邦航空局的許多人認為代碼生成是神奇的，因此需要更嚴格的審查悟民，”Shivappa告訴我坝辫。

大多數(shù)程序員都有同感。他們喜歡代碼射亏。至少他們理解它淘钟。使用“有限狀態(tài)機”和“循環(huán)系統(tǒng)”的數(shù)學方法為您編寫代碼并驗證其正確性的工具聽起來很深奧且難以使用，如果不是太好而不是真的运挫。

這是一種以前發(fā)揮過的模式迟几。只要編程與文字和零的寫入相差甚遠，最大的反對意見就來自程序員。瑪格麗特·漢密爾頓是阿波羅任務中著名的軟件工程師 - 實際上是“軟件工程”這個詞的內(nèi)容 - 告訴我，在1964年她在麻省理工學院德雷珀實驗室的第一年，她記得有一個派系在一起戰(zhàn)斗另一個是關于從“一些非常低的機器語言”過渡到盡可能接近的零和“匯編語言”咐柜。“最低級別的人們正在努力保持它更振。這些論點非常相似：“我們怎么知道匯編語言會做得對嗎炕桨？”

“一邊說，他們的臉變紅了肯腕，他們開始尖叫献宫，”她說。她說她“驚訝于他們有多情緒化”实撒。

達索航空公司的埃馬紐埃爾·萊迪諾特指出姊途，當匯編語言本身被逐步淘汰以支持今天仍然流行的編程語言時，就像C一樣知态，這次匯編程序員對此持懷疑態(tài)度捷兰。他說，難怪“人們不是那么容易過渡到基于模型的軟件開發(fā)：他們認為這是失去控制的另一個機會负敏，甚至比他們已經(jīng)更多贡茅。”

基于模型的設計（有時稱為模型驅(qū)動的工程或MDE）的偏見實際上是根深蒂固的其做，根據(jù)最近的一篇論文顶考，“有人甚至認為，調(diào)查人們對MDE的看法比研究更有必要新的MDE技術妖泄【匝兀“

這聽起來幾乎像個笑話，但對于基于模型的方法的支持者來說蹈胡，重要的一點是：我們已經(jīng)知道如何使復雜的軟件可靠渊季，但在很多地方，我們選擇不這樣做罚渐。為什么却汉？

[圖片上傳失敗...(image-89219e-1565709376163)]

[圖片上傳失敗...(image-286f33-1565709376163)]

在2011年，克里斯·紐科姆曾在亞馬遜工作了近七年荷并，并已躍升為首席工程師病涨。他曾參與過該公司一些最關鍵的系統(tǒng)，包括零售產(chǎn)品目錄和管理世界上每個Kindle設備的基礎設施璧坟。他是高度珍視的亞馬遜網(wǎng)絡服務團隊的領導者既穆，該團隊為網(wǎng)絡上一些最大的資產(chǎn)維護云服務器，如Netflix雀鹃，Pinterest和Reddit幻工。在亞馬遜之前，他幫助建立了世界上最大的在線游戲服務公司Steam的骨干網(wǎng)黎茎。他是那些悄悄地保持互聯(lián)網(wǎng)運行的工程師之一囊颅。他所研究的產(chǎn)品被認為是巨大的成功。但他所能想到的是傅瞻，那些深藏在這些系統(tǒng)設計中的災難是等待發(fā)生的災難踢代。

他在一篇論文中寫道：“人類的直覺很難估計在每秒數(shù)百萬次請求操作的系統(tǒng)中，所謂的”非常罕見“事件組合的真實概率嗅骄「炜妫“人類的易犯錯誤意味著一些更微妙，更危險的錯誤變成了設計上的錯誤; 代碼忠實地實現(xiàn)了預期的設計溺森，但設計無法正確處理特定的“罕見”場景慕爬。“

Newcombe確信真正關鍵系統(tǒng)背后的算法 - 例如屏积，存儲大量網(wǎng)絡數(shù)據(jù)的系統(tǒng) - 應該不僅僅是好的医窿，而是完美的。一個微妙的錯誤可能是災難性的炊林。但他知道如何找到更難的bug姥卢，特別是當算法變得越來越復雜時。你可以做你想要的所有測試渣聚，但你永遠都找不到它們独榴。

這就是為什么他如此感興趣，因為在他正在閱讀的一篇論文的附錄中饵逐，他遇到了一種奇怪的數(shù)學和代碼混合 - 或者看起來像代碼的東西 - 它描述了一種叫做“TLA +”的算法括眠。令人驚訝的是，這種描述被認為在數(shù)學上是精確的：用TLA +編寫的算法原則上可以證明是正確的倍权。在實踐中掷豺，它允許您創(chuàng)建一個真實的問題模型，并不僅徹底薄声，而且詳盡地測試它当船。這正是他一直在尋找的東西：一種用于編寫完美算法的語言。

TLA +默辨，代表“行動的時間邏輯”德频，在精神上類似于基于模型的設計：它是一種用于寫下要求的語言 - TLA +稱它們?yōu)椤耙?guī)范” - 計算機程序。然后缩幸，計算機可以完全驗證這些規(guī)范壹置。也就是說竞思，在你編寫任何代碼之前，你要編寫一個簡潔的程序邏輯大綱钞护，以及你需要滿足的約束（比如說盖喷，如果你是在編程ATM，一個限制可能是你永遠不能撤回同樣的錢兩次從您的支票帳戶）难咕。然后课梳，TLA +會詳盡地檢查您的邏輯是否確實滿足了這些約束。如果沒有余佃，它會告訴你如何違反它們暮刃。

該語言由圖靈獎獲獎計算機科學家Leslie Lamport發(fā)明。憑借大大的白胡子和邋white的白發(fā)爆土，以及大眼鏡后面的善良眼睛椭懊，Lamport看起來可能是美國霍格沃茨的友好教授之一。現(xiàn)在在微軟研究院雾消，他被稱為“分布式系統(tǒng)”理論的先驅(qū)之一灾搏，它描述了由多個部分組成的任何計算機系統(tǒng)，它們相互通信立润。Lamport的工作為許多支持現(xiàn)代網(wǎng)絡的系統(tǒng)奠定了基礎狂窑。

對于Lamport來說，今天軟件充滿漏洞的一個主要原因是程序員直接編寫代碼桑腮。他在一篇文章中寫道：“建筑師在鋪設磚塊或錘釘之前會制定詳細的計劃泉哈。” “但是很少有程序員甚至在開始編碼之前寫下他們的程序?qū)鍪裁吹拇致圆輬D破讨〈曰蓿”程序員被編程的細節(jié)所吸引，因為代碼是使程序運行的原因; 花時間在其他任何事情上似乎都會分散注意力提陶。并且通過迷惑代碼的微觀機制烫沙，可以獲得耐心的快樂，一種冥想的滿足感隙笆。但Lamport認為锌蓄，代碼從來就不是一種思想媒介〕湃幔“當你用編程語言思考時瘸爽，它確實限制了你思考的能力，”他說铅忿。代碼讓你錯過樹林：它將您的注意力集中在各個部分的工作上剪决，而不是更深入地了解您的程序如何組合在一起，或者它應該做什么 - 以及它是否真正按照您的想法行事。這就是Lamport創(chuàng)造TLA +的原因柑潦。與基于模型的設計一樣享言，TLA +將您的注意力集中在系統(tǒng)的高級結構，即其基本邏輯渗鬼，而不是實現(xiàn)它的代碼担锤。

Newcombe和他在亞馬遜的同事將繼續(xù)使用TLA +在主要系統(tǒng)中發(fā)現(xiàn)微妙的關鍵錯誤，包括S3背后的核心算法中的錯誤乍钻，被認為可能是世界上最可靠的存儲引擎。它現(xiàn)在在公司廣泛使用铭腕。在曾經(jīng)使用過TLA +的微小人群中银择，他們的成功并不那么罕見。微軟的一名實習生使用TLA +來捕捉一個可能導致世界上每個Xbox在使用四個小時后崩潰的錯誤累舷。歐洲航天局的工程師使用它來重寫碼浩考，操作系統(tǒng)是第一個在彗星上輕輕降落的探測器，其編碼少了10倍被盈。英特爾定期使用它來驗證其芯片析孽。

但是TLA +只占據(jù)主流的一個小角落，如果它可以說占據(jù)了那里的任何空間只怎。即使對于像Newcombe這樣經(jīng)驗豐富的工程師來說袜瞬，這種語言最初也是一種奇異而神秘的東西 - 一個象征動物園。對于Lamport來說身堡，這是教育的失敗邓尤。雖然編程誕生于數(shù)學，但它已經(jīng)基本上脫離了它贴谎。大多數(shù)程序員都不太熟悉數(shù)學 - 邏輯和集合理論 - 大多數(shù) - 你需要使用TLA +汞扎。“很少有程序員 - 包括很少的編程老師 - 了解最基本的概念以及它們在實踐中的應用方式擅这。他們似乎認為他們所需要的只是代碼澈魄，“Lamport說≈亵幔“這個想法比你需要能夠準確思考的代碼有更高的級別痹扇，并且數(shù)學實際上允許你精確地思考它，只是完全是外來的谭确。因為他們從未學過它帘营。“

Lamport認為逐哈，未能在數(shù)學上思考他們正在做什么作為現(xiàn)代軟件開發(fā)的問題芬迄，簡而言之：風險不斷增加，但程序員并沒有加強 - 他們還沒有開發(fā)出處理日益復雜的問題所需的印章昂秃≠魇幔“在15世紀杜窄，”他說，“人們習慣于在不知道微積分的情況下建造大教堂算途，而現(xiàn)在我認為你不允許任何人在不知道微積分的情況下建造大教堂塞耕。我希望經(jīng)過一段相當長的一段時間后，如果他們不理解這些簡單的事情嘴瓤，就不會允許人們編寫程序扫外。“

Newcombe并不確定這是程序員的責任廓脆∩秆瑁“我從Leslie那里聽說他認為程序員害怕數(shù)學。我發(fā)現(xiàn)程序員不知道 - 或者不相信 - 數(shù)學可以幫助他們處理復雜性停忿。復雜性是程序員面臨的最大挑戰(zhàn)驾讲。“他說席赂，讓人們使用TLA +的真正問題是讓他們相信這不會浪費他們的時間吮铭。程序員作為一個物種，是無情務實的颅停。像TLA +象牙塔一樣的工具谓晌。當程序員遇到“正式方法”（所謂的因為它們涉及數(shù)學，“正式”精確的程序描述）時便监，他們根深蒂固的本能就是反沖扎谎。

大多數(shù)在大學學習計算機科學的程序員都曾短暫地遇到過正式方法。通常它們會在一些微不足道的東西上展示出來烧董，就像一個從零開始計算的程序; 學生的工作是在數(shù)學上證明該程序確實從零開始計算毁靶。

“我需要改變?nèi)藗儗φ椒椒ǖ目捶ǎ盢ewcombe告訴我逊移。甚至Lamport本人似乎也沒有完全掌握這一點：正式方法存在圖像問題预吆。修復它的方法不是要求程序員改變 - 改變自己。Newcombe意識到要將TLA +等工具帶入編程主流胳泉，你必須開始講他們的語言拐叉。

一方面，他說扇商，當他向亞馬遜的同事介紹TLA +時凤瘦，他會避免告訴他們它代表什么，因為他害怕這個名字讓它看起來不必要地禁止：“行動的時間邏輯”恰恰就是那種高調(diào)的在學術界發(fā)揮得很好案铺，但推遲了大多數(shù)練習程序員蔬芥。他還試圖不使用“正式”，“驗證”或“證明”這兩個術語，這些術語提醒程序員進行繁瑣的課堂練習笔诵。相反返吻，他將TLA +作為一種新的“偽代碼”，一種真實代碼的踏腳石乎婿，讓你能夠詳盡地測試你的算法 - 這讓你在設計過程中盡早思考测僵。“工程師在調(diào)試方面考慮而不是'驗證'谢翎，”他寫道捍靠，所以他將這個主題的內(nèi)部談話稱為亞馬遜工程師“調(diào)試設計”∩“而不是哀嘆程序員用代碼看世界的事實剂公，Newcombe接受了它。他知道他會失去他們吊宋。“我有一群人說颜武，'現(xiàn)在我明白了璃搜，'”Newcombe說。

此后他離開亞馬遜去甲骨文鳞上，在那里他能夠說服他的新同事嘗試TLA +这吻。對他來說，使用這些工具現(xiàn)在是一個責任問題篙议⊥倥矗“我們需要在這方面做得更好，”他說鬼贱。

“我是自學成才移怯，從九歲開始編碼，所以我的直覺就是開始編碼这难。這是我的唯一 - 這是我的思維方式：你會畫一些東西舟误，嘗試一些東西，你會有機地進化它姻乓∏兑纾“在他看來，這就是今天許多程序員仍在做的事情蹋岩±挡荩“他們谷歌，他們看看Stack Overflow”（一個流行的網(wǎng)站剪个，程序員回答彼此的技術問題）“他們得到了代碼片段秧骑，以解決他們在這個小功能中的戰(zhàn)術問題，并將它們粘合在一起，并進行迭代腿堤》Щ担”

“在你遇到真正的問題之前，這一切都很好笆檀〖商茫”

[圖片上傳失敗...(image-115f54-1565709376163)]

[圖片上傳失敗...(image-5187e-1565709376163)]

在2015年夏天，一對美國安全研究人員Charlie Miller和Chris Valasek確信汽車制造商沒有嚴重控制軟件缺陷酗洒，證明2014年的Jeep Cherokee可以被黑客遠程控制士修。他們充分利用了汽車的娛樂系統(tǒng)，它具有蜂窩連接（例如樱衷，你可以用你的iPhone開車）棋嘲，它連接到更多的中央系統(tǒng)，比如控制擋風玻璃刮水器的系統(tǒng)矩桂，轉向沸移，加速和制動（例如，您可以在后視屏幕上看到在轉動車輪時響應的指南）侄榴。作為他們在夜晚和周末發(fā)展的攻擊的證據(jù)雹锣，當記者在高速公路上駕駛它時，他們侵入了米勒的車癞蚕，并使其變得混亂; 記者蕊爵，

雖然他們實際上沒有創(chuàng)建一個，但他們表明可以編寫一個聰明的軟件桦山，一個“車輛蠕蟲”攒射，它將使用被黑客入侵的吉普切諾基的車載計算機來掃描和攻擊他人; 如果他們想要的話，他們本可以同時進入全國范圍內(nèi)的弱勢汽車和SUV車隊恒水。（至少有五輛菲亞特克萊斯勒車型受到影響会放，其中包括Jeep Cherokee。）有一天钉凌，他們可以告訴他們所有人鸦概，例如，突然向左轉或高速切斷發(fā)動機甩骏。

“我們需要以不同的方式思考軟件窗市，”Valasek告訴我。汽車公司長期以來由數(shù)百家不同供應商生產(chǎn)的零件組裝成品饮笛。但是咨察，這些部件曾經(jīng)是純機械的，現(xiàn)在福青，它們通常會帶有數(shù)百萬行代碼摄狱。雖然這些代碼中的一些 - 用于自適應巡航控制脓诡，用于自動制動和車道輔助 - 確實使汽車更安全（“我的吉普車的安全功能已經(jīng)無數(shù)次拯救了我，”米勒說）媒役，它也創(chuàng)造了一個級別復雜性是全新的祝谚。它使一種新的失敗成為可能。

“車內(nèi)有很多漏洞酣衷，”Esterel背后的法國研究員Gerard Berry在一次談話中說道交惯。“這不像航空電子設備 - 在航空電子設備中穿仪，它非常重視席爽。而且它承認軟件與機制不同“∑“汽車行業(yè)可能是尚未意識到它們實際上屬于軟件業(yè)務的行業(yè)之一只锻。

“我們不會在汽車制造業(yè)中擁有一個知道它正在做什么的軟件安全監(jiān)管機構，”在豐田案中作證的軟件專家邁克爾巴爾說紫谷。他說齐饮，NHTSA“只有有限的軟件專業(yè)知識。他們是從機械歷史中得出的結論笤昨∩蚩螅“使基于模型的設計和代碼生成對航空業(yè)具有吸引力的相同監(jiān)管壓力對汽車制造來說變得越來越慢。達索航空公司（Dassault Aviation）的埃馬紐埃爾·萊迪諾特（Emmanuel Ledinot）推測咬腋，這種差異可能還有經(jīng)濟原因。汽車制造商根本不能將零部件的價格提高幾美分睡互，因為它增加了數(shù)百萬倍; 因此根竿，嵌入汽車中的計算機必須精簡到最低限度，幾乎沒有空間來運行未經(jīng)過手動調(diào)整的代碼就珠。

人們懷疑激勵機制正在發(fā)生變化寇壳。“我認為自動駕駛汽車可能會推動它們妻怎，”Ledinot告訴我 - “ISO 26262和自動駕駛汽車可能會慢慢推動他們對關鍵部件采用這種方法壳炎。”（ISO 26262是2011年發(fā)布的汽車安全標準逼侦。巴爾說了同樣的話：在自動駕駛汽車的世界里匿辩，軟件不能成為事后的想法。它不能像今天的航空公司預訂系統(tǒng)或911系統(tǒng)或股票交易系統(tǒng)那樣建造榛丢。代碼將負責數(shù)億人的生活铲球，并且必須工作。這不是一項小任務晰赞。

“計算基本上是看不見的稼病，”Gerard Berry在他的演講中說选侨。“當你的輪胎是平的時然走，你會看到你的輪胎援制，它們是平的。當你的軟件壞了芍瑞，你看你的軟件晨仑，什么也看不見∽那桑“

“所以這是個大問題寻歧。”