在之前一篇關於人工智慧的文章中，我指出了自動程式設計的不可能性。 今天我想談談乙個相關的話題：以太坊式智慧型合約的形式化驗證。 一些人聲稱對智慧型合約進行基於深度學習的自動化形式驗證，以確保合約的正確性。 但是，我今天要告訴大家的是，就像自動程式設計一樣，全自動合同驗證是不可能的。
隨著區塊鏈技術的深入，許多人開始對以太坊的智慧型合約語言大驚小怪。 他們中的一些人是從事PL的人，他們試圖正式驗證用Solidity等語言編寫的智慧型合約，聲稱使用嚴謹的數理邏輯方法來自動驗證智慧型合約的正確性。 一種方法是使用深度學習，深度學習經過訓練可以自動生成 Hoare Logic 的前置和後置條件。
我好像把你弄糊塗了......讓我們從 Hoare Logic 開始。
Hoare Logic 是一種形式驗證方法，用於驗證程式的正確性。 這樣做的方法是先標記一些前置條件和後置條件（前置條件和後置條件），然後進行邏輯推理來驗證**的一些基本屬性，例如轉移後的餘額是否正確。 下面是乙個非常簡單的 Hoare Logic 示例：
這意味著，如果起始 x 等於 0，則在執行 x：=x+1 後，x 應大於 0。 前置條件為 x=0，後置條件為 x > 0。 如果 x 以零開頭，則執行x:=x+1之後，x 將大於 0，因此將驗證此句子。
Hoare Logic的系統將所有這些前置和後置條件與**連線起來，經過邏輯推導和驗證，可以做出這樣的保證：在前置條件滿足的情況下，在**執行後，後置條件必須為真。 如果滿足所有這些條件，系統將認為這是正確的過程。 需要注意的是，這裡所說的“正確”完全是由人決定的，系統並不知道“正確”是什麼意思。
Hoare Logic確實對程式的安全性有一定的影響，並且已經應用到一些實際專案中。 例如，在 Microsoft Windows 的驅動程式中，有一種稱為 SAL 的安全注釋語言，它實際上是 Hoare Logic 的實現。 但是，前置條件和後置條件是什麼，你必須自己標記**，否則系統將無法工作。
例如，在上面的示例中，系統如何知道我想要 x>0 屬性？只有我自己寫的。 因此，要使用 Hoare Logic，您必須在 **. 如何編寫這些條件需要對程式語言和形式邏輯的原理有深刻的理解。 這項工作需要訓練有素的專家，並且需要大量時間。
因此，即使使用Hoare Logic，程式驗證也不是一件容易的事。 於是，有人趁火搶，提出了乙個與第一種藥物類似的想法，聲稱他們會用深度學習來學習已經標註的**，最後讓機器自動標註這些前後條件。 還處於幻想階段，但已經寫進了自動標註的優點中，作為自己的***我們的方法是自動的，其他專案都是手動的......
不幸的是，自動注釋和自動程式設計一樣是一種幻想。 自動程式設計的困難在於機器不知道你想做什麼。 同理，自動標註的難點在於機器無法知道你想滿足什麼樣的屬性。 這些資訊只存在於你的心中。 如果你不表達它，其他人或機器都不會知道它。
除非你把它寫出來，否則機器永遠不會知道函式的引數應該滿足什麼條件（前置條件），也永遠不會知道函式的返回值應該滿足什麼條件（後置條件）。 例如，在上面的例子中，機器如何知道你在程式執行後希望 x 大於零？除非你告訴它，否則不可能知道。
你可能會問，深度學習不是嗎？想想吧。。。。。。您可以為深度學習系統提供數千萬條已經標記的行。 你可以標記整個Windows系統、整個Linux系統、Firefox，再加上一些戰鬥機、飛船，輸入到深度學習系統中進行學習。 現在請問系統，**要寫乙個新函式，你知道我想做什麼嗎？你知道我希望它滿足什麼性質嗎？你還不知道！只有我知道：這是:p曾經為我的貓鏟屎
因此，使用深度學習來自動標註Hoare Logic前後的條件，就像自動程式設計一樣，是在試圖實現讀心術，這顯然是不可能的。 作為資深的PL和形式驗證專家，這些人應該知道這不可能自動實現。 他們提出了這樣的想法，並利用它作為優於其他智慧型合約專案的優勢，當然，只是為了愚弄外行，為了發行貨幣;)
如果真的有可能使用深度學習來生成前置和後置條件，以完全自動地驗證程式的正確性，那麼這種方法應該在形式驗證領域早就爆炸了。每個形式驗證專家都希望能夠完全自動地證明程式的正確性，但他們已經知道這是不可能的。
設計一種語言來告訴機器我們想要什麼，什麼是正確的，這本身就是PL專家和形式驗證專家的工作。 一旦語言設計好了，我們就要依靠優秀的程式設計師來編寫這些**，並告訴機器我們想做什麼。 我們要依靠優秀的安全專家來標記前後的情況，並告訴機器什麼叫正確和安全**，這一切都必須手動完成，不能由機器自動完成。
當然，我也不排除用 hoare 邏輯手動標記智慧型合約的可能性，這是有一定價值的。 我只想提醒大家，這些標籤必須手動編寫，不能自動生成。 此外，雖然該工具可以起到一定的輔助作用，但如果編寫**的人不小心，則無法保證程式完全正確。
如何保證智慧型合約的正確性？這與確保程式的正確性是同乙個問題。 只有懂得寫得乾淨簡單，思維嚴謹，才能寫出正確的智慧型合約。 有關如何編寫乾淨、簡單和可靠的更多資訊，您可以參考我以前的一些文章。
做智慧型合約驗證的工作可能會賺錢，但很無聊，很不充實。 出於這個原因，我拒絕了幾個與區塊鏈相關的合作專案。 雖然我對區塊鏈的其他一些想法很感興趣，比如去中心化的共識機制，但我對智慧型合約正確性的驗證一點也不樂觀。
事實上，我認為智慧型合約的整個概念是不可靠的，是乙個很大的誤解。 在位元幣和以太坊的系統中，根本不應該有指令碼語言，也不需要指令碼語言。
位元幣的解鎖指令碼在開始時執行時出現低階錯誤，導致注入安全漏洞。 使用者可能會惡意寫入**，從而導致執行指令碼的系統出現錯誤。 位元幣最初的解鎖方法是將**（解鎖指令碼+鎖定指令碼）的兩段拼接成文字，然後執行。 程式的文字處理是程式語言實現的禁忌。 有一點經驗的黑客知道這裡可能會有攻擊點。
以太坊的 Solidity 語言始於乙個低階錯誤，導致價值 5000 萬美元的以太幣被盜。 以太坊的智慧型合約系統消耗了大量的計算資源，也導致了嚴重的效能問題。
雖然位元幣和以太坊的作者可能是密碼學和分布式系統領域的專家，但我不得不承認，他們都是PL的外行:p但是，如果您是這些語言的專家，那不是更好嗎？我不這麼認為。
第乙個問題是PL領域充滿了各種宗教，傳教士也很多。 普通的 PL 內部人員會通過試圖設計一種完美的語言來表達自己的信仰，而不管他人的生活如何，從而使事情複雜化。 如果你運氣不好，你會遇到那種極客......充滿純函式、單子、依賴型別、線性邏輯然後語言被設計成沒有人可以使用:p
負責任的PL科學家，他們都試圖避免首先創造新的語言。 如果可以在沒有新語言的情況下解決問題，就不要設計新語言，盡量不要在系統中使用嵌入式語言。 所以，如果我設計了位元幣，我根本不會為它設計一種語言。
讓使用者可程式設計是很危險的！很少有使用者能夠正確可靠地編寫**，並且很少有語言系統能夠開發出沒有錯誤。 語言系統設計中的錯誤可能會給黑客編寫惡意指令碼進行破壞的機會。 從來沒有任何語言和它們的編譯器，執行時系統從一開始就是正確的，需要很多年才能穩定下來。 然後你必須考慮效能，這對於去中心化的分布式系統來說更加困難。 對於普通語言來說，這不是什麼大問題，你不需要用它來控制飛機。 然而，數字貨幣系統的語言幾乎不允許這個問題。
因此，與其擔心設計這些智慧型合約語言，不如完全不要使用這種功能。
我們真的需要這些指令碼的功能嗎？雖然位元幣有指令碼語言，但實際上常用的指令碼不超過 5 個，你可以直接硬編碼它。 雖然以太坊的***已經做了這麼多的應用前景，但EVM上有什麼有價值的應用嗎？我認為我們不需要這些智慧型合約。 只要數字貨幣做好一件事，就可以安全高效地當錢使用，這已經很好了。
美元、人民幣、**他們有合約功能嗎？不。 為什麼數字貨幣必須具有這樣的功能？我覺得這違反了模組化設計的原則：一件事只做一件事，而且做得最好。 數字貨幣應該像貨幣一樣，可以實現轉賬兌換的簡單功能。 合約應該是乙個單獨的系統，不應與貨幣相關聯。
合同呢？將其留給律師和會計師，或使用單獨的系統。 你有沒有想過為什麼世界上的法律體系沒有被程式設計為自動化？為什麼我們需要律師和法官，而不僅僅是機械人？為什麼一些國家法院有必要有陪審團，而不僅僅是根據法律條款來裁決案件？這不僅僅是乙個歷史問題。 你需要了解法律的本質，才能明白在沒有人類的情況下機械地執行法律是不可行的。 智慧型合約就是要把人們完全帶出系統，這將是乙個問題。
期望過多的功能實際上是過度設計。 花費精力折騰智慧型合約系統可能會大大延遲世界對數字貨幣的真正接受。 說實話，在嘗試了多種數字貨幣，了解了它們使用的技術後，我發現它們挺有意思的，但這些數字貨幣還處於實驗階段，離真正被當成貨幣使用還有一定的距離。 專注於改善它們作為貨幣的功能將加速它們的接受。 把精力花在智慧型合約上，我認為這是乙個錯誤。
在這一點上，我認為位元幣比它的繼任者（例如以太坊）更真實一些。 位元幣也有一種指令碼語言，但它並沒有過分強調這種指令碼的作用。 位元幣的指令碼語言非常簡單，而且不是圖靈完備的。 這迫使使用者編寫功能簡單、不會損害系統效能且易於驗證的指令碼。 相比之下，以太坊花費了太多精力來折騰智慧型合約，使它們過於複雜，導致各種問題並影響對最重要的貨幣特徵的接受。