我今天要教大家一個魔法，會了這個魔法，念一句咒語，任何程式碼都沒有bug
想知道咒語是什麽嗎？現在就告訴你。
跟我念：「這段程式碼沒有任何期望行為。」
A software bug is an error, flaw, failure or fault in a computer program or system that causes it to produce an incorrect or unexpected result, or to behave in unintended ways.當然，你接下來肯定要問我，能不能寫出符合某specification的軟體呢？能。這，比如 @Belleve 提到的Coq，Hoare Logic，等等等等，都能做。唯一的問題就是，做起來太繁瑣了，證明比實作難很多。這也是為什麽大部份軟體都沒有人做formal verification（Coq，Hoare Logic等）。至於安全性遠遠高於軟體成本的safety critical的東西有沒有人用這種辦法？當然有了！DeepSpec: The Science of Deep Specification，file system: http:// css.csail.mit.edu/6.888 /2015/papers/haogang.pdf ，基礎演算法：http://www. cs.ru.nl/~james/RESEARC H/types2008.pdf ，分布式系統：https:// homes.cs.washington.edu /~mernst/pubs/verify-distsystem-pldi2015-abstract.html ，作業系統：http:// web1.cs.columbia.edu/~j unfeng/09fa-e6998/papers/sel4.pdf ，編譯器：CompCert - The CompCert C compiler
這就是答案，以下是略相關的東西，開始離題：
能不能降低FV的成本呢？可以，並且一直在降低：在這裏有兩條路，一是用軟體完全自動的證明沒bug（Model Checking, SMT，Dafny @ rise4fun from Microsoft），一是采用半自動化，使你在更高層次（tactic等）上控制證明。
這還是太高，能不能再降低FV的成本呢？如果我們犧牲一部份正確性，可以：我們可以用contract，把static analysis改成dynamic analysis，同時，我們可以做一半不做一半，一定的地方用static analysis證明沒bug，剩下的用contract，降低bug機率/範圍http:// arxiv.org/abs/1506.0420 5
能不能降低學習FV的成本呢？可以，我這裏要舉兩個沒有人會猜到我會一起用的例子：Simply Typed Lambda Calculus, Java Card，前者對於所有程式，都會計算出答案，不會死迴圈，也不會不能運算下去，後者符合Applet Isolation Principle(http://www. labri.fr/perso/ly/publi cations/using_coq_to_verify_javacard.pdf )。型別系統就是FV最著名的例子，沒有之一。
能不能反過來用testing幫助formal verification？能！Isabelle就是這樣做的：http:// isabelle.in.tum.de/dist /Isabelle2015/doc/nitpick.pdf
可以看出，這裏已經有一條盡管比較粗糙，但是pay as you go的gradual path了，我也希望並預言，隨著CS/CPU的發展，這條path會越來越無縫（adapt cost越來越低），較高層的成本也會慢慢降低，會使得被驗證沒bug的地方越來越多
