鲍勃大叔继续说：静态类型是试图使软件更具数学性，类型正确性是演绎和可证明的。但是，类型正确性并不意味着行为正确。即使完全类型正确，也必须凭经验证明行为。
但这不会使类型系统变得无用。相反，许多人发现类型系统是非常宝贵的。但是，它并不意味着类型系统会将软件从科学变为数学，最后，软件仍然是一种经验科学。
科学理论通过实验证明，只有系统稳定运行后才是支持理论的证据，即使有偶尔错误也可以容忍。
在软件中，这些科学实验就是软件测试，我们通过执行足够的测试来证明正确性，以便将我们的信心提升到一个我们感觉到可以安全部署了。
因此，测试多少与类型无关，您编写和执行的测试数量不受您的语言类型系统的影响。
每个功能特征都是一个理论。每一个这样的理论都通过一系列科学试验形式的实验来验证。如果你可以编写一个特征理论的代码，你可以编写测试，这些实验就是表明支持这个特征功能。
评：当然学院派不满意上述这套说服，搬出了麻省理工的“ 类型和编程语言”这本教科书来驳斥。。。。。
