Comment by bluGill
9 days ago
"the Rust semantics" are defined informally as sound. Anything that the implementation accepts that is unsound is a bug. We might never be able to prove the rust implementation, and may forever find loop holes, but informally it is sound and that is the intent.
There is no such thing as "informally sound". Soundness is a mathematical property and needs to be proven mathematically. For that, you first need a mathematical definition.