我今天要教大家一个魔法，会了这个魔法，念一句咒语，任何代码都没有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的地方越来越多
