我先引別人的一句話，“
以太坊上的智能合約既沒有智能也不是合約。”用可編程的計算機語言來表達合約，就存在根本性的約束。譬如，合約寫成代碼后是“定死”了的，哪來的智能。要能隨機應變的智能，必須事先考慮好各種變化的可能。而在現實世界中，再緊湊的合約也有預想不到考慮不周的時候，或者雙方對合約的內容有不同認知。現實世界中合約各方還可以坐下來商量，修改合約。在以太坊上，這些修改和商議或者仲裁的功能怎么實現？
跟隨著以太坊的智能合約被很多人滿嘴跑火車的另外一個詞就是圖靈完整 (Turing Complete)，好像這是個什么偉大的功能。其實若要真的想做智能合約，圖靈完整又是一個背道而馳的思路。為什么這么講？設計過計算機程序設計語言的人都知道，一個程序語言的限制越少，功能越強，程序員越容易出錯。譬如， 大家常用的 C 語言就是這樣一個例子。它功能強，是因為它出身是系統級的語言，做操作系統用的，需要這么強大的靈活性。但是作為寫應用程序的需求來說，可以說到處是陷阱。后來推出的 Java 語言，增加了很多限制，譬如 type safety 和 garbage collection，把很多程序員容易掉陷阱的地方都回避開了，因此成為企業級應用的首選語言。
回到
區塊鏈的智能合約這個問題。要想安全可靠地寫合約，合約語言必須進 一步縮減功能，加入很多約束。跟律師打過交道的都知道，合同一般分類有范本的，律師從來不愿意從頭起草，而是在范本的基礎上寫合約。這就是因為范本提供了很多約束條件，經歷過時間的考驗和不斷的更新，不容易犯錯誤。律師的范本就類似高級程序語言設計中的 type 和 pattern。前段時間以太坊上的 DAO 出現被攻擊的事件，就是因為合約代碼中的錯誤。所以說，對于寫智能合約的程序語言來說，少反而是多。另外，真正要設計一個智能合約的語言，恐怕從一開始就要考慮如何結合形式驗證(formal verification) 技術來證明每個合約的正確性，把可證明性(verifiability 或 provability)設計到語言的結構內。
版權申明：本內容來自于互聯網，屬第三方匯集推薦平臺。本文的版權歸原作者所有，文章言論不代表鏈門戶的觀點，鏈門戶不承擔任何法律責任。如有侵權請聯系QQ：3341927519進行反饋。
