“可靠”这个词在 PLT 里有两种常见用法，容易混：

• 类型系统相对运行时可靠：规则说有类型的，运行时不受阻。这就是 [推论] 类型安全 。
• 算法相对规则可靠：算法说有类型的，规则真能推出来。 type_of type_of 的这一性质见 [定理] 算法可靠性 ，一般定义见 [定义] 可靠与完备 。

两条串起来才是我们真正关心的：检查器接受的程序，运行时不会受阻。只有一条，链条就是断的；两条的组合见 [推论] 检查器接受的程序不会受阻 。