How does this deal with non-termination? Eg. declare x (must_use); P; use(x) (I apologies for the non-Rust-conforming pseudo-code.) The type-checker

How does this deal with non-termination? Eg. declare x (must_use); P; use(x) (I apologies for the non-Rust-conforming pseudo-code.) The type-checker won't be able to tell if P terminates or not, whence x's use can't be enforced. That's a direct consequence of Rice's theorem (which in turn follows directly form the non-computability of the halting predicate).