这期的内容涉及了类型系统的一些术语，下面会注释一下。实际上Clarkson不需要从近乎哲学的角度讲认知论。但归纳（induction）和演绎（deduction）这两个基于哲学认知论的术语的使用是准确的。

软件测试的主力方法本质上是归纳法，因为事实上无法完全归纳，所以它证明的软件可靠性不如演绎法，如果演绎法的证明存在且能做到的话。但如果你能完全覆盖的测试一个函数，exhaustive induction和deduction的证明强度是一样的，这种完全覆盖测试在工业领域也不罕见。

当然，这门课主要是讲形式化方法的。100%的Deductive Reasoning。

++++

02:40 说到了可靠，sound；03:07说到了完备，complete。

sound，complete，以及这里没有提到的consistent，都是源自于逻辑学的词语；PL领域从逻辑学借用了这些词语但是含义不一样。Logic和PL的共同点是他们都是形式化的，formal的，在语法的处理上也都是高度相似的；但Logic的语义是true/false，PL的语义有多种定义方法但不是true/false；Logic有基于语法规则的推理（即演绎，这不奇怪因为Logic就是研究演绎推理的学科），也有基于语义的“推理”（比如真值表，implication），如果所有语法规则推理的结果都能被语义“推理”证实，我们说这个语法规则推理（演绎）是可靠的（sound，unsound意味着规则会推理出错误结果），如果所有可以用语义“推理”证实的，语法规则推理也都能做到，我们说这个语法规则推理是完备的（complete，incomplete意味着存在正确定理但是无法推导出来）；这是这两个词在逻辑学上的本意。

在类型系统里，类型系统通常是非常practical的，不象类型理论那样规则，以为毕竟编程语言的类型系统是为了工程服务的，要解决实际问题，也要让程序跑在实际的处理器和操作系统上。

说一个programming language sound（或type sound）指的是所有符合类型要求的程序（通过类型检查）不会有运行时错误。

在类型系统里，一个程序well-typed或者well-behaved，指的是它能通过类型检查；如果说一个程序ill-typed，指的是它无法通过类型检查。但是类型检查检查什么，不同语言不同编译器不一样，但通常well-typed（=well-behaved）至少保证程序是safe的，即不能有untrapped error，例如C语言里和野指针，越界，都是unsafe的。这个是type system的底线，实际语言都在这个底线之上加入很多其它要求。

02:40 说的well typed programs don't go wrong说的就是这个意思。类似的说法还有well-typed programs are well behaved，指的是一个type system被证明为sound。

象C是unsafe的，不能算well-typed。ML可以算。而js和scheme，是safe的（因为没有untrapped error），但这两个都不算有类型的，所以也不是well-typed，即使他们有dynamic checking。

以上如果想多了解一点可以搜索Luca Cardelli写的Type Systems，网上一搜就有。Benjamin Pierce说他对type的了解都是Cardelli教的，你不用担心Cardelli的文章里有任何表述或者术语使用有问题。

++++

有任何问题可以在讨论区讨论。 http://t.cn/A6oCKX2B