circular reasoning is a potential source of unsoundness [LWN.net]

circular reasoning is a potential source of unsoundness

Posted Mar 31, 2026 1:22 UTC (Tue) 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

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.

to post comments

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.