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