Soundness Proof (Part 2)

A sound function is one that can’t trigger UB if its safety preconditions are satisfied.

Corollary: All functions implemented in pure safe Rust are sound.

Proof:

  • Safe Rust code has no safety preconditions.

  • Therefore, callers of functions implemented in pure safe Rust always trivially satisfy the empty set of preconditions.

  • Safe Rust code can’t trigger UB.

QED.

  • Read the corollary.

  • Explain the proof.

  • Translate into informal terms: all safe Rust code is nice. It does not have safety preconditions that the programmer has to think of, always plays by the rules, and never triggers UB.