波普尔（Popper）认为，经验科学里的普遍命题无法被有限次观察证实，只能被一次反例证伪。测试的处境与此相同：一万个通过的样本不能证实“所有良类型程序都不受阻”，一个受阻的样本就能推翻它。

证明则走另一条路。它不观察，而是从定义出发推出结论，所以可以对无穷多个程序负责。代价是它只对定义负责：如果规则本身没有描述我们心里想的那门语言，证明再严密也帮不上忙。这说明了证明与测试的分工：证明管“从规则到结论”，测试和实现管“规则是不是我们想要的”。 [推论] 类型安全 与 用测试对照证明 分别给出了这两种工作的例子。