序
無(wú)利不起早。1月23日4:30起來(lái)趕高鐵去上海，就是為了聽(tīng)鄧輝和孫鳴老師的課。鄧輝老師講了兩個(gè)主題《設(shè)計(jì)的價(jià)值與未來(lái)》和《從問(wèn)題到系統(tǒng)》，孫鳴老師講的是《正確性驅(qū)動(dòng)建模：用TLA+設(shè)計(jì)系統(tǒng)》，都非常精彩。
解決問(wèn)題的途徑
必須用新技術(shù)嗎？
知乎上有一個(gè)討論“為什么有不少互聯(lián)網(wǎng)公司在面對(duì)開(kāi)發(fā)中的問(wèn)題時(shí)，會(huì)傾向于使用新技術(shù)解決？"的帖子，我看大多數(shù)回復(fù)都是說(shuō)新技術(shù)的價(jià)值以及為什么要用新技術(shù)。這里不要糾結(jié)“新技術(shù)”的定義，新出現(xiàn)的新理論、新方法、新工具、新語(yǔ)言等都是這里討論的新技術(shù)范疇。我認(rèn)為作者拋出的這個(gè)問(wèn)題還得仔細(xì)分析，首先”開(kāi)發(fā)中的問(wèn)題“必須都要新技術(shù)來(lái)解決嗎？
比如解決并發(fā)的問(wèn)題就非得用go嗎？Erlang這種支持電信級(jí)高并發(fā)、容錯(cuò)的語(yǔ)言已經(jīng)30多年的歷史，不能算是新技術(shù)吧？退一步說(shuō)，”開(kāi)發(fā)中的問(wèn)題“用現(xiàn)有的語(yǔ)言比如java就不能解決嗎？這里面不可避免的夾雜著“喜新厭舊”、“裝逼”的人性的因素。DevOps被炒得爛的差不多的時(shí)候，現(xiàn)在又開(kāi)始AIOps了，然而DevOps我們搞好了么？
曹沖稱(chēng)象的故事可以給我們很多啟發(fā)。首先要搞清楚為啥要用新技術(shù)，即要問(wèn)自己新的技術(shù)是否能解決目前的問(wèn)題，大部分問(wèn)題是因?yàn)闆](méi)有把握問(wèn)題的本質(zhì)導(dǎo)致。新的技術(shù)，開(kāi)始或許會(huì)簡(jiǎn)單，但是隨著問(wèn)題的深入，后面遇到新的問(wèn)題，那么問(wèn)題固有的困難是什么？這些固有的困難是與編程語(yǔ)言無(wú)關(guān)的。
圖1是我們看到過(guò)各種技術(shù)，不是說(shuō)這些技術(shù)不好，也不是說(shuō)下面的就比上面的技術(shù)更有效，比如我就比較喜歡TDD（測(cè)試驅(qū)動(dòng)開(kāi)發(fā)）的技術(shù)，也喜歡領(lǐng)域驅(qū)動(dòng)的技術(shù)。這里列出這些技術(shù)的目的是想問(wèn)一下，xxx系統(tǒng)要解決的問(wèn)題必須要用這些“時(shí)髦”的技術(shù)嗎？“一寸長(zhǎng)一寸強(qiáng)，一寸短一寸險(xiǎn)”，各個(gè)技術(shù)都有各自的優(yōu)缺點(diǎn)，我們?cè)诮鉀Q問(wèn)題時(shí)需要綜合考慮，達(dá)到一種平衡。
何時(shí)用新技術(shù)？
不是不用新技術(shù)，而是不能不經(jīng)研究而隨便用新技術(shù)。歷史上有很多使用新技術(shù)很好的解決問(wèn)題的故事。
為了研究“動(dòng)量的變化率”，弄清楚速度就能滿足牛頓的要求，而速度是位置的變化率。對(duì)這個(gè)問(wèn)題的研究，使他掌握了揭開(kāi)變化率及其度量的全部秘密的萬(wàn)能鑰匙--微分學(xué)，由變化率產(chǎn)生的“怎樣計(jì)算一個(gè)速度每時(shí)每刻都在變化的運(yùn)動(dòng)質(zhì)點(diǎn)在給定時(shí)間內(nèi)跑過(guò)的全部距離”的問(wèn)題又使牛頓掌握了積分學(xué)。最后，牛頓又發(fā)現(xiàn)了微分學(xué)和積分學(xué)的密切聯(lián)系，這就是“微積分學(xué)的基本定理”，微積分學(xué)的創(chuàng)立，極大地推動(dòng)了數(shù)學(xué)的發(fā)展，過(guò)去很多用初等數(shù)學(xué)無(wú)法解決的問(wèn)題，運(yùn)用微積分，這些問(wèn)題往往迎刃而解。
也有因?yàn)榧夹g(shù)的局限性失敗的例子。寫(xiě)給程序員的范疇論(英文原文)中舉了一個(gè)例子，法國(guó)的博韋有一座未完工的哥特式教堂，它的設(shè)計(jì)企圖在高度與采光方面擊敗所有的教堂，但是建造中卻出現(xiàn)了一系列的崩塌。當(dāng)時(shí)不得不用鋼梁木柱臨時(shí)做成支撐架構(gòu)來(lái)阻止崩塌，但于事無(wú)補(bǔ)，因?yàn)楹芏鄸|西在設(shè)計(jì)上就是錯(cuò)的。這個(gè)例子說(shuō)明，有些事情必須要使用新的技術(shù)、工具才能完成，所以學(xué)習(xí)和應(yīng)用新技術(shù)也是很重要的。
當(dāng)我們?cè)诮鉀Q問(wèn)題的過(guò)程中，發(fā)現(xiàn)解決的問(wèn)題缺少相應(yīng)的技術(shù)和工具時(shí)，這時(shí)就需要研究、創(chuàng)造新的技術(shù)和工具。
什么是設(shè)計(jì)
圖2是我們開(kāi)發(fā)的整個(gè)過(guò)程中設(shè)計(jì)所處的位置。從問(wèn)題、需求、用例、特性到設(shè)計(jì)，然后根據(jù)設(shè)計(jì)通過(guò)人肉生成源代碼，再把源代碼編譯成機(jī)器代碼，最后到機(jī)器硬件執(zhí)行，另一邊是通過(guò)測(cè)試用例驗(yàn)證執(zhí)行的結(jié)果是否正確。這里考慮兩個(gè)問(wèn)題：
- 寫(xiě)測(cè)試用例時(shí)你在想什么？
- 做設(shè)計(jì)時(shí)你在想什么？
考慮圖中測(cè)試、設(shè)計(jì)是一個(gè)什么過(guò)程。我們知道，寫(xiě)測(cè)試用例時(shí)，是先把期望的行為、屬性、約束表達(dá)出來(lái)，然后驗(yàn)證系統(tǒng)運(yùn)行的行為是否和期望的一致，這個(gè)過(guò)程與設(shè)計(jì)方法和語(yǔ)言是沒(méi)有關(guān)系的。從這個(gè)角度來(lái)理解TDD時(shí)，你應(yīng)該能夠明白它的好處，因?yàn)樗彩敲嫦騿?wèn)題約束的，迫使你考慮系統(tǒng)的屬性和約束。再來(lái)看設(shè)計(jì)，設(shè)計(jì)也是針對(duì)系統(tǒng)的行為、屬性和約束進(jìn)行的，在設(shè)計(jì)過(guò)程中會(huì)采用一系列的設(shè)計(jì)方法、原則和模式等，而且還有考慮設(shè)計(jì)的可理解性、模塊化和可擴(kuò)展性等，最后還要考慮使用的編程語(yǔ)言。有些過(guò)程是因?yàn)橛腥说膮⑴c才引入的，而且?guī)в兄饔^性。比如說(shuō)可理解性，你說(shuō)兩行代碼好理解還是十行代碼好理解？這個(gè)是說(shuō)不清楚的，但是如果是一萬(wàn)行肯定不好理解。
其實(shí)設(shè)計(jì)方法、可理解性等都是為了產(chǎn)生可執(zhí)行的代碼服務(wù)的。那么設(shè)計(jì)方法、設(shè)計(jì)原則、設(shè)計(jì)模式又是為了什么呢？
設(shè)計(jì)的價(jià)值
從上圖可以看出，從問(wèn)題內(nèi)在的行為、約束和屬性到產(chǎn)生源代碼之間有一個(gè)鴻溝，目前是不能自動(dòng)完成的。我們根據(jù)系統(tǒng)的行為、約束和屬性選擇一些設(shè)計(jì)方法、原則、模式等，來(lái)指導(dǎo)設(shè)計(jì)方案，形成文字、圖示和原型，然后經(jīng)手工翻譯成源代碼，而設(shè)計(jì)方案的可理解性、模塊化和可擴(kuò)展性等是為人設(shè)計(jì)的，與產(chǎn)生源代碼無(wú)關(guān)。所以設(shè)計(jì)方法、設(shè)計(jì)原則、設(shè)計(jì)模式這些過(guò)程都是為了“半自動(dòng)化”的產(chǎn)生代碼。設(shè)計(jì)->開(kāi)發(fā)->測(cè)試，最后發(fā)現(xiàn)問(wèn)題再反饋到設(shè)計(jì)，這個(gè)迭代循環(huán)的過(guò)程，實(shí)際是一種人參與的強(qiáng)化學(xué)習(xí)的過(guò)程(是不是聽(tīng)著很熟悉^^)。
靠人參與的東西一般都有瓶頸，一旦這些能夠自動(dòng)化，那么原來(lái)人們引以為傲的技術(shù)都將不值一提。
系統(tǒng)的行為、約束和屬性是嚴(yán)格、精確、抽象和簡(jiǎn)潔的，源代碼也是嚴(yán)格、精確、具體的，如果能把設(shè)計(jì)的過(guò)程自動(dòng)化，從系統(tǒng)的行為、約束和屬性能夠直接生成源碼，那么就能消除由人的參與引入的瓶頸，現(xiàn)有的設(shè)計(jì)方法、原則、模式等都不再需要，更不用考慮什么易理解、模塊化、可擴(kuò)展等問(wèn)題(當(dāng)然，一大批程序員就不再需要了)。
設(shè)計(jì)的未來(lái)
AlphaGo的啟發(fā)
我們經(jīng)常說(shuō)設(shè)計(jì)是一門(mén)藝術(shù)，一般當(dāng)我們對(duì)某項(xiàng)技術(shù)還沒(méi)有搞清楚時(shí)都會(huì)說(shuō)它是藝術(shù)。圍棋也一樣，至今已有四千多年的歷史，一直是智慧、藝術(shù)的象征，在AI領(lǐng)域被認(rèn)為是最具挑戰(zhàn)的棋類(lèi)游戲。而當(dāng)AlphaGo擊敗人類(lèi)職業(yè)圍棋選手時(shí)，在全世界引起巨大的轟動(dòng)，而由此引發(fā)的人類(lèi)對(duì)人工智能的恐慌更是前所未有。難道人類(lèi)幾千年來(lái)積累下的智慧在冷冰冰的機(jī)器面前就如此不堪一擊嗎？作為一個(gè)程序員，并不應(yīng)該有太多恐慌。人類(lèi)是有智慧的，能駕馭在某方面能力遠(yuǎn)遠(yuǎn)超越自己的東西。人不會(huì)飛，但是能造出飛機(jī)；人的力氣不夠大，但是可以造出拖拉機(jī)、挖土機(jī)；人走的慢，但是能造出汽車(chē)。如此看來(lái)，人類(lèi)與AlphaGo、AlphaGo Zero比賽下圍棋，與人類(lèi)和汽車(chē)、飛機(jī)比賽誰(shuí)跑的快有何區(qū)別呢？但是人工智能的發(fā)展確實(shí)會(huì)讓某些單一技能的職業(yè)消失。
回歸到我們的正題，對(duì)于設(shè)計(jì)來(lái)講，從AlphaGo我們能得到那些啟發(fā)呢？
AlphaGo在技術(shù)上其實(shí)并沒(méi)有創(chuàng)新，主要還是工程實(shí)踐上的優(yōu)化，其核心框架主要是
- MCTS（蒙特卡羅樹(shù)搜索，統(tǒng)計(jì)學(xué)方法）
- 深度神經(jīng)網(wǎng)絡(luò)（空間太大，模擬啟發(fā)）
- UCB（置信區(qū)間，隨機(jī)選擇概率低的點(diǎn)，鼓勵(lì)創(chuàng)新）
其中深度神經(jīng)網(wǎng)絡(luò)是最可能被取代的，它是一種具體的模擬啟發(fā)的方法，而其它兩種是數(shù)學(xué)方法。
是否可以用AlphaGo的思路解決軟件開(kāi)發(fā)的問(wèn)題？生成源代碼的規(guī)則是否可以自動(dòng)化？
來(lái)看一下AlphaGo解決問(wèn)題的特征。首先，和其它棋類(lèi)一樣，圍棋的目標(biāo)很明確，有明確的判斷輸贏的標(biāo)準(zhǔn)，基于這個(gè)判斷標(biāo)準(zhǔn)就可以給出走棋的好壞；其次， 有生成完整棋局的規(guī)則，圍棋棋局的可能性在 10170數(shù)量級(jí)，比宇宙中的原子數(shù)量為1080還要多的多，也就是說(shuō)圍棋的搜索空間太大，不能靠窮舉的方式，如何在減少搜索空間的前提下又保證解的最優(yōu)是考慮的核心問(wèn)題，深度神經(jīng)網(wǎng)絡(luò)就是解決空間太大的問(wèn)題，而為了像人一樣，有時(shí)需要出＂奇招＂，以便尋找創(chuàng)新，這個(gè)是UCB策略的作用。
在解決軟件開(kāi)發(fā)的問(wèn)題時(shí)，我們是否也可以找到類(lèi)似的方法？前面討論設(shè)計(jì)問(wèn)題的時(shí)候，我們了解到，從設(shè)計(jì)、開(kāi)發(fā)到測(cè)試再反饋到設(shè)計(jì)這樣一個(gè)迭代循環(huán)過(guò)程，實(shí)際是一種人參與的強(qiáng)化學(xué)習(xí)的過(guò)程。也就是說(shuō)在龐大的解的空間逐漸逼近最優(yōu)解的過(guò)程，我們需要找到把人參與的過(guò)程規(guī)則化、自動(dòng)化的方法。
從這些特征給我啟發(fā)：
- 嚴(yán)格、精確的系統(tǒng)規(guī)格說(shuō)明（目標(biāo)）
- 行為、屬性、約束 - 程序?qū)С?、變換（生成規(guī)則)
- 語(yǔ)義模型
- 抽象-精化（Abstraction-Refinement）
- Equational Reasoning
幾個(gè)例子
下面幾個(gè)例子來(lái)理解前面講的目標(biāo)和生成規(guī)則。
Genetic Programming(遺傳編程)
遺傳編程（GP）是機(jī)器學(xué)習(xí)的一種，開(kāi)始于一群由隨機(jī)生成的千百萬(wàn)個(gè)計(jì)算機(jī)程序組成的"人群"，根據(jù)一個(gè)程序完成給定的任務(wù)的能力來(lái)確定某個(gè)程序的適合度，應(yīng)用達(dá)爾文的自然選擇（適者生存）確定勝出的程序。這里“合適度”就是評(píng)價(jià)程序好壞的標(biāo)準(zhǔn)，而其生成規(guī)則則是利用交叉、變異、評(píng)估等操作，是一種自動(dòng)隨機(jī)產(chǎn)生搜索程序的方法，所以最終產(chǎn)生的程序可能完全出乎人的預(yù)料。對(duì)于生物的“優(yōu)勝劣汰”中的“勝”就是交給大自然來(lái)選擇，能生存下來(lái)的就是“勝者”。而遺傳編程中很難找到這樣一種通用的評(píng)估函數(shù)。不管怎樣，遺傳編程已經(jīng)成功地應(yīng)用于許多不同的領(lǐng)域，而且在近幾年中得到了更深入的研究。
上圖是遺傳編程的流程圖，個(gè)體（individual）程序一般用樹(shù)型結(jié)構(gòu)表示，并且有不同類(lèi)型的基因組成。下圖是一個(gè)稱(chēng)為＂two-offspring crossove＂的例子。
Specification As Abstraction
抽象的本質(zhì)
有了嚴(yán)格、精確的系統(tǒng)規(guī)格說(shuō)明，還需要給出其語(yǔ)義模型，然后通過(guò)抽象、精化，再進(jìn)行等價(jià)推理，就可以從規(guī)格說(shuō)明導(dǎo)出程序。
先來(lái)看這樣一段代碼：
if currentLocation() == Korea then
say "?????"
else
say "Hello"
fi
你應(yīng)該很快就能看明白，這個(gè)是在用兩種不同的方式說(shuō)“你好”。if后面是根據(jù)當(dāng)前所處的國(guó)家來(lái)進(jìn)行選擇說(shuō)英語(yǔ)還是韓語(yǔ)。想一下，if后面不僅僅可以根據(jù)國(guó)家來(lái)區(qū)分，還可以有很多其它的條件，從外部的行為來(lái)看，好像就是有時(shí)在說(shuō)韓語(yǔ)，有時(shí)在說(shuō)英語(yǔ)，至于條件的內(nèi)容并不是我們關(guān)心的，就像這樣：
if ??? then
say "?????"
else
say "Hello"
fi
再進(jìn)一步把說(shuō)的內(nèi)容抽象，我們不單單可以打招呼，可以是任何其它事情，即我們不再關(guān)注具體的內(nèi)容，可能是Ｐ也可能是Ｑ：
if ??? then P else Q fi
是否可以再抽象一點(diǎn)？比如，可以簡(jiǎn)化為
P + Q
這樣是不是很抽象，可以表達(dá)的內(nèi)容更多？
關(guān)于語(yǔ)義的抽象可以總結(jié)以下幾點(diǎn)：
- 用不確定性忽略無(wú)關(guān)的行為
- 用狀態(tài)變遷關(guān)系表達(dá)語(yǔ)義
狀態(tài)變遷是初始狀態(tài)到所有可能結(jié)束狀態(tài)的集合。 - 狀態(tài)是變量到值的映射
簡(jiǎn)單來(lái)說(shuō)抽象的本質(zhì)就是不確定性。以前有個(gè)故事說(shuō)有個(gè)人進(jìn)京趕考，問(wèn)一個(gè)算命先生自己能考第幾名，先生沒(méi)有說(shuō)任何話，只是伸出一根手指頭。這可厲害了，考個(gè)第一說(shuō)的也對(duì)，考個(gè)最后也對(duì)，看到抽象的威力了吧:)
語(yǔ)義模型就是系統(tǒng)行為的集合，抽象是這個(gè)集合大小的度量，越抽象，行為集合越大，我們說(shuō)程序A是程序B的抽象，可以記做：
從規(guī)格說(shuō)明導(dǎo)出程序
-
一個(gè)簡(jiǎn)單的語(yǔ)言
-
語(yǔ)義定義
假如我們要用這個(gè)語(yǔ)言實(shí)現(xiàn)如下的規(guī)格說(shuō)明，如何做？
-
句法的精化計(jì)算
-
程序推導(dǎo)
根據(jù)上面的精化計(jì)算規(guī)則：
程序是推導(dǎo)出來(lái)的，其正確性是有保證的。這個(gè)過(guò)程還需要深入閱讀相關(guān)書(shū)籍才能完全明白，文章最后列出了一些書(shū)籍。
Caculating a Compiler
（這部分功力不到，修煉后再詳細(xì)說(shuō)明^^）
一個(gè)簡(jiǎn)單語(yǔ)言的編譯器
語(yǔ)法和語(yǔ)義
data Expr = Val Int | Add Expr Expr
eval :: Expr -> Int
eval (Val n) = n
eval (Add x y) = eval x + eval y
規(guī)格說(shuō)明
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)
通過(guò)這些例子我們相信程序的自動(dòng)導(dǎo)出是有可能的，加上機(jī)器學(xué)習(xí)，就可以有效、快速的生成源代碼。
我們?cè)撊绾巫?/h1>
面向未來(lái)的學(xué)習(xí)
-
系統(tǒng)規(guī)格說(shuō)明
- 離散數(shù)學(xué) - TLA+, Alloy - 清晰、嚴(yán)格的思考和表達(dá) - 可運(yùn)行、可調(diào)試、自動(dòng)窮舉驗(yàn)證的設(shè)計(jì) -
程序語(yǔ)言理論
- 語(yǔ)義學(xué) - 類(lèi)型系統(tǒng) - 編譯和解釋 -
抽象和組合
- Denotational Semantics - Category Theory
如何對(duì)待工作
-
認(rèn)真對(duì)待測(cè)試用例
- 清晰、嚴(yán)格思考表達(dá) - 系統(tǒng)行為、屬性 -
維護(hù)老系統(tǒng)，認(rèn)真分析解決每一個(gè)Bug
- 深入理解系統(tǒng)的行為、屬性和約束 - 收益要遠(yuǎn)大于用新技術(shù)、新語(yǔ)言開(kāi)發(fā)新系統(tǒng) -
以全局的眼光和理論的態(tài)度學(xué)習(xí)“流行”技術(shù)
- 問(wèn)題、團(tuán)隊(duì)、成本、收益等 - 規(guī)范、穩(wěn)定、可控的代碼人肉生成
推薦讀物
