Chris Smith's article“辩论类型系统之前要了解的内容”包含以下无法解释的陈述：
测试：确定正确性的上限
证明：确定正确性的下限
上下文正在比较证明程序正确性（例如使用类型检查器）与测试程序行为（例如使用动态类型语言的TDD）的好处。
在这种情况下，正确性的“上限”和“下限”分别是什么？
最佳答案
假设您有一个程序，但对程序的工作原理一无所知。它应该具有很多属性（例如X，Y和Z），但您不确定它是否确实有。您该怎么做才能解决？
一种选择是尝试使用程序验证工具来正式证明该程序具有X，Y和Z属性。不幸的是，通常来说，不可能自动验证该程序是否具有任何有趣的属性（谢谢，暂停了问题！ ），因此即使程序实际上具有这些属性，也可能永远无法确定。但是，如果程序检查器报告该程序确实具有属性X，则可以说至少该程序具有X属性。从这种意义上说，您是在“下限”该程序的正确性：它肯定是具有属性X，并且可能具有更多属性。
另一个选择是运行程序，看看会发生什么。假设在测试过程中发现一个导致该程序行为异常的测试用例，因此绝对没有属性Z。但是，您的测试用例没有暴露任何其他错误。在那种情况下，由于您看到程序的行为异常，因此可以肯定地知道它没有属性Z。因此，您已经“上限”了程序的正确性-它当然没有属性Z，但是你不能排除其他任何东西。
如果将两者结合在一起，则可以证明程序具有属性X，并且可以直接证明其不具有属性Z。不知道它是否具有属性Y，因为那样都没有解决。
希望这可以帮助！