We held our first "lang team design meeting" today, and dedicated an hour to discussing this topic. You can find the minutes on the lang-team repo, and there is a recording on YouTube. I don't have time for a detailed write-up, but it seemed like we were centralizing on a solution based around strengthening negative reasoning. In particular, I think with a rough set of actions like:
- Introduce some (unstable) technique to
impl<T> !DerefMut for &Tshortly- this would prevent the
impl DerefMut for &LocalTypewe've seen in this thread
- this would prevent the
- Improve the documentation of
new_uncheckedto describe the invariants to be proven and to emphasize that, in order to rely on 'negative reasoning', there should be an explicit negative impl (presently only available on nightly, but coherence can temporarily be used to similar effect for non-fundamental types; we don't think this is a good basis long term though)- @RalfJung also expects to do a more formal treatment here to increase confidence
- Introduce or sketch out what it might look like to permit negative impls of this kind more generally
- this is a larger design effort but we have lots of pre-existing thoughts that can be collated