oskgo

> > I don't think it would make it onto this first slate of goals. But the exercise may be valuable and I do hope that going forward this eoll.be...

It's not enough to handle traits that are explicitly sealed. What about the following case: ```rust mod M1 { pub struct Foo; pub trait Tr1 { const ID1: u32; }...

@Tamschi It's not sealed, at least not in the conventional sense. I've changed the example to add `pub` to things that can be exported. I don't see how one could...

Maybe my notation is a bit imprecise here. The idea is that the contents of `M1` are defined in one crate while everything else is in another. A third crate...

It's sound under current rules because `Tr2::prove` being able to produce a `Proof` without diverging serves as a proof that the `Tr1` and `Tr2` implementations are consistent with each other....

@Ygg01 I probably should have defined `Sealed`. I'll be more explicit in my examples in the future. In case you don't know about the [sealed trait pattern](https://predr.ag/blog/definitive-guide-to-sealed-traits-in-rust/), `Sealed` is a...