This may be too much advanced type theory for a useful language.
You can go all the way to formal verification. This is not enough for that. Or you can stop at the point all memory error holes have been plugged. That's more useful.
You can go way overboard with templates/macros/traits/generics. Remember C++ and Boost. I understand that Boost is now deprecated.
I should work some more on my solution to the back-reference problem in Rust. The general idea is that Rc/Weak/upgrade/downgrade provide enough expressive power for back references, but the ergonomics are awful. That could be fixed, and some of the checking moved to compile time for the single owner/multiple users case.
> You can go way overboard with templates/macros/traits/generics.
You can go overboard on any language concept imaginable, but conflating all these mechanisms makes it sound like you haven't interacted much with non-C++ languages—particularly since rust doesn't have templates or anything like templates, traits are an entirely unrelated composition mechanism, and macros are entirely unrelated to the type discussion in the article.
This isn't really "advanced type theory" so much as picking up programming language developments from the 90s. I suppose it's "advanced" in the sense that it's a proper type system and not a glorified macro ala templating, but how is that a bad thing?
Boost is as actual as ever.
Also the way nowadays is with constexpr, templates, and around the corner, static reflection.
Thanks for posting this! As a long-time Rust user (and contributor, in the good old days), the thing that has always fascinated me about Rust is the healthy balance it strikes between academic brilliance and industry pragmatism. Radical changes like the ones suggested by the OP risk damaging that balance IMO. I'd rather put up with some language quirks and see Rust achieve "boring technology" status...
But who knows, maybe the "academic brilliance" from the article is more pragmatic than I give it credit for. I sure hope for it if these changes ever go through.