For clarification, "trait objects" are a subset of the trait system, and have much less use in rust programs than traits overall. A trait object is a dynamicall

For clarification, "trait objects" are a subset of the trait system, and have much less use in rust programs than traits overall. A trait object is a dynamically dispatched pointer (often owned through Box or Arc), as opposed to the usually statically dispatched generic usage of traits that's more common in rust. Destructors aren't guaranteed to run in Rust, they aren't necessary for memory safety. It's a fair concern to note that they aren't modeled, because they are pervasive and can impact memory safety, but they don't exist to support it. Panics not being modeled is of course also a big gap, although you could always compile your code with panic=abort if you wanted to dodge that issue!