|
|
Log in / Subscribe / Register

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

The "obvious" concern I would have with this is user-defined unsafe traits.

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?


to post comments

circular reasoning is a potential source of unsoundness

Posted Mar 30, 2026 17:34 UTC (Mon) by daroc (editor, #160859) [Link] (2 responses)

I suspect the answer is the same as any other unsafe thing that breaks the language: "don't do that". You can't have a coinductive loop without at least one trait implementation block, so for an unsafe trait, that unsafe trait implementation is the specific use of unsafe that could break things.

But yes, one of the remaining open items to work on before the next-generation trait solver can be stabilized is documentation, which will presumably include documenting how any proposed changes to the type system interact with unsafe code.

circular reasoning is a potential source of unsoundness

Posted Mar 31, 2026 1:22 UTC (Tue) by NYKevin (subscriber, #129325) [Link] (1 responses)

Sure, but what happens if someone has already constructed an incomplete loop, which is only sound in the current version of Rust because coinduction is impossible (and therefore the loop cannot be closed)? You could imagine a situation where the "missing link" of the loop is implementable in safe code, and that would retroactively render the existing (unsafe) implementations unsound.

I don't think you can fix it with an edition, either. Trait solving is semantic, not syntactic.

circular reasoning is a potential source of unsoundness

Posted Mar 31, 2026 11:49 UTC (Tue) by daroc (editor, #160859) [Link]

Oh, I see your point! That's an interesting thought.

You're right; I'm not sure how that ought to be handled. I don't think the list of considerations for unsafe code to be aware of have changed very much over time.

Perhaps it would still be possible to make it an edition change by tagging each trait implementation with which edition it comes from, and disallowing coinductive cycles that dip into previous editions, but that's pure speculation on my part.

circular reasoning is a potential source of unsoundness

Posted Mar 31, 2026 3:36 UTC (Tue) by theemathas (guest, #183008) [Link]

This exact issue has been raised in https://github.com/rust-lang/rust/issues/149743

There's currently no good answer to this yet.


Copyright © 2026, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds