I look forward to it and hope it helps with at least some of the diverging behavior bits or lack of having a common set of terms that new things can be discussed using. The recent discussion about subtyping, Never, and so on has shown how the lack of agreed-upon definitions can hurt even discussion of the system as it exists now, let alone how one might want to change it.
Yeah, I don’t have good answers for this in particular. It seems that tooling will naturally want to use things that are supported by the language, this included, but I think the issue with this is somewhat magnified by the fact that there isn’t a good canonical typing reference right now for users to not feel like they are fighting the type system because of the choices external to what can be accomplished here, so while it’s a factor, it’s a factor we can’t directly address here, only be mindful of how other decisions may change the perception of how much that impacts users.
For me personally, yes this would be the largest disconnect. I view the lack of soundness as a place for divergent behavior between type-checking implementation to emerge, as an unnecessary lack of safety that could be provided by typing, and as a way where the type system becomes harder to teach and harder to soundly build upon because it doesn’t follow rules people may be familiar with either from theory or other sound type systems in other languages. For languages with type systems I would consider worth comparing, those would be Julia, Elixir, Haskell, Rust, OCaml, and Kotlin. Julia, in particular, is interesting as a comparison as types are entirely optional and allowed to be gradually added, while being as rigorous as all of the others there when provided. Elixir is in a similar position, but the parallels are harder to draw.
The lack of soundness in particular has led to a discussion internally at my work about either implementing our own type checker which does enforce soundness or not using Python in a specific context. I don’t hold either of these options as great and largely a product of somewhat unneeded red tape, but the decision on the level of acceptable risks is outside of my direct influence. Creating our own type-checker without the broader community buying into soundness wouldn’t help, it would only create further divergence between type-checking implementations by adding yet another implementation that does things differently.
Quite bluntly, I don’t think something should claim to be a type checker if its primary purpose is not to check for soundness based on type information with what is currently known to be sound. Anything short of that is just another linter, albeit one that can leverage type information.
That comes into a philosophical difference though that isn’t necessarily useful to what comes next, but I would hope that if someone has bought into the benefits of typing, they would see that a system that can be self-consistent because it has chosen soundness requires less work to understand as there don’t need to be special cases where “pragmatic” decisions interact with each other, and is therefore also easier to teach and harder for there to be a meaningful divergence between type-checkers.
I should also emphasize that I don’t think a sound type system requires everything to be typed or for adding type information to be any harder than it is today, I expect it to be easier because the consistency provided by a sound, self-consistent system should make it easier to teach and document the “right” way, but I do acknowledge that changing existing tools to enforce soundness would cause some projects to need to fix things that are not currently enforced, and it’s definitely something that needs to be kept in mind.
I would be very surprised if people picked rust for type safety as their first choice leaving Python unless they have some other very specific needs as well. I would expect that most people starting from python but wanting stronger benefits from typing as their primary goal would be better served by either Kotlin or Julia as both would have more similarities with their current code.