Fair enough about the particular Github comment, but even there I think you are wrong. The architectural downside is being unable to understand a program you h

Fair enough about the particular Github comment, but even there I think you are wrong. The architectural downside is being unable to understand a program you have written: "However, if the type does not have an explicit impl for Send/Sync, I don't know how to even figure this out -- I would have to chase all types (including safe ones, and across all abstractions) of all fields recursively and then check when they are Send/Sync... that's way too error-prone." This doesn't just talk about his particular proof tool being unable to understand this. It's about any Rust developer being unable to easily understand the types used by their programs, using only standard library constructs. (If anything, this should be easier for tools than for humans.)