Why naive program transformation systems are unlikely to work

這篇是 E.W. Dijkstra 對於 program transformation 的小評論，編號 EWD 636。（Dijkstra 的 manuscripts 收集在 E.W. Dijkstra Archive，有空可以上去逛逛。）前面一半介紹 program transformation 並和傳統方法比較，後面一半是 Dijkstra 的質疑。他的主要論點大概有三：

• Derivation 的過程太長，因為已發現的 transformation steps 太過瑣細；
• 正確的 specification 並不見得好寫；
• 從 specification 不一定能透過一條 semantic-preserving path 而抵達理想的演算法。

Dijkstra 針對的應該是（至少接近）「自動的」（機械式的）程式轉換系統，所以第一個論點對 AoP-style derivation 並不造成絕大的衝擊（雖然我覺得的確需要發展更強的定理）。後面兩個就真的比較麻煩，特別是第三個。不知道有沒有人做過這種 "completeness" 的證明？

--
我猜不外乎要重整到 formal logic 或 / 和 lambda calculus 吧？