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