健全性の証明（パート 2）
健全な関数とは、その安全性の前提条件が満たされているなら UB を引き起こせない関数のことです。
系: 純粋な safe Rust で実装されたすべての関数は健全である。
証明:
-
safe Rust コードには安全性の前提条件がない。
-
したがって、純粋な safe Rust で実装された関数の呼び出し側は、前提条件の空集合を常に自明に満たす。
-
safe Rust コードは UB を引き起こせない。
QED.
-
この系を読む。
-
証明を説明する。
-
くだけた言い方にすると、すべての safe Rust コードはちゃんとしている。プログラマーが考えなければならない安全性の前提条件はなく、常にルールに従い、UB を決して引き起こさない。