|
|
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:34 UTC (Mon) by daroc (editor, #160859)
In reply to: circular reasoning is a potential source of unsoundness by NYKevin
Parent article: Rust's next-generation trait solver

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.


to post comments

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.


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