• <tr id='raamXT'><strong id='raamXT'></strong><small id='raamXT'></small><button id='raamXT'></button><li id='raamXT'><noscript id='raamXT'><big id='raamXT'></big><dt id='raamXT'></dt></noscript></li></tr><ol id='raamXT'><option id='raamXT'><table id='raamXT'><blockquote id='raamXT'><tbody id='raamXT'></tbody></blockquote></table></option></ol><u id='raamXT'></u><kbd id='raamXT'><kbd id='raamXT'></kbd></kbd>

    <code id='raamXT'><strong id='raamXT'></strong></code>

    <fieldset id='raamXT'></fieldset>
          <span id='raamXT'></span>

              <ins id='raamXT'></ins>
              <acronym id='raamXT'><em id='raamXT'></em><td id='raamXT'><div id='raamXT'></div></td></acronym><address id='raamXT'><big id='raamXT'><big id='raamXT'></big><legend id='raamXT'></legend></big></address>

              <i id='raamXT'><div id='raamXT'><ins id='raamXT'></ins></div></i>
              <i id='raamXT'></i>
            1. <dl id='raamXT'></dl>
              1. <blockquote id='raamXT'><q id='raamXT'><noscript id='raamXT'></noscript><dt id='raamXT'></dt></q></blockquote><noframes id='raamXT'><i id='raamXT'></i>
                軟件開發的世界末日

                標簽:軟件開發 2019-07-24 16:10:35

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

                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在演講中說:“計算基本上是不可見√的。當你的輪胎沒氣時,你會看見它是癟的。當你的軟件出問題了,你看著軟件卻什麽也看不到。”

                “所以這是一個大問題。”

                猜你愛看

                028-8444 9577    15928373167

                微信掃描二維碼
                與銷售顧問咨詢

                電話咨詢 在線咨詢