Right. The whole problem with all this is ergonomics, from the point of view of programmers who don't want to obsess over ownership and type theory. We sort of know how to make this work. It works fine with enough Rc/Weak/etc. But it's a huge pain.

I appreciate people arguing over this. It helps. We've seen proposals from people who are too much into the type theory and not enough into ease of use. I used to do proof of correctness work, where the problem is that proof of correctness people are too into the formalism and not enough into killing bugs.