今天我想來談談一個相關的話題：
以太坊式的智能合約的形式驗證。有些人聲稱要實現基于“深度學習”的，自動的智能合約形式驗證（formal verification），用于確保合約的正確性。然而今天我要告訴你的是，跟自動編程一樣，完全自動的合約驗證，也是不可能實現的。
隨著
區塊鏈技術的愈演愈烈，很多人開始在以太坊（Ethereum）的“智能合約語言”上做文章。其中一部分是搞 PL 的人，他們試圖對 Solidity 之類語言寫的智能合約進行形式驗證，號稱要用嚴密的數理邏輯方法，自動的驗證智能合約的正確性。其中一種方法是用“深度學習”，經過訓練之后，自動生成 Hoare Logic 的“前條件”和“后條件”。
版權申明：本內容來自于互聯網，屬第三方匯集推薦平臺。本文的版權歸原作者所有，文章言論不代表鏈門戶的觀點，鏈門戶不承擔任何法律責任。如有侵權請聯系QQ：3341927519進行反饋。
