Yeah this is a great example of why formally defining "soundness" is so tricky. Not only do we have to worry about unsafe code committing UB, we also have to wo

Yeah this is a great example of why formally defining "soundness" is so tricky. Not only do we have to worry about unsafe code committing UB, we also have to worry about it setting up a situation where safe code might commit UB later. Soundness is a property of functions and modules, but that property is a statement about the entire program that contains them, or actually about any program that could contain them. In retrospect, I kind of wish I had asked somebody like Ralf Jung to review this post before I published it. On the other hand, the fastest way to get an answer on the internet is to post the wrong answer :-D