程序與文檔

通過半年的實踐，期間也斷斷續續的在折騰本身所寫的一個文式編程工具。如今能夠正式但不嚴肅的談談對文式編程的一些體會了。

寫程序不難，關鍵是寫出有用的程序。

寫出有用的程序也不難，關鍵是寫出可以讓別人繼續維護下去的程序。

文檔是重要的，沒有文檔，單憑代碼中那些常常很蹩腳的變量名與函數名，每每很難理解一段代碼的功能及用途。$y=ax^2$ 是拋物線吧？那 $E=mc^2$ 是什麼？編程雖然也像數學那樣依賴於符號，但它更像是物理學。

編程語言所提供的註釋機制能夠解釋代碼，可是它不能替代程序文檔。若是將一個程序視爲一部電影，那麼代碼的註釋像是電影裏的旁白，而程序的文檔則是這部電影的劇本。

閱讀沒有文檔的程序源碼，閱讀者弄懂這些源碼的過程，本質上只是爲這些源碼從新撰寫了一份文檔。去爲一份並不是本身編寫的程序源碼重建文檔，困難係數一般遠大於程序源碼的做者本人來寫。

寫文檔，所耗費的精力與時間每每要大於寫編寫程序源碼的時間。這是不少程序缺少文檔——抑或有文檔，可是文檔每每落後於源碼幾個世紀的緣由之一。另一個緣由，寫程序的人多爲理工科出身，文字表達能力一般比較着急。雖然 Knuth 於上個世紀 70 年代就在倡導文學編程的理念，可是迄今爲止還沒據說過哪一個寫程序的人用文學編程寫出了一部發人深省的做品。不過，可能更主要的緣由是，老闆們不會爲此多給錢，甚至會由於你代碼寫的慢而開掉你。

這一現實讓我很差意思在這裏談什麼文學編程，仍是弱化一下，稱之爲『文式編程』更好一些。

按照柯里-霍華德同構定理，寫程序的過程與證實一個數學命題的過程是等價的。也就是說，咱們寫程序，本質上就是一連串的推理過程，當程序可以運行起來，而且可以正確的解決咱們要解決的問題之時，這意味着咱們已經完成了一個數學命題的證實。若是將這個推理的過程用文檔記述下來，而且將程序的源碼也嵌入這個推理的過程之中，做爲每一個推理階段的所得結果，這樣就實現了程序文檔與源碼的融合。這樣的結果一定不是文學做品，而是一篇論文。

每一個人寫程序的過程，實際上是有程序文檔的，只不過他們沒有把它寫出來。他們像拍電影同樣，基於劇本，一個鏡頭一個鏡頭的將電影拍出來，而後燒掉了劇本。

要用好文式編程，必需要按照一個問題的推理順序將文檔與代碼一併寫出來。