逻辑学里也有一对“可靠 / 完备”：一个证明系统是可靠的，如果能证明的都是真的；是完备的，如果真的都能证明。哥德尔 1929 年证明一阶逻辑的证明系统是完备的；两年后的不完备定理则说，足够强的算术理论里，总有真而不可证的命题。

[定义] 可靠与完备 描述的类型检查算法与类型规则之间的关系，与此平行： type_of type_of 扮演“机械的证明过程”，类型规则扮演“什么才算对”的标准。差别在于，这里的标准本身也是一组规则，而且足够简单，两个方向分别由 [定理] 算法可靠性 与 [定理] 算法完备性 证明。语言再大一些，“完备”就常常要附加条件，甚至干脆不成立，设计者必须决定放弃哪一边。