以 类型与类型判断 的关系 $𝑡:𝑇$ 为规格， 以 Rust 类型检查算法 type_of type_of 为实现． 在 算术语言形式化的未展开前提 的实现假设下， 正常返回 Some(T) Some(T) 表示算法报告类型 $𝑇$， None None 表示拒绝； Rust 的 Bool Bool 、 Nat Nat 分别对应对象语言的 $\text{Bool}$、$\text{Nat}$．

若 type_of(t) = Some(T) type_of(t) = Some(T) 蕴涵 $𝑡:𝑇$，则称算法相对规则可靠； 若 $𝑡:𝑇$ 蕴涵 type_of(t) = Some(T) type_of(t) = Some(T) ，则称算法相对规则完备．