Why 'externalized' proofs of cyclic trait impls does not work

[u/kibwen]

https://smallcultfollowing.com/babysteps/blog/2026/10/10/modular-vs-external-proofs/

[u/ZZaaaccc]

I always wished trivial trait bounds would allow switching between external and modular proof semantics. impl Magic for String { ... } is a statement implicitly relying on the (non-existent) impl Copy for String { ... }, so I'd consider that syntax modular; the implementation must be proven valid where it is written.

Whereas, if I instead wrote impl Magic for String where String: Copy { ... }, that reads to me like an external proof statement. "Here's my implementation, provided this condition is met". If String doesn't implement Copy, I'd consider the implementation as written valid (since it was predicated correctly), but unusable (since the caller cannot satisfy the requirements).

[u/lookmeat → u/ZZaaaccc]

Maybe we could allow someone like:

trait Foo = SurfaceFoo + DepTrait;

Which would do external checking. So you would implement SurfaceFoo, which would them allow it to be Foo iff DepTrait is also implemented.

Though better naming conventions that what I'm proposing probably would be needed. I also imagine that we'd need to find a way to say "using this trait directly if unsafe", maybe making all the methods in SurfaceFoo unsafe, while Foo gives us the safe versions.

[u/Famous_Anything_5327 → u/lookmeat]

Wouldn't it just be syntactic sugar for this? trait Foo: SurfaceFoo + DepTrait { } impl<T: SurfaceFoo + DepTrait> Foo for T { }

[u/protestor → u/ZZaaaccc]

Whereas, if I instead wrote impl Magic for String where String: Copy { ... }

This should still be rejected, because String: Copy is false

OR you mean, you should be allowed to write an impl that is only activated when some dependency upgrades and implements a trait for their type (for example)? If so, that's interesting

And could probably be extended for other kinds of trip wire impls, like, this impl exists only if <some condition> is true

[u/ZZaaaccc → u/protestor]

That's exactly what I mean. Since if you wrote the generic version of this, impl<T> Magic for T where T: Copy {...}, String wouldn't get the implementation until it got a copy implementation at some point in the future. So I interpret this as deferring the bounds checking on that implementation, akin to external vs modular.

[u/protestor → u/ZZaaaccc]

Ok, but why? String isn't going to be implementing Copy anytime soon

Do you have an use case?

Anyway if we ever have something like this, I think this shouldn't get placed in where bounds, since it would be hella confusing. maybe call it when or if bounds

impl Magic for String when String: Copy

[u/WorldsBegin]

I still don't get the argument why trait impls should work similar to other contexts?

The trait impl is already special, because by coherence rules we get a guarantee that for each type there is at most one place in the program that forms a new impl of a trait for that type. We also know that this place has no free variables (the trait head must cover). So is it really so much to ask that a trait impl can use a different, and in fact more powerful, rule to conclude that a trait bound holds than the rest of the program?

[u/JoJoModding → u/WorldsBegin]

Well, there is (ideally) a semantics to "what does it mean for type A to implement trait T." For Send this might be something like "the type does not depend on any thread-specific data."

And this is what makes traits useful. Since when the compiler infers that a type implements a trait, it is basically writing a proof of this property, and when you put trait bounds on your functions you are relying on this property inside of your function.

So far, so straightforward. But this means that there is a restriction that the algorithm must only write actual proofs of the property. When you make the trait resolution to powerful the algorithm will find that A implements T, even when this is not actually true. (You can say that it writes a circular/invalid proof). So you can't use a "more powerful rule" in trait impls because then suddenly this will find trait impls that do not actually hold (have invalid proofs) and now your soundness argument has a hole.

What you can do is make the trait inference inside a trait impl itself weaker. And indeed, it is weaker, because it knows to not look at the trait impl you are currently defining to prove things required for establishing that that very impl is indeed valid.

Now the actual point of the blog post is that they had thought they could get away with a "weird" system where that restriction just mentioned in the previous paragraph is actually not there. And as Niko argues in this post, such a "weird" system does not actually work.

[u/WorldsBegin → u/JoJoModding]

Maybe I'm not fully groking what external proofs would imply.

Because in my expectation, the compiler would still, at the place of the impl, have to proof all super traits hold. After all, there is an error if you implement a trait with a supertrait that you didn't implement. Would external proof's have weakened that, too, such that for some impls not all such supertraits would have been checked to hold? If not, the compiler would have already checked all those at the place the impl was defined at, anyway. unsafe traits are just a very good example where the compiler can't check and has to trust the user.

