鲍勃大叔认为软件不同于数学，软件是科学，科学与数学是有区别的

软件更像是科学而不是数学。数学表达式是可证明的，科学理论只是可表明的。数学是演绎的。科学是经验的，软件也是经验的。我们可表明，但不证明正确性。

Software is more like science than mathematics. Mathematical expressions are provable, scientific theories are merely demonstrable. Math is deductive. Science is empirical. Software is empirical. We demonstrate, but do not prove, correctness.

banq评论：软件是经验的，也就是通过经验积累表明只有某些方式行得通，但是无法证明为什么只有这种方式才行得通，后者是因果关系的证明，是数学问题。通过不断失败摸索，将软件系统扶上墙运行起来了，然后开始烧香拜神，不要死机啊！这些都是经验的特点。

鲍勃大叔是软件工程与MF齐名的大师，他们的观点与麻省理工等学院派还是有些区别，学院派更注重算法和数据结构，这两者偏重数学，而经验派偏重最佳实践，只有这条路好走无疑是最佳实践，是模式，上升为框架和架构。

软件是一门艺术！

和黑客和画家里的话一样，编码是渐进的，不是一开始就设计好的，设计的再漂亮，该踩的坑一个不少。

鲍勃大叔继续补充道：
Types==propositions.
Programs==proofs.
Execution==simplification.

Test==hypothesis.
Code==experiment.
Run==observation.

类型==科学命题
程序==科学证据
执行==简化
测试==假说
代码==科学实验
运行==科学观察

鲍勃大叔继续说：

静态类型是试图使软件更具数学性，类型正确性是演绎和可证明的。但是，类型正确性并不意味着行为正确。即使完全类型正确，也必须凭经验证明行为。

但这不会使类型系统变得无用。相反，许多人发现类型系统是非常宝贵的。但是，它并不意味着类型系统会将软件从科学变为数学，最后，软件仍然是一种经验科学。

科学理论通过实验证明，只有系统稳定运行后才是支持理论的证据，即使有偶尔错误也可以容忍。

在软件中，这些科学实验就是软件测试，我们通过执行足够的测试来证明正确性，以便将我们的信心提升到一个我们感觉到可以安全部署了。

因此，测试多少与类型无关，您编写和执行的测试数量不受您的语言类型系统的影响。

每个功能特征都是一个理论。每一个这样的理论都通过一系列科学试验形式的实验来验证。如果你可以编写一个特征理论的代码，你可以编写测试，这些实验就是表明支持这个特征功能。

评：当然学院派不满意上述这套说服，搬出了麻省理工的“ 类型和编程语言”这本教科书来驳斥。。。。。

和黑客和画家里的话一样，编码是渐进的，不是一开始就设计好的，设计的再漂亮，该踩的坑一个不少