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.e. 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 negative will result in bad consequence.

**Edit (01/31/2023)**: In the earlier version, I incorrectly mentioned false
*positive* in the last sentence. It should be false *negative*. The text has
been updated. Special thanks to Yuk Lam Sung for pointing this out to me.

[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. |