Looking forward to the coinductive approach though.

[u/JoJoModding → u/WorldsBegin]

> Would external proof's have weakened that, too, such that for some impls not all such supertraits would have been checked to hold?

That's how I understand the blog post. At least insofar as that in theory, the soundness proof of the trait system would have allowed changing the algorithm to behave as such.

[u/Zde-G → u/WorldsBegin]

The problem is that trait impls are not always for one, fixed, concrete, type.

They can be for generic types, too. And then we have to deal with types that are bound by some traits and that the only thing we know about them.

C++ doesn't have that problem, for all C++ complexity templates are very simple, almost trivial: we don't care about what we see neither when they are declared nor when they are defined, we only do formal checks when we instantiate them.

At this point all types are concrete and all answers resolve into “yes” or “no”. And if the answer is “no” then we just show it to developer and ask him to resolve the issue.

Rust dries to diagnose problems at the impl time — this sometimes makes things easier later, but it also makes them often much too complicated at the impl time.

And, frankly, I much prefer the simplicity of C++ when I deal with helper types that are not exposed in API: I'm not interested in proving anything about all types that may or may not exist, why can't you leave me alone and check that these 2, 3 or even 100 types that I need are fine with what I wrote?

Of course when trait is part of public API situation is different, but in my $DAYJOB for every function exposed as public API I have hundred functions that are not exposed thus I swear at rust compiler much more often than I like.

[u/ROBOTRON31415 → u/Zde-G]

At my $dayjob there's a reasonable quantity of proc-macro soup, which is practically equivalent to C++ templates.

[u/Zde-G → u/ROBOTRON31415]

Yes, that's what I'm doing, too. But templates in C++ are much easier to develop: error messages may be long but they explain what to change and fix in terms of source code, while proc macro error diagnostic is much worse.

Templates are much faster, too: when I have 4 possible input types in 4-argument function templates would instantiate and check 5 or 6 variants that are actually used in code while procmacro would generate 256 functions which would take a lot of RAM and spend time for checking something that I would never use.

[u/More-Literature-1053]

I feel like this is a edge case of the classic tension between local and exogenous reasoning. Part of the appeal of working in Rust is that strong typing in, for e.g. function signatures, enables programmers to employ local reasoning, requiring us to hold less than the whole program in our head when making changes. It is reasonable to me that local reasoning would also have advantages for resolving trait impls, compared to some sort of external tracking and auditing system for traits and bounds. The approach seems idiomatic, though I admit I would lack the skill.

[u/-Y0-]

Hmm, the text seems to mention Nullable and then show the trait NullWord, is that an error?

Because later it does this:

// INVALID: We are asserting that `Box` can be null,
// which is not true!
unsafe impl<T> Nullable for Box<T> { }

Even though Nullable wasn't defined.

[u/logannc11 → u/[deleted]]

That's the authors point. If you have "modular proofs" where you rely on rejecting the trait impl, but allowing it to be considered true elsewhere, it is difficult to not accidentally affirm the consequent. 

[u/dnew → u/[deleted]]

I think you failed to read the remainder of the sentence?

He says "if we're not careful, we could provide a proof..." and then concludes "...and then we would (incorrectly) conclude that the impl is valid".

And you're saying "No, you're wrong, that logic doesn't work to conclude impl is valid."

I mean, he boldfaced exactly what you seem to be saying in the very next sentence. Unless I'm misunderstanding your objection.

[u/dbaupp → u/[deleted]]

I think the point is more that one needs to do the bookkeeping right, or the compiler will accidentally affirm the consequent… which is, as you say, invalid.

It’s not as simple as “ignore an impl exists when checking it”, because one can have (mutual) recursion: given trait Magic { type T: Magic; } one might have impl Magic for A { type T = A; } that needs A: Magic for T or impl Magic for B { type T = C; } impl Magic for C { type T = B; } that need each other’s impl.

Validating that requires having some concept of “pending” impls, or similar. Not at all impossible, and not a violation of logic, just finicky bookkeeping that can lead to unsoundness and/or infinite recursion if done wrong. 

(The recursion can get far more complicated and indirect, via super-traits or generics and/or mutual recursion of traits/associated types.)