Karl Popper 认为， 经验科学里的普遍命题无法靠有限次观察证实，只能由反例证伪． 测试也有这样的边界：一万个通过的样本不能证实“所有良类型程序都不受阻”． 要反驳 类型安全 ，反例必须同时满足：

$$⊢𝑡:𝑇,𝑡{⟶}^{\ast }𝑢,\mathrm{stuck}\left(𝑢\right).$$

其中前两个判断必须能由 类型与类型判断 与 多步规约 的正式规则推出， 受阻按 正规形式与受阻 判断． 单独找到受阻项并不够，例如 $\text{succ }\text{ true}$ 本来就不良类型； 错误的 Rust 实现产生受阻状态，往往说明实现偏离了规则，原规则本身的类型安全并未推翻．

证明则走另一条路： 它从定义出发推出结论，无需靠抽样观察，因此可以对无穷多个程序负责． 代价是它只对定义负责： 如果规则本身没有描述我们想要的语言，证明再严密也帮不上忙． 这就划清了证明与测试的分工：证明管“从规则到结论”，测试和实现管“规则是否符合预期”． 类型安全 与 用测试对照证明 分别给出了这两种工作的例子．