程式推導(program derivation)是本書的重要主題。 給定一個待解決的問題，並假設該問題能描述成邏輯、數學、或其他形式語言（稱作一個形式規格(specification)）， 程式推導泛指以嚴謹方式將該規格轉換成一個解決該問題的程式的方法。 指令式語言與函數語言都能做程式推導，而且有許多道理可相通。 本書討論函數語言的程式推導。 一個簡單、典型的函數程式語言推導可能有如下的形式：

  spec
=  {- 性質 1 -}
  e1
=  {- 性質 2 -}
  ....
=  {- 性質 n -}
  en 

其中 spec 是問題的規格，通常也是一個函數語言程式。 根據性質 1, spec 等於 e1；根據性質 2，e1 等於 e2... 長此以往，直到我們導出一個符合我們要求的 en. 光這麼看來，這和我們前幾章作的數學證明似乎沒什麼不同。 差別在於，做證明時我們已有 spec 和 en，要做的是把 spec 到 en 之間的步驟補足。 但做程式推導時，我們是從 spec 出發，希望透過種種跡象找出一個滿意的（可能是夠快的、不佔空間的、或滿足某些其他性質的）en. 當然，找出 en 之後，從 spec 推出 en 的過程就成了 spec = en 的證明。 當程式推導的進行方式類似數學演算，有人可能稱之為程式演算(program calculation)。 本書混用這兩個詞彙，並不區分。

為何做程式推導？第一個理由是我們希望程式正確。 此處「正確」指的是 en 確實滿足了最初的規格 spec。但如果只為了正確性，我們為何不能先無論如何把 en 寫出，再試著證明 spec = en？ 原因之一是通常程式寫好了，大家便不想證它了。 更重要的是：程式開發時，若沒有把「怎麼證明它」列入考量，寫出的程式常常是很難證明的。 為了確保有證明，最好讓「產生證明」這件事成為程式開發過程的一部分，甚至讓證明引導程式的開發。 Dijkstra 說道：

先給一個程式再證明它，在某個意義上是把馬車放在馬前面。 更有希望的做法是讓正確性證明與程式一起長出來： 如此一來，我們能選擇證明的結構，然後設計一個能用這種方法證明出來的程式。 這還有個額外的好處：正確性考量可以成為程式該怎麼寫的引導與啟發。 [Dijkstra 1974]

Dijkstra 的最後一句話帶到了程式推導的第三個理由： 提倡者認為，程式推導的種種方法與技巧可以引導我們去分析、思考、解決問題； 這是解問題、甚至發現新演算法的方法（Backhouse [2003], Backhouse [2011]）。 藉由良好的符號設計，我們可以發現常見的程式推導模式，並將其推廣到其他有類似性質的問題上。

第0 章的結尾說道「函數語言的價值便是：它是個適於演算的語言。」 便於做程式推導，是我覺得函數語言最突出的特質。 我們可以由規格出發、在符號上操作，將程式如同求代數的解一樣地算出來。只要每個小步驟都正確，最後的程式就是正確的。 由第1 章至今，我們做了許多準備工作，備齊需要的基本知識。現在我們終於可以開始做一些演算了。