Soundness and Completeness of the Type System

In the section 6 of Programming Languages course, Dan Grossman discussed about the soundness and the completeness of the type system. He said that:

  • A type-system is sound implies that all of type-checked programs are correct (in the other words, all of the incorrect program can't be type checked), i.e. there won't be any false negative [1].
  • A type-system is complete implies that all of the correct program can be accepted by the type checker, i.s. there won't be any false positive [2].

With this explanation, I have better understanding to the soundness and the completeness of the logic system. In the logic system, we would say that:

  • A logic system is sound means that all provable statements are true in models [3].
  • A logic system is complete means that all statements which are true in all models are provable [3].

Besides, according to Godel's incompleteness theorems, if your system is expressive enough to represent natural numbers, then it can't be both sound and complete. This theorem applies to the type system as well. Usually, most programming language would prefer soundness over completeness, since false positive will result in bad consequence.

[1]For negative, we mean that the type checker claims that there is no error in the input program, i.e. the input program is correct.
[2]For positive, we mean that the type checker claims that there are some errors in the input program, i.e. the input program is incorrect.
[3](1, 2) Analogous to the type system, provable is corresponded to type checked and model is the set of correct program.