序
無利不起早介却。1月23日4:30起來趕高鐵去上海谴供，就是為了聽鄧輝和孫鳴老師的課。鄧輝老師講了兩個主題《設計的價值與未來》和《從問題到系統(tǒng)》筷笨，孫鳴老師講的是《正確性驅動建模：用TLA+設計系統(tǒng)》憔鬼，都非常精彩龟劲。
解決問題的途徑
必須用新技術嗎胃夏？
知乎上有一個討論“為什么有不少互聯(lián)網(wǎng)公司在面對開發(fā)中的問題時，會傾向于使用新技術解決昌跌？"的帖子仰禀，我看大多數(shù)回復都是說新技術的價值以及為什么要用新技術。這里不要糾結“新技術”的定義蚕愤，新出現(xiàn)的新理論答恶、新方法、新工具萍诱、新語言等都是這里討論的新技術范疇悬嗓。我認為作者拋出的這個問題還得仔細分析，首先”開發(fā)中的問題“必須都要新技術來解決嗎裕坊？
比如解決并發(fā)的問題就非得用go嗎包竹？Erlang這種支持電信級高并發(fā)、容錯的語言已經(jīng)30多年的歷史籍凝，不能算是新技術吧周瞎？退一步說，”開發(fā)中的問題“用現(xiàn)有的語言比如java就不能解決嗎饵蒂？這里面不可避免的夾雜著“喜新厭舊”声诸、“裝逼”的人性的因素。DevOps被炒得爛的差不多的時候退盯，現(xiàn)在又開始AIOps了彼乌，然而DevOps我們搞好了么泻肯？
曹沖稱象的故事可以給我們很多啟發(fā)。首先要搞清楚為啥要用新技術慰照，即要問自己新的技術是否能解決目前的問題软免，大部分問題是因為沒有把握問題的本質導致。新的技術焚挠，開始或許會簡單膏萧，但是隨著問題的深入，后面遇到新的問題蝌衔，那么問題固有的困難是什么榛泛？這些固有的困難是與編程語言無關的。
圖1是我們看到過各種技術噩斟，不是說這些技術不好曹锨，也不是說下面的就比上面的技術更有效，比如我就比較喜歡TDD（測試驅動開發(fā)）的技術剃允，也喜歡領域驅動的技術沛简。這里列出這些技術的目的是想問一下，xxx系統(tǒng)要解決的問題必須要用這些“時髦”的技術嗎斥废？“一寸長一寸強椒楣，一寸短一寸險”，各個技術都有各自的優(yōu)缺點牡肉，我們在解決問題時需要綜合考慮捧灰，達到一種平衡。
何時用新技術统锤？
不是不用新技術毛俏，而是不能不經(jīng)研究而隨便用新技術。歷史上有很多使用新技術很好的解決問題的故事饲窿。
為了研究“動量的變化率”煌寇，弄清楚速度就能滿足牛頓的要求，而速度是位置的變化率逾雄。對這個問題的研究阀溶，使他掌握了揭開變化率及其度量的全部秘密的萬能鑰匙--微分學，由變化率產(chǎn)生的“怎樣計算一個速度每時每刻都在變化的運動質點在給定時間內跑過的全部距離”的問題又使牛頓掌握了積分學嘲驾。最后淌哟，牛頓又發(fā)現(xiàn)了微分學和積分學的密切聯(lián)系，這就是“微積分學的基本定理”辽故，微積分學的創(chuàng)立徒仓，極大地推動了數(shù)學的發(fā)展，過去很多用初等數(shù)學無法解決的問題誊垢，運用微積分掉弛，這些問題往往迎刃而解症见。
也有因為技術的局限性失敗的例子。寫給程序員的范疇論(英文原文)中舉了一個例子殃饿，法國的博韋有一座未完工的哥特式教堂谋作，它的設計企圖在高度與采光方面擊敗所有的教堂，但是建造中卻出現(xiàn)了一系列的崩塌乎芳。當時不得不用鋼梁木柱臨時做成支撐架構來阻止崩塌遵蚜，但于事無補，因為很多東西在設計上就是錯的奈惑。這個例子說明吭净，有些事情必須要使用新的技術、工具才能完成肴甸，所以學習和應用新技術也是很重要的寂殉。
當我們在解決問題的過程中，發(fā)現(xiàn)解決的問題缺少相應的技術和工具時原在，這時就需要研究友扰、創(chuàng)造新的技術和工具。
什么是設計
圖2是我們開發(fā)的整個過程中設計所處的位置庶柿。從問題村怪、需求、用例澳泵、特性到設計实愚，然后根據(jù)設計通過人肉生成源代碼，再把源代碼編譯成機器代碼兔辅，最后到機器硬件執(zhí)行，另一邊是通過測試用例驗證執(zhí)行的結果是否正確击喂。這里考慮兩個問題：
- 寫測試用例時你在想什么维苔？
- 做設計時你在想什么？
考慮圖中測試懂昂、設計是一個什么過程介时。我們知道，寫測試用例時凌彬，是先把期望的行為沸柔、屬性、約束表達出來铲敛，然后驗證系統(tǒng)運行的行為是否和期望的一致褐澎，這個過程與設計方法和語言是沒有關系的。從這個角度來理解TDD時伐蒋，你應該能夠明白它的好處工三，因為它也是面向問題約束的迁酸，迫使你考慮系統(tǒng)的屬性和約束。再來看設計俭正，設計也是針對系統(tǒng)的行為奸鬓、屬性和約束進行的，在設計過程中會采用一系列的設計方法掸读、原則和模式等串远，而且還有考慮設計的可理解性、模塊化和可擴展性等儿惫，最后還要考慮使用的編程語言抑淫。有些過程是因為有人的參與才引入的，而且?guī)в兄饔^性姥闪。比如說可理解性始苇，你說兩行代碼好理解還是十行代碼好理解？這個是說不清楚的筐喳，但是如果是一萬行肯定不好理解催式。
其實設計方法、可理解性等都是為了產(chǎn)生可執(zhí)行的代碼服務的避归。那么設計方法荣月、設計原則、設計模式又是為了什么呢梳毙？
設計的價值
從上圖可以看出哺窄，從問題內在的行為、約束和屬性到產(chǎn)生源代碼之間有一個鴻溝账锹，目前是不能自動完成的萌业。我們根據(jù)系統(tǒng)的行為、約束和屬性選擇一些設計方法奸柬、原則生年、模式等，來指導設計方案廓奕，形成文字抱婉、圖示和原型，然后經(jīng)手工翻譯成源代碼桌粉，而設計方案的可理解性蒸绩、模塊化和可擴展性等是為人設計的，與產(chǎn)生源代碼無關铃肯。所以設計方法患亿、設計原則、設計模式這些過程都是為了“半自動化”的產(chǎn)生代碼缘薛。設計->開發(fā)->測試窍育，最后發(fā)現(xiàn)問題再反饋到設計卡睦，這個迭代循環(huán)的過程，實際是一種人參與的強化學習的過程(是不是聽著很熟悉^^)漱抓。
靠人參與的東西一般都有瓶頸表锻，一旦這些能夠自動化，那么原來人們引以為傲的技術都將不值一提乞娄。
系統(tǒng)的行為瞬逊、約束和屬性是嚴格、精確仪或、抽象和簡潔的确镊，源代碼也是嚴格、精確范删、具體的蕾域，如果能把設計的過程自動化，從系統(tǒng)的行為到旦、約束和屬性能夠直接生成源碼旨巷，那么就能消除由人的參與引入的瓶頸，現(xiàn)有的設計方法添忘、原則采呐、模式等都不再需要，更不用考慮什么易理解搁骑、模塊化斧吐、可擴展等問題(當然，一大批程序員就不再需要了)仲器。
設計的未來
AlphaGo的啟發(fā)
我們經(jīng)常說設計是一門藝術煤率，一般當我們對某項技術還沒有搞清楚時都會說它是藝術。圍棋也一樣娄周，至今已有四千多年的歷史涕侈，一直是智慧、藝術的象征煤辨，在AI領域被認為是最具挑戰(zhàn)的棋類游戲。而當AlphaGo擊敗人類職業(yè)圍棋選手時木张，在全世界引起巨大的轟動众辨，而由此引發(fā)的人類對人工智能的恐慌更是前所未有。難道人類幾千年來積累下的智慧在冷冰冰的機器面前就如此不堪一擊嗎舷礼？作為一個程序員鹃彻，并不應該有太多恐慌。人類是有智慧的妻献，能駕馭在某方面能力遠遠超越自己的東西蛛株。人不會飛团赁，但是能造出飛機；人的力氣不夠大谨履，但是可以造出拖拉機欢摄、挖土機；人走的慢笋粟，但是能造出汽車怀挠。如此看來，人類與AlphaGo害捕、AlphaGo Zero比賽下圍棋绿淋，與人類和汽車、飛機比賽誰跑的快有何區(qū)別呢尝盼？但是人工智能的發(fā)展確實會讓某些單一技能的職業(yè)消失吞滞。
回歸到我們的正題，對于設計來講盾沫，從AlphaGo我們能得到那些啟發(fā)呢裁赠？
AlphaGo在技術上其實并沒有創(chuàng)新，主要還是工程實踐上的優(yōu)化疮跑，其核心框架主要是
- MCTS（蒙特卡羅樹搜索组贺，統(tǒng)計學方法）
- 深度神經(jīng)網(wǎng)絡（空間太大，模擬啟發(fā)）
- UCB（置信區(qū)間祖娘，隨機選擇概率低的點失尖，鼓勵創(chuàng)新）
其中深度神經(jīng)網(wǎng)絡是最可能被取代的，它是一種具體的模擬啟發(fā)的方法渐苏，而其它兩種是數(shù)學方法掀潮。
是否可以用AlphaGo的思路解決軟件開發(fā)的問題？生成源代碼的規(guī)則是否可以自動化琼富？
來看一下AlphaGo解決問題的特征仪吧。首先，和其它棋類一樣鞠眉，圍棋的目標很明確薯鼠，有明確的判斷輸贏的標準，基于這個判斷標準就可以給出走棋的好壞械蹋；其次出皇， 有生成完整棋局的規(guī)則，圍棋棋局的可能性在 10170數(shù)量級哗戈，比宇宙中的原子數(shù)量為1080還要多的多郊艘，也就是說圍棋的搜索空間太大，不能靠窮舉的方式，如何在減少搜索空間的前提下又保證解的最優(yōu)是考慮的核心問題纱注，深度神經(jīng)網(wǎng)絡就是解決空間太大的問題畏浆，而為了像人一樣，有時需要出＂奇招＂狞贱，以便尋找創(chuàng)新刻获，這個是UCB策略的作用。
在解決軟件開發(fā)的問題時斥滤，我們是否也可以找到類似的方法将鸵？前面討論設計問題的時候，我們了解到佑颇，從設計顶掉、開發(fā)到測試再反饋到設計這樣一個迭代循環(huán)過程，實際是一種人參與的強化學習的過程挑胸。也就是說在龐大的解的空間逐漸逼近最優(yōu)解的過程痒筒，我們需要找到把人參與的過程規(guī)則化、自動化的方法茬贵。
從這些特征給我啟發(fā)：
- 嚴格簿透、精確的系統(tǒng)規(guī)格說明（目標）
- 行為、屬性解藻、約束 - 程序導出老充、變換（生成規(guī)則)
- 語義模型
- 抽象-精化（Abstraction-Refinement）
- Equational Reasoning
幾個例子
下面幾個例子來理解前面講的目標和生成規(guī)則。
Genetic Programming(遺傳編程)
遺傳編程（GP）是機器學習的一種螟左，開始于一群由隨機生成的千百萬個計算機程序組成的"人群"啡浊，根據(jù)一個程序完成給定的任務的能力來確定某個程序的適合度，應用達爾文的自然選擇（適者生存）確定勝出的程序胶背。這里“合適度”就是評價程序好壞的標準巷嚣，而其生成規(guī)則則是利用交叉、變異钳吟、評估等操作廷粒，是一種自動隨機產(chǎn)生搜索程序的方法，所以最終產(chǎn)生的程序可能完全出乎人的預料红且。對于生物的“優(yōu)勝劣汰”中的“勝”就是交給大自然來選擇坝茎，能生存下來的就是“勝者”暇番。而遺傳編程中很難找到這樣一種通用的評估函數(shù)。不管怎樣，遺傳編程已經(jīng)成功地應用于許多不同的領域，而且在近幾年中得到了更深入的研究厨喂。
上圖是遺傳編程的流程圖，個體（individual）程序一般用樹型結構表示蜕煌，并且有不同類型的基因組成派阱。下圖是一個稱為＂two-offspring crossove＂的例子。
Specification As Abstraction
抽象的本質
有了嚴格斜纪、精確的系統(tǒng)規(guī)格說明贫母，還需要給出其語義模型，然后通過抽象盒刚、精化腺劣，再進行等價推理，就可以從規(guī)格說明導出程序因块。
先來看這樣一段代碼：
if currentLocation() == Korea then
say "?????"
else
say "Hello"
fi
你應該很快就能看明白橘原，這個是在用兩種不同的方式說“你好”。if后面是根據(jù)當前所處的國家來進行選擇說英語還是韓語。想一下，if后面不僅僅可以根據(jù)國家來區(qū)分典予，還可以有很多其它的條件蹬碧，從外部的行為來看，好像就是有時在說韓語首尼，有時在說英語，至于條件的內容并不是我們關心的，就像這樣：
if ??? then
say "?????"
else
say "Hello"
fi
再進一步把說的內容抽象脐帝，我們不單單可以打招呼，可以是任何其它事情甘穿，即我們不再關注具體的內容腮恩，可能是Ｐ也可能是Ｑ：
if ??? then P else Q fi
是否可以再抽象一點？比如温兼，可以簡化為
P + Q
這樣是不是很抽象秸滴，可以表達的內容更多？
關于語義的抽象可以總結以下幾點：
- 用不確定性忽略無關的行為
- 用狀態(tài)變遷關系表達語義
狀態(tài)變遷是初始狀態(tài)到所有可能結束狀態(tài)的集合募判。 - 狀態(tài)是變量到值的映射
簡單來說抽象的本質就是不確定性荡含。以前有個故事說有個人進京趕考，問一個算命先生自己能考第幾名届垫，先生沒有說任何話释液，只是伸出一根手指頭误债。這可厲害了寝蹈，考個第一說的也對，考個最后也對箫老，看到抽象的威力了吧:)
語義模型就是系統(tǒng)行為的集合耍鬓，抽象是這個集合大小的度量笆制，越抽象各薇，行為集合越大峭判，我們說程序A是程序B的抽象林螃，可以記做：
從規(guī)格說明導出程序
-
一個簡單的語言
-
語義定義
假如我們要用這個語言實現(xiàn)如下的規(guī)格說明，如何做谨设？
-
句法的精化計算
-
程序推導
根據(jù)上面的精化計算規(guī)則：
程序是推導出來的，其正確性是有保證的二蓝。這個過程還需要深入閱讀相關書籍才能完全明白指厌，文章最后列出了一些書籍鸥诽。
Caculating a Compiler
（這部分功力不到，修煉后再詳細說明^^）
一個簡單語言的編譯器
語法和語義
data Expr = Val Int | Add Expr Expr
eval :: Expr -> Int
eval (Val n) = n
eval (Add x y) = eval x + eval y
規(guī)格說明
comp :: Expr -> Code
comp' :: Expr -> Code -> Code
exec :: Code -> Stack -> Stack
exec (comp e) s = eval e : s
exec (comp' e c) = exec c (eval e : s)
exec (comp' (Val n) c) s
= {specification of comp'}
exec c (eval (Val n) : s)
= {applying eval}
exec c (n : s)
exec c' s = exec c (n : s)
PUSH :: Int > Code -> Code
exec (PUSH n c) s = exec c (n : s)
exec c (n : s)
= {unapplying exec}
exec (PUSH n c) s
comp' (Val n) c = PUSH n c
data Code
= HALT | PUSH Int Code | ADD Code
comp :: Expr -> Code
comp e = comp' e HALT
comp' :: Expr -> Code -> Code
comp' (Val n) c = PUSH n c
comp' (Add x y) c
= comp' x (comp' y (ADD c))
exec :: Code -> Stack -> Stack
exec HALT s = s
exec (PUSH n c) s = exec c (n : s)
exec (ADD c) (m : n : s)
= exec c (n + m : s)
通過這些例子我們相信程序的自動導出是有可能的，加上機器學習，就可以有效俊鱼、快速的生成源代碼并闲。
我們該如何做
面向未來的學習
-
系統(tǒng)規(guī)格說明
- 離散數(shù)學 - TLA+, Alloy - 清晰帝火、嚴格的思考和表達 - 可運行犀填、可調試九巡、自動窮舉驗證的設計 -
程序語言理論
- 語義學 - 類型系統(tǒng) - 編譯和解釋 -
抽象和組合
- Denotational Semantics - Category Theory
如何對待工作
-
認真對待測試用例
- 清晰冕广、嚴格思考表達 - 系統(tǒng)行為、屬性 -
維護老系統(tǒng)睬辐，認真分析解決每一個Bug
- 深入理解系統(tǒng)的行為何吝、屬性和約束 - 收益要遠大于用新技術瓣喊、新語言開發(fā)新系統(tǒng) -
以全局的眼光和理論的態(tài)度學習“流行”技術
- 問題黔酥、團隊、成本熄求、收益等 - 規(guī)范逗概、穩(wěn)定卿城、可控的代碼人肉生成
推薦讀物
