“静态”指不运行程序就能知道的性质，“动态”指运行时才能观察到的性质． 按类型检查发生的时机，程序语言通常分为静态类型语言与动态类型语言． 静态类型语言在运行前（通常是编译阶段）完成静态类型检查，未通过检查的程序会遭拒绝； Rust、Haskell、OCaml、Java、C 都属此类， 类型与类型判断 的类型系统也是如此，$𝑡:𝑇$ 只看项的形状，不执行 一步规约 的 $⟶$ 规约． 动态类型语言则让程序先运行，每次真正做运算时再检查参与运算的值是否符合要求的种类，不合要求就抛出错误；Python、JavaScript、Ruby 属于这一类．

用 词项的集合 的布尔值与自然数语言作类比， 动态检查的设计可以省去预先构造 $𝑡:𝑇$ 的推导， 直接在 $⟶$ 里给不合适的运行时操作补上报错规则 （ 显式错误规则与 Kotlin 的底类型 ）， 把受阻换成可预期的异常； 另一种设计可以采用转换规则 （ JavaScript 隐式转换与相等三角图 ）． 真实语言往往同时有这两类处理； JavaScript 的条件还会采用真假值转换，不要求参数字面上就是布尔值．

对这门小语言的运算，类型规则、 典范形式 与 保型 合起来保证： 参数若要求为 $\text{Nat}$，求值为值时就一定是数值，所以不必在运行时再检查它是否为布尔值． 这不等于真实静态类型语言可以省掉所有运行时检查； 例如 Kotlin 仍会抛出数组越界异常，Rust 的数组索引也可能需要边界检查． 两者的取舍是：静态检查更早排除它所覆盖的错误， 但会拒绝一些实际运行不会出错的程序（ 类型系统是保守的 ）； 动态检查更灵活，但错误通常要等到运行到那一行才暴露．

静态检查发生在运行前，不等于它能排除所有运行时错误． C 使用静态类型检查，但这种检查不能排除越界访问、通过悬垂指针访问对象等未定义行为 （参见 C11 草案 N1570 §6.2.4、§6.5.6）． 类型安全 证明的“类型安全”， 表达的是这套类型规则相对于操作语义的类型健全性， 需要由具体规则及证明支撑，不靠未说明判准的“强类型／弱类型”标签．

延伸阅读可参见 FrankHB 的 类型 vs. 类型检查．