circular reasoning is a potential source of unsoundness
circular reasoning is a potential source of unsoundness
Posted Mar 30, 2026 17:10 UTC (Mon) by NYKevin (subscriber, #129325)In reply to: circular reasoning is a potential source of unsoundness by daroc
Parent article: Rust's next-generation trait solver
In the case of Send and Sync, the traits impose a negative obligation. Types in Rust are thread-safe by default, and they can only become thread-unsafe through the use of interior mutability or raw pointers. So it's entirely reasonable to coinductively infer Send and Sync. If you never encounter something manifestly !Send or !Sync in your chain of reasoning, then there can't be any source of thread-unsafety, so inferring Send or Sync is fine.
On the other hand, the unsafe trait TrustedLen imposes a positive obligation. Specifically, if a type implements TrustedLen, then unsafe code may soundly assume that its len() method returns the right value, and execute UB if that assumption turns out to be wrong. In pragmatic terms, that means the Source of Truth for len() must be hidden behind some visibility annotation so that foreign safe code cannot mess with it. If len() is computed by calling into something else, then that callee is under the same obligation, transitively all the way down to the ground truth.
In the case of TrustedLen, I don't think there exists a counterexample where coinduction actually produces an unsound implementation. Coinduction implies, to my mind, that you end up with TrustedLen-or-some-equivalent all the way down, and there's no actual soundness hole. But it is the sort of thing that would keep me awake at night if I were responsible for trait-solving in Rust. Users can define arbitrary unsafe traits with arbitrary soundness requirements, and those requirements typically exist only in documentation or comments, not in actual code the compiler can read and understand. Who is to say whether any one of those unsafe traits might be incompatible with coinduction?
