所以即使有了 Hoare Logic，程序驗證也不是輕松的事情。于是呢就有人乘火打劫，提出一個類似減肥藥的想法，聲稱他們要用“深度學習”，通過對已有標注的代碼進行學習，最后讓機器自動標注這些前后條件。還在“空想”階段呢，卻已經把“自動標注”作為自己的“優勢”寫進了白皮書：“我們的方法是自動的，其他的項目都是手動的……”
很可惜的是，“自動標注”其實跟“自動編程”是一樣的空想。自動編程的難點在于機器沒法知道你想要做什么。同理，自動標注的難點在于，機器沒法知道你想要代碼滿足什么樣的性質（property）。這些信息只存在于你的心里。如果你不表達出來，任何其它人和機器都沒有辦法知道。
除非你把它寫出來，機器永遠無法知道函數的參數應該滿足什么樣的條件（前條件），它也無法知道函數的返回值應該滿足什么樣的條件（后條件）。比如上面的那個例子，機器怎么知道你想要程序執行之后 x 大于零呢？除非你告訴它，它是不可能知道的。
你也許會問，深度學習難道幫不上忙嗎？想想吧…… 你可以給深度學習系統上千萬行已經標注好的代碼。你可以把整個 Windows 系統，整個 Linux 系統，FireFox 的代碼全都標注好，再加上一些戰斗機，宇宙飛船的代碼，輸入深度學習系統進行“學習”。現在請問系統，我下面要寫一個新的函數，你知道我想要做什么嗎？你知道我希望它滿足什么性質嗎？你仍然不知道啊！只有我自己才知道：它是用來給我的貓鏟屎的 :p
所以，利用深度學習自動標注 Hoare Logic 的前后條件，跟“自動編程”一樣，是在試圖實現“讀心術”，那顯然是不可能的。作為資深的 PL 和形式驗證專家，這些人應該知道這是不可能自動實現的。他們提出這樣的想法，并且把它作為相對于其他智能合約項目的優勢，當然只是為了忽悠外行，為了發
幣圈錢 ;)
如果真能用深度學習生成前后條件，從而完全自動的驗證程序的正確性，那么這種辦法應該早就在形式驗證領域炸鍋了。每一個形式驗證專家都希望能夠完全自動的證明程序的正確性，然而他們早就知道那是不可能的。
設計語言來告訴機器我們想要什么，什么叫做“正確”，這本身就是 PL 專家和形式驗證專家的工作。設計出了語言，我們還得依靠優秀的程序員來寫這些代碼，告訴機器我們想要做什么。我們得依靠優秀的安全專家，給代碼加上前后條件標注，告訴機器什么叫做“正確安全的代碼”…… 這一切都必須是人工完成的，無法靠機器自動完成。
當然，我并沒有排除對智能合約手動加上 Hoare Logic 標記這種做法的可行性，它是有一定價值的。我只是想提醒大家，這些標記必須是人工來寫的，不可能自動產生。另外，雖然工具可以有一定的輔助作用，但如果寫代碼的人自己不小心，是無法保證程序完全正確的。
如何保證智能合約的正確呢？這跟保證程序的正確性是一樣的問題。只有懂得如何寫出干凈簡單的代碼，進行嚴密的思考，才能寫出正確的智能合約。關于如何寫出干凈，簡單，嚴密可靠的代碼，你可以參考我之前的一些文章。
做智能合約驗證的工作也許能圈到錢，然而卻是非常枯燥而沒有成就感的。為此我拒絕了好幾個有關
區塊鏈的合作項目。雖然我對區塊鏈的其它一些想法（比如去中心化的共識機制）是感興趣的，我對智能合約的正確性驗證一點都不看好。
版權申明：本內容來自于互聯網，屬第三方匯集推薦平臺。本文的版權歸原作者所有，文章言論不代表鏈門戶的觀點，鏈門戶不承擔任何法律責任。如有侵權請聯系QQ：3341927519進行反饋。
