0.4 抽象化與表達力
在開發較具規模的軟體前，許多軟體方法建議我們分析問題、需求，並寫成形式化的規格。例如，Abrial [1996] 的 B method 是以一套基於集合論與一階邏輯的形式語言描述軟體規格的方法。 這是一種抽象化。面對真實的問題時，這一步不容易。
我們再回到蘋果的例子，回想起在該例中，我們選擇抽取出和值有關的資訊，而拋棄了許多其他：因果、先後順序... 等等。
在某些問題或應用中，因果或時間順序是否有可能是重要的？確實有。解這些問題時，我們可能在中途發現選錯了抽象的方式，使得留下的資訊不足以解決該問題。於是我們只好重新開始。有時，我們甚至會發現現有的符號不足以表達這些問題，得設計另一套符號。
這讓我們討論到解決問題重要的第零步：在我們能用符號表達問題之前，得先有人設計出一套完善的、足以表達許多問題的符號及其運算規則。為不同目的，我們可能設計不同的符號。一套符號也伴隨著該符號可如何轉變、操作（例如我們見過的交換律、結合律，某些符號碰在一起可化簡、等等）的規則。符號及其規則合起來成為一個「形式(formal)系統」。使用設計過的符號與其規則解決問題的研究被稱作「形式方法(formal method)」。此處的 "formal" 一詞，意指我們利用符號的「形式(form)」來解決問題。大學資訊系所的一門必修課 "formal language" 中的 "formal" 也為「形式」之意。早期台灣將該門課稱為「正規語言」，可能是將 formal 誤解為相對於 casual 的「正式/正規」。
如果我們希望電腦幫我們解問題，需設計的符號就是一套程式語言。這不是一件容易的事：一個程式語言的表達力得強到足以描述所有該語言被設計來解決的問題。一套程式語言是設計者看待世界的抽象觀點。有些程式語言主張世界的狀態可以被一個個指令改變（「把 x 的值更新為 x + y; 在螢幕上畫一個方塊... 」）；有些語言認為世界應該看待為一個個物件；有些語言認為世界是許多彼此傳送訊息的共時程序；有些語言認為只要描述出每個個體之前的邏輯關係，交給電腦推論結果，就是很好的計算模型；本書中將介紹的抽象觀點則主張把一切都看成函數：寫程式是定義函數，圖形是座標到顏色的函數，動畫則是時間到圖形的函數...。
晚近的語言設計，尤其是型別系統的設計，採用了許多邏輯學界的結果。本章談「騎士與惡棍之島」時，使用的是命題邏輯(propositional logic)的一種分支。一套「邏輯」也可視作一群符號以及其規則。許多人可能不知道，邏輯有許多種。命題邏輯是一套簡單的邏輯，其優點是給定任一合法的句子，都有一套機械性作法可得知其成立與否 --- 這個性質稱作「可判定性(decidability)」。但命題邏輯的表達力並不強：許多事情無法在命題邏輯中表達出來。
想表達更細緻的陳述，可使用表達力更強的邏輯。有些邏輯能表達「對所有」、「存在」；有些邏輯能表達先後順序以及「將一直成立」、「將在未來某時間成立」等觀念；有些邏輯可用來表達概念與概念之間的關係。但有得必有失，一套邏輯的表達力只要強到某個程度，就不再有可判定性了，沒有一套固定的方法可知道任意一個邏輯式子的真假。這是理性的限制。在知道形式系統的侷限之下盡力探索並發揮其極限，便是這套學問迷人之處。
因此，設計程式語言時總得掌握這樣的平衡：我們希望語言的表達力強到足以描述我們希望表達的運算程序，但又不希望強到無法掌握其性質。