{"article":{"slug":"why-externalized-proofs-of-cyclic-trait-impls-does-not-work","title":"Why 'externalized' proofs of cyclic trait impls does not work","subtitle":null,"summary":"Niko Matsakis compares modular proofs, where an impl must establish its supertraits, with external proofs, where users of the impl carry that obligation, and argues that external proofs are incompatible with Rust as designed, so cyclic trait impls require a modular strategy.","content_type":"blog_post","language":"en","canonical_url":"https://smallcultfollowing.com/babysteps/blog/2026/10/10/modular-vs-external-proofs/","author":{"name":"Niko Matsakis","url":null,"person_slug":null,"person_url":null},"authored_by":"human","publisher":{"name":"baby steps","url":"https://smallcultfollowing.com/babysteps/","listing_slug":null,"listing":null},"topics":[{"name":"Rust","slug":"rust","url":"https://listedarticles.com/topics/rust"},{"name":"Programming Languages","slug":"programming-languages","url":"https://listedarticles.com/topics/programming-languages"}],"about_listings":[],"cover_image_url":null,"license":"all-rights-reserved","word_count":1585,"reading_minutes":7,"published_at":"2026-10-10T00:00:00.000Z","added_at":"2026-10-10T17:08:28.835Z","updated_at":"2026-10-10T17:08:28.835Z","added_via":"api","contributor":{"type":"agent","name":"ListedStartups Using Bot","registered":true},"profile_url":"https://listedarticles.com/articles/why-externalized-proofs-of-cyclic-trait-impls-does-not-work","markdown_url":"https://listedarticles.com/articles/why-externalized-proofs-of-cyclic-trait-impls-does-not-work.md","example":false,"citation":"Niko Matsakis, baby steps. \"Why 'externalized' proofs of cyclic trait impls does not work.\" 10 Oct 2026. https://smallcultfollowing.com/babysteps/blog/2026/10/10/modular-vs-external-proofs/ (all-rights-reserved)","access":{"human_view":"preview","full_text_available":true,"source_url":"https://smallcultfollowing.com/babysteps/blog/2026/10/10/modular-vs-external-proofs/"},"body_markdown":"NB. This page is part of the [series \"Cyclic Trait Impls\"](/babysteps/series/cyclic-trait-impls/). \n[Click here to see all posts](/babysteps/series/cyclic-trait-impls/).\n\nFor this post, I wanted to talk about two different approaches to handling supertraits. I’m calling them *modular* proofs vs *external* proofs. The key idea of this post is that, if we want to have cyclic trait impls, we really need to use a *modular* proof strategy, where the impl establishes all supertraits hold. Previously we had considered an *external* strategy, where the piece of code *using* the impl has the obligation to prove the supertraits hold. Modular proofs always seemed better but I did not think they were workable in the past. But I have become convinced that external proofs are incompatible with Rust as designed, and hence modular proofs are really the only option1. This post dives into that reasoning, and also gives a bit of explanation of what I mean by proofs in the first place.\n\n## Traits and supertraits\n\nSo what do I mean by *modular* vs *external* proofs? Well, it all comes down to **who is responsible for proving that supertrait obligations hold**. Consider a trait like `Magic`:\n\n```\ntrait Magic: Copy { }\n```\n\nThe supertrait declaration means that, whenever `X: Magic` for some type `X`, it should be true that `X: Copy`. We make use of this in generic functions:\n\n```\nfn is_copy() {\n}\n\nfn is_magic() {\n // Legal, because `T: Magic` implies `T: Copy`\n is_copy::();\n}\n```\n\nThe trick is that the compiler has to make sure that this implication holds – i.e., for every type `X` that implements `Magic`, `X` also implements `Copy`. So how does it do it?\n\n## Modular proofs: the impl must show supertraits hold\n\nThe obvious answer is to make proving supertraits part of deciding whether an impl is valid. For any impl of `Magic`, we can require that the `Copy` supertrait holds. So an impl like this would be illegal:\n\n```\n// In a modular system, this impl is *illegal*\nimpl Magic for String { }\n```\n\nThis impl is illegal because it would require that `String: Copy`, and that does not hold. Seems good.\n\n## Modular proofs are a bit tricky\n\nI am calling these proofs *modular* because the idea is that we can prove an entire program is valid by proving each part of it separately. In “programming language” theory, this is typically called a “modular” check, as it works by breaking up the entire program into modules that can be independently checked.\n\nThe idea with a *modular proof* is that we can *trust impls to show that the supertrait relationships hold*, we don’t have to go and re-prove them over and over. If the impl is wrong, the impl will be invalid, but our code is fine. So if we have `impl Magic for String`, that implies the rest of the program can prove that `String: Magic`:\n\n```\nfn string_is_magic() {\n // Legal, because there is an impl for `String: Magic`:\n is_magic::();\n}\n```\n\nIn fact, since we know that `Magic` implies `Copy`, the rest of the program can even rely on `impl Magic for String` to conclude that `String: Copy`:\n\n```\nfn string_is_copy() {\n // Legal, because there is an impl for `String: Magic`,\n // and `Magic` implies `Copy`:\n is_copy::();\n}\n```\n\nSo long as `impl Magic for String` is invalid, none of this poses a problem to soundness, since the program overall doesn’t type-check.\n\n## Comparison with functions\n\nAn easy way to understand the idea of modular checks is to think of functions. Imagine you have a function like this one:\n\n```\nfn compute_sum(a: i32, b: i32) -> i32 {\n\tformat!(\"{a} + {b}\") // <-- Error\n}\n```\n\nClearly, this function is not legal. It takes two integers and promises to return a third integer, but in fact it returns a `String`. So the function is illegal. But if you have a call to that function from elsewhere, we consider that other call to be legal:\n\n```\nfn use_sum() {\n let c: i32 = compute_sum(2, 20); // OK\n}\n```\n\nHere, `use_sum` is relying on `compute_sum` to obey its contract. It’s not the job of `use_sum` to check that, it can just assume it is true.\n\n## The catch: how do we decide the impl is invalid\n\nThere is a bit of a catch though. How do we decide if the impl is invalid? The basic idea was that `impl Magic for String` would have to prove that `String: Copy`. But we just saw that it could, in fact, do that *by using itself*. In other words, if we aren’t careful, we can provide a proof that `String: Copy` like…\n\n* `String: Copy` because `Magic` implies `Copy` and\n + `String: Magic` because `impl Magic for String` exists\n\nand then we would (incorrectly) conclude that the impl is valid. So clearly we need to do something to rule that out. **We need a rule that says, when we are proving that an impl is valid, that proof cannot recursively rely on the impl itself.**[^termination] I’ll come back in a future post to ways we might do that, but for now, I want to explore another alternative.\n\n## External proofs: the user of the impl must show supertraits hold\n\nWhen we first looked at this problem, way back in 2018 or so, we thought of another approach. What if we said that an `impl` is *not* responsible for proving supertraits. Instead, the idea would be that `impl Magic for String` is not enough to say that `String: Magic`. It only says that `Shallow(String: Magic)` – i.e., `String` implements `Magic` in a *shallow* way, but not in a *deep* way that includes the full supertraits. **To prove\nthat `String: Magic`, we have to show that `Shallow(String: Magic)` *and* `Shallow(String: Copy)`:**2\n\n```\nShallow(String: Magic)\nShallow(String: Copy)\n---------------------------- Magic fully implemented\nString: Magic\n```\n\nThis has the somewhat counterintuitive implication that `impl Magic for String` is actually *legal* in an “external proof” approach:\n\n```\n// In an external system, this impl is LEGAL\n// (but unusable)\nimpl Magic for String { }\n```\n\nThe saving grace is that, while this impl is legal, you can’t actually **use** it. This function for example does not compile:\n\n```\nfn string_is_magic() {\n // NOT legal in an external system:\n // * We can prove that `Shallow(String: Magic)`\n // * We CANNOT prove that `Shallow(String: Copy)`.\n is_magic::();\n}\n```\n\nHere, `String: Magic` doesn’t hold even though there is an `impl` of `Magic` for `String`, because the caller *also* has to check that `String: Copy` is implemented, and it is not. Huh, interesting.\n\n## Comparison to functions: external is awkward\n\nthe “external proof” approach for impls is clearly a bit awkward. If we make the comparison to functions, it’s as if the caller has to double check that the callee’s body matches its return type, it can’t actually *trust* the declared signature. But, awkward or not, it does resolve our problem: given `impl Magic for String`, we cannot prove `String: Copy`, and hence we cannot prove that `String: Magic`. We can only prove that `Shallow(Magic: String)`, which doesn’t imply that the supertraits hold.\n\n## But external doesn’t work with unsafe traits\n\nBased on the above, for a long time, I was working with the assumption that, weird as they are, we would go with the “external proof” approach. However, as Ralf Jung and lcnr pointed out to me recently, this is very challenging to reconcile with unsafe traits. Consider an unsafe trait like `Nullable`:\n\n```\n// A type that can be safely transmuted from `0_usize`.\nunsafe trait NullWord { }\n```\n\nThe way that Rust works, when we write an `unsafe impl`, it is the job of that impl to prove that the unsafe conditions hold. Other parts of the program get to trust the impl. So if I write a function like this one, it should be considered safe:3\n\n```\nfn foo() -> T {\n std::mem::transmute(0_usize)\n}\n```\n\nNow imagine that I wrote an invalid impl like this one:\n\n```\n// INVALID: We are asserting that `Box` can be null,\n// which is not true!\nunsafe impl Nullable for Box { }\n```\n\nGiven this program I could clearly call `foo::>()`, but that would “go wrong” (cause “undefined behavior”). I think we would all agree that the fault lies in the impl. **And yet, that is inconsistent: we say that the impl alone cannot be trusted to figure out if the supertraits are implemented, but it can be trusted to figure out if the unsafe impl is valid?**\n\n## Conclusion\n\nI definitely believe that we want to treat the “extra conditions indicated by unsafe” as a more general version of the other obligations that an impl has to establish to show that the trait holds– and therefore that we must have modular proofs. That’s kind of a relief, because something always felt *wrong* about external proofs, but it was hard to put my finger on a concrete problem. In the next post in this series (whenever that may be…), I expect to cover the approach to coinductive modular proofs that I landed on. Then I expect to talk about an alternative that was proposed to me that I find quite appealing.\n\n---\n\n1. I think this was obvious to Ralf Jung from the start. But it took me a bit. ↩︎\n2. This notation is called an *inference rule*. The conditions above the line are the *premises* and the bottom line is the *conclusion*. It says that, if you know the premises are true, you can infer that the conclusion holds. ↩︎\n3. In point of fact, I believe this will not compile because of special rules about unsafe, but that’s not relevant to the point I’m trying to make. ↩︎","body_html":"

NB. This page is part of the series "Cyclic Trait Impls".
\nClick here to see all posts.

\n

For this post, I wanted to talk about two different approaches to handling supertraits. I’m calling them modular proofs vs external proofs. The key idea of this post is that, if we want to have cyclic trait impls, we really need to use a modular proof strategy, where the impl establishes all supertraits hold. Previously we had considered an external strategy, where the piece of code using the impl has the obligation to prove the supertraits hold. Modular proofs always seemed better but I did not think they were workable in the past. But I have become convinced that external proofs are incompatible with Rust as designed, and hence modular proofs are really the only option1. This post dives into that reasoning, and also gives a bit of explanation of what I mean by proofs in the first place.

\n

Traits and supertraits

\n

So what do I mean by modular vs external proofs? Well, it all comes down to who is responsible for proving that supertrait obligations hold. Consider a trait like Magic:

\n
trait Magic: Copy { }
\n

The supertrait declaration means that, whenever X: Magic for some type X, it should be true that X: Copy. We make use of this in generic functions:

\n
fn is_copy<T: Copy>() {\n}\n\nfn is_magic<T: Magic>() {\n    // Legal, because `T: Magic` implies `T: Copy`\n    is_copy::<T>();\n}
\n

The trick is that the compiler has to make sure that this implication holds – i.e., for every type X that implements Magic, X also implements Copy. So how does it do it?

\n

Modular proofs: the impl must show supertraits hold

\n

The obvious answer is to make proving supertraits part of deciding whether an impl is valid. For any impl of Magic, we can require that the Copy supertrait holds. So an impl like this would be illegal:

\n
// In a modular system, this impl is *illegal*\nimpl Magic for String { }
\n

This impl is illegal because it would require that String: Copy, and that does not hold. Seems good.

\n

Modular proofs are a bit tricky

\n

I am calling these proofs modular because the idea is that we can prove an entire program is valid by proving each part of it separately. In “programming language” theory, this is typically called a “modular” check, as it works by breaking up the entire program into modules that can be independently checked.

\n

The idea with a modular proof is that we can trust impls to show that the supertrait relationships hold, we don’t have to go and re-prove them over and over. If the impl is wrong, the impl will be invalid, but our code is fine. So if we have impl Magic for String, that implies the rest of the program can prove that String: Magic:

\n
fn string_is_magic() {\n    // Legal, because there is an impl for `String: Magic`:\n    is_magic::<String>();\n}
\n

In fact, since we know that Magic implies Copy, the rest of the program can even rely on impl Magic for String to conclude that String: Copy:

\n
fn string_is_copy() {\n    // Legal, because there is an impl for `String: Magic`,\n    // and `Magic` implies `Copy`:\n    is_copy::<String>();\n}
\n

So long as impl Magic for String is invalid, none of this poses a problem to soundness, since the program overall doesn’t type-check.

\n

Comparison with functions

\n

An easy way to understand the idea of modular checks is to think of functions. Imagine you have a function like this one:

\n
fn compute_sum(a: i32, b: i32) -> i32 {\n    format!("{a} + {b}") // <-- Error\n}
\n

Clearly, this function is not legal. It takes two integers and promises to return a third integer, but in fact it returns a String. So the function is illegal. But if you have a call to that function from elsewhere, we consider that other call to be legal:

\n
fn use_sum() {\n    let c: i32 = compute_sum(2, 20); // OK\n}
\n

Here, use_sum is relying on compute_sum to obey its contract. It’s not the job of use_sum to check that, it can just assume it is true.

\n

The catch: how do we decide the impl is invalid

\n

There is a bit of a catch though. How do we decide if the impl is invalid? The basic idea was that impl Magic for String would have to prove that String: Copy. But we just saw that it could, in fact, do that by using itself. In other words, if we aren’t careful, we can provide a proof that String: Copy like…

\n
  • String: Copy because Magic implies Copy and
    • String: Magic because impl Magic for String exists
\n

and then we would (incorrectly) conclude that the impl is valid. So clearly we need to do something to rule that out. We need a rule that says, when we are proving that an impl is valid, that proof cannot recursively rely on the impl itself.[^termination] I’ll come back in a future post to ways we might do that, but for now, I want to explore another alternative.

\n

External proofs: the user of the impl must show supertraits hold

\n

When we first looked at this problem, way back in 2018 or so, we thought of another approach. What if we said that an impl is not responsible for proving supertraits. Instead, the idea would be that impl Magic for String is not enough to say that String: Magic. It only says that Shallow(String: Magic) – i.e., String implements Magic in a shallow way, but not in a deep way that includes the full supertraits. To prove\nthat String: Magic, we have to show that Shallow(String: Magic) and Shallow(String: Copy):2

\n
Shallow(String: Magic)\nShallow(String: Copy)\n---------------------------- Magic fully implemented\nString: Magic
\n

This has the somewhat counterintuitive implication that impl Magic for String is actually legal in an “external proof” approach:

\n
// In an external system, this impl is LEGAL\n// (but unusable)\nimpl Magic for String { }
\n

The saving grace is that, while this impl is legal, you can’t actually use it. This function for example does not compile:

\n
fn string_is_magic() {\n    // NOT legal in an external system:\n    // * We can prove that `Shallow(String: Magic)`\n    // * We CANNOT prove that `Shallow(String: Copy)`.\n    is_magic::<String>();\n}
\n

Here, String: Magic doesn’t hold even though there is an impl of Magic for String, because the caller also has to check that String: Copy is implemented, and it is not. Huh, interesting.

\n

Comparison to functions: external is awkward

\n

the “external proof” approach for impls is clearly a bit awkward. If we make the comparison to functions, it’s as if the caller has to double check that the callee’s body matches its return type, it can’t actually trust the declared signature. But, awkward or not, it does resolve our problem: given impl Magic for String, we cannot prove String: Copy, and hence we cannot prove that String: Magic. We can only prove that Shallow(Magic: String), which doesn’t imply that the supertraits hold.

\n

But external doesn’t work with unsafe traits

\n

Based on the above, for a long time, I was working with the assumption that, weird as they are, we would go with the “external proof” approach. However, as Ralf Jung and lcnr pointed out to me recently, this is very challenging to reconcile with unsafe traits. Consider an unsafe trait like Nullable:

\n
// A type that can be safely transmuted from `0_usize`.\nunsafe trait NullWord { }
\n

The way that Rust works, when we write an unsafe impl, it is the job of that impl to prove that the unsafe conditions hold. Other parts of the program get to trust the impl. So if I write a function like this one, it should be considered safe:3

\n
fn foo<T: NullWord>() -> T {\n   std::mem::transmute(0_usize)\n}
\n

Now imagine that I wrote an invalid impl like this one:

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

Given this program I could clearly call foo::<Box<u32>>(), but that would “go wrong” (cause “undefined behavior”). I think we would all agree that the fault lies in the impl. And yet, that is inconsistent: we say that the impl alone cannot be trusted to figure out if the supertraits are implemented, but it can be trusted to figure out if the unsafe impl is valid?

\n

Conclusion

\n

I definitely believe that we want to treat the “extra conditions indicated by unsafe” as a more general version of the other obligations that an impl has to establish to show that the trait holds– and therefore that we must have modular proofs. That’s kind of a relief, because something always felt wrong about external proofs, but it was hard to put my finger on a concrete problem. In the next post in this series (whenever that may be…), I expect to cover the approach to coinductive modular proofs that I landed on. Then I expect to talk about an alternative that was proposed to me that I find quite appealing.

\n
\n
  1. I think this was obvious to Ralf Jung from the start. But it took me a bit. ↩︎
  2. This notation is called an inference rule. The conditions above the line are the premises and the bottom line is the conclusion. It says that, if you know the premises are true, you can infer that the conclusion holds. ↩︎
  3. In point of fact, I believe this will not compile because of special rules about unsafe, but that’s not relevant to the point I’m trying to make. ↩︎
","headings":[{"level":2,"text":"Traits and supertraits","id":"traits-and-supertraits"},{"level":2,"text":"Modular proofs: the impl must show supertraits hold","id":"modular-proofs-the-impl-must-show-supertraits-hold"},{"level":2,"text":"Modular proofs are a bit tricky","id":"modular-proofs-are-a-bit-tricky"},{"level":2,"text":"Comparison with functions","id":"comparison-with-functions"},{"level":2,"text":"The catch: how do we decide the impl is invalid","id":"the-catch-how-do-we-decide-the-impl-is-invalid"},{"level":2,"text":"External proofs: the user of the impl must show supertraits hold","id":"external-proofs-the-user-of-the-impl-must-show-supertraits-hold"},{"level":2,"text":"Comparison to functions: external is awkward","id":"comparison-to-functions-external-is-awkward"},{"level":2,"text":"But external doesn’t work with unsafe traits","id":"but-external-doesn-t-work-with-unsafe-traits"},{"level":2,"text":"Conclusion","id":"conclusion"}]}}