以 [定义] 类型与类型判断 的关系 $𝑡:𝑇$ 为规格，以 Rust 类型检查算法 type_of type_of 为实现。 Some(T) Some(T) 表示算法报告类型 $𝑇$， None None 表示拒绝；Rust 的 Bool Bool 、 Nat Nat 分别对应对象语言的 $\text{Bool}$、$\text{Nat}$。

• 算法相对规则可靠（sound）：若 type_of(t) = Some(T) type_of(t) = Some(T) ，则 $𝑡:𝑇$。
• 算法相对规则完备（complete）：若 $𝑡:𝑇$，则 type_of(t) = Some(T) type_of(t) = Some(T) 。