Oh this is really good!

I wrote https://github.com/Ericson2314/rust-papers a decade ago for a slightly different purpose, but fundamentally we agree.

For those trying to grok their stuff after reading the blog post, consider this.

The borrow checker vs type checker distinction is a hack, a hack that works by relegating a bunch of stuff to be "second class". Second class means that the stuff only occurs within functions, and never across function boundaries.

Proper type theories don't have this "within function, between function" distinction. Just as in the lambda calculus, you can slap a lambda around any term, in "platonic rust" you should be able to get any fragment and make it a reusable abstraction.

The author's here lens is async, which is a good point that since we need to be able to slice apart functions into smaller fragments with the boundaries at await, we need this abstraction ability. With today's Rust in contrast, the only way to do safe manual non-cheating awake would instead to be drasticly limit where one could "await" in practice, to never catch this interesting stuff in action.

In my thing I hadn't considered async at all, but was considering a kind of dual thing. Since these inconsievable types do in fact exist (in a Rust Done Right), and since we can also combine our little functions into a bigger function, then the inescable conclusion is that locations do not have a single fixed type, but have types that vary at different points in the control flow graph. (You can try model the control flow graph as a bunch of small functions and moves, but this runs afowl of non-movable stuff, including borrowed stuff, the ur-non-moveable stuff).

Finally, if we're again trying to make everything first class to have a language without cheating and frustration artificial limits on where abstraction boundaries go, we have to consider not just static locations changing type, but also pointers changing type. (We don't want to liberate some types of locations but not others.) That's where my thing comes in — references that have one type for the pointee at the beginning of the lifetime, and another type at the end.

This stuff might be mind blowing, but if should be seriously pressude. Having second class concepts in the language breeds epiccycles over time. It's how you get C++. Taking the time to make everything first class like this might be scary, but it yields a much more "stable design" that is much more likely to stand the test of time.

This is going to take some serious reading.

I've been struggling with a related problem over at [1]. Feel free to read this, but it's nowhere near finished. I'm trying to figure out how to do back references cleanly and safely. The basic approach I'm taking is

- We can do just about everything useful with Rc, Weak, RefCell, borrow(), borrow_mut(), upgrade, and downgrade. But it's really wordy and there's a lot of run time overhead. Can we fix the ergonomics, for at least the single-owner case? Probably. The general idea is to be able to write a field access to a weak link as

    sometype.name

    sometype.upgrade().unwrap().borrow().name

What I've discovered so far is that the way to write about this is to come up with real-word use cases, then work on the machinery. Otherwise you get lost in type theory. The "Why" has to precede the "How" to get buy-in.

I notice this paper is (2024). Any progress?

[1] https://github.com/John-Nagle/technotes/blob/main/docs/rust/...