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).