In Rust, `loop {}` is an expression of type `!`, which means that from a type-theoretic perspective it is inhabited. This means that the Curry–Howard correspondence fails for Rust.