1樓：Jason Hu
可以。你所說的領域叫做software verification，橫跨了數學、理論計算機和軟體工程的很大的應用方向。做software verification有整乙個譜系的方法。
全自動化。
model checking。model checking需要你把specification用temporal logic來表達。典型的temporal logic有CTL, LTL和CTL*。
model checking有個好處就是提到的三個temporal logic都有完備的檢查演算法，因此是全自動的。在狀態空間有限的情況下model checking的應用很普遍，比方說電子硬體又或者是分布式協議。
SAT。有完備的NP-complete演算法。DPLL演算法是歷史上的突破點。
SMT和automatic theorem prover。現有成熟的都是基於first order logic，內部用到了SAT。SMT專注於arithematic而automatic theorem prover專注於quantifiers。
有名的有MSR的z3[1] 和Vampire[2]。荷蘭有個專案在開發基於AI和higher order logic的SMT，非常有前途。[3] 但是注意first order logic是undecidable theory所以這個自動工具的能力有限。
要利用這些工具進行定理證明需要你對實現有很深的理解。
半自動。半自動的往往是基於SMT的。比方說Dafny[4]和Ivy[5]。
他們本身是程式語言，可以編寫specification驗證寫的程式。Dafny和Ivy都是基於z3的。這個方向在純軟體工程很常見，這些工具往往都是軟工的人開發的。
（基本上）全手動。這一型別的工具更加偏向於數學性的。常見的有Isabelle[6], HOL[7], Coq[8], Agda[9]和Lean[10]。
他們有的是基於formal logic，比方說Isabelle和HOL，有的基於type theory比方說剩下三個。但是本質上他們本身也是程式語言。我對type theory比較了解。
在type theory，你可以表達很多的程式，包括很多高階的程式，你用Dafny是沒辦法驗證的。雖然這些語言都是函式式語言，你也可以用他們來驗證其他程式。比方說VST[11]用Coq裡的separation logic模型來驗證C程式。
基本上，這個方向的工具太多了。一般來講，自動化越強的可證明的命題就越弱；自動化越弱的需要的專業知識就越多。你對這個方向感興趣的話可以先從比方說Dafny入手，感受一下。
這個方向基本跟CS一樣老。
2樓：
Knuth曾經很幽默地說過，「我只證明了這個演算法的正確性，沒有實際試過。」
有時候太過關注學術的人會忘記一件事，那就是書面上的證明是無法「證明」實際世界中的「事實」的。
這就好比那個有些無聊的腦筋急轉彎，「1+1什麼時候不等於2？」「算錯的時候。」
形式化證明可以解決很多問題，但它無法證明這些問題就是我們所關心的所有問題（而實際上，我們關心的所有問題，已經完全用形式化的語言敘述出來的可能性幾乎是0）。
我們能夠證明，這個排序演算法是正確的，那麼我們能夠證明實際執行的時候，這個演算法100%每一次都會返回「正確」的結果嗎？不能的。我們的證明過程是過於簡略的，我們的前提假設都隱含了太多內容。
比如，我們證明了排序過程中不會產生「棧溢位」嗎？幾乎肯定沒有，要證明這個，首先要提供「棧大小」「機器字對齊」「編譯器對程式變換時對空間使用的保證條件」等，我從來沒有在「幾頁紙以內的證明」中看到過這些，最多也就是說明一下「空間複雜度」。
比如，我們證明了「編譯器能夠正確翻譯我們的程式」嗎？幾乎肯定沒有，這被認為是不證自明的東西。然而實際中，我們幾乎從來不使用經過形式化證明的編譯器，即使是CompCert，也沒有完成所有的形式化工作。
順便一提，CompCert的bug列表不是空的。
再比如，我們證明了「作業系統中不會出現死鎖，或者作業系統的排程不存在餓死」嗎？幾乎肯定沒有，這是太過瑣碎的東西，幾乎所有的書本上的形式化證明都不會提到作業系統。然而我們都知道，從前的作業系統是經常會「宕機」的，如果作業系統宕機，我們的程式將無法完成「我們已經證明它一定能完成」的功能。
再比如，我們證明了「CPU能夠正確地執行我們的程式」嗎？幾乎肯定沒有。CPU是太過複雜的裝置，沒有人能夠用形式化證明來它不會出錯。
實際上，CPU「經常」出錯，比如著名的Intel浮點bug。順便說一句，在Intel的浮點除法出現「重大」bug之後，各大廠商開始用形式化方法證明除法運算實現的「正確性」了。
歸根結底，我們能通過「紙面上的證明」來證明現實世界的「命題」嗎？我們能證明我們的「證明不會出錯」嗎？我們對這個宇宙的物理定律已經足夠了解了嗎？
我們能夠相信，這個世界的物理規律（包括那些我們已知的和我們所未知的）不會影響我們結論的正確性嗎？
作為宇宙的一部分，我們任何試圖100%證明這個「物理宇宙」的努力，都注定是徒勞。即使證明了，那也注定是錯誤的。這就好比有人聲稱自己創造的公理體系既一致又完備一樣，即使他說的不是胡說八道，大家也不會有多少興趣，因為那是太過於簡單的結論，不足以回答我們的問題。
別誤會了我的意思，我是說，形式化方法當然是有用的，很有用，在某些時候，展現了過於強大的能力。我只是想說，即使你「用形式化方法證明了某架飛機上所有硬體軟體的正確性」，我也一定會在乘坐它的首航時心裡不停地犯嘀咕。
3樓：NeoX
可以，但是你需要問三個問題：
1. 什麼是正確？
正確可以是證明演算法的某個屬性（比如說收斂），或者證明整個演算法的「過程」，如果是過程，你需要寫這個過程的Specification， 形式話的specification需要用某種形式化語言，可以是TLA+, 可以是一階邏輯, 也可以是CIC（Coq 的 underlying logic）
2. 證明什麼正確？
換句話說，一般正確性證明，是證明實現(implementation) 等價於specification. 比如Coq裡面，你需要證明演算法的每一步都跟specification是等價的，以及用到的一些資料結構的正確性等等。
3. 正確性意味著什麼？
有乙個概念叫Trusted Code Base, 你的specification 和 Coq本身是必須要被信任的，如果你用了Coq 的Extraction， Extraction也需要被信任。
4樓：陳煒
有乙個很有意思的結論叫Curry Howard correspondence. 歌詞大意是程式是定理的證明。 如果把乙個型別當作定理， 那麼寫出乙個正確的程式具有那個型別， 這個程式就可以當作那個定理的證明(更準確地說是這個程式型別檢查的整個過程是那個定理的證明)。
至於怎麼樣使用定理證明引擎， 幫小夥伴Soonho Kong打個廣告, 乙個很好的教程就是微軟研究院新出的定理證明引擎Lean的文件[1]。
[1] Tutorial: Theorem Proving in Lean
5樓：Da Guagua
可以。基於定理證明器（如 Isabelle, Coq等）的方法主要是在定理證明器內把程式寫出來並證明相關的性質，然後把定理證明器內寫的程式提取（Coq的code extraction或Isabelle的code generation）成函式語言，如Haskell, OCaml 等，再編譯執行。目前的成果可以參見Coq裡的CompCert project（乙個形式化驗證的C編譯器）和Isabelle裡的seL4（乙個形式化驗證的系統核心）。
C 開發的程式，能 100 避免被破解或反編譯嗎？
已登出 不能100 的，只要能做到防止大部分破解就行了。要做防反編譯還是得幾步走，先用vc,vb 非.net工程 一類的寫乙個殼，在這個殼中把exe壓縮，加密儲存，然後自己把JIT入口Hook了，做實時解碼，然後再把程式進行提權 不要直接把程式設定成管理員許可權執行，容易被直接殺掉 把一些執行緒啊記...
是否所有的 C C 程式都可以被編譯到 WebAssembly 呢？
玄魂 肯定不是了，理清這個問題，需要了解下wasm的基本原理。推薦閱讀 玄魂 系統學習WebAssembly 1 理論篇 堂吉可德 理論上是的，它就是個執行在瀏覽器上的虛擬機器，這個虛擬機器載入了某種語言的執行環境，那麼就能執行這種語言。不能執行部分就在於瀏覽器的安全限制，這個安全限制使應用程式成為...
把機械系統抽象為程式或數學函式，它是否可以完成所有的初等函式？
HelloWorld 槓桿實現的或非門 上為0，下為1 輪子上連個活塞，可以把勻速圓周運動變成三角函式。指數函式理論上可以化為虛三角函式，不過純機械似乎不宜借助虛數，暫時不好想。 GsOnG 在不考慮金錢和時間的情況下，題主所有問題的答案都是可以。還有我要多說一句，將機械系統抽象為函式來表達是為了了...