I think that having a compromise between types and untyped is best.
So first, have a type all other types can be cast to, call it object and allow it to perform generic operations. Then have a type that can be cast to all other types, call it null. These two gives you a lot of the nice parts of untyped languages while still allowing for tooling like quick refactoring or name completions. When I code in a system lacking any of these I feel way slower.
On the contrary, I find myself more productive in languages that do not have pervasive null because then I don't have to manually reason about which values might be null.
People build huge programs in untyped languages, reasoning about null is trivial in comparison. The cost of not having null is that all initialization and generic code gets much harder to write and work with, the benefit is that once in a blue moon you get a hard to debug null pointer error. I've worked as a software engineer at large companies for years and never had a hard to debug null pointer error, so at least to me they don't exist.
Edit: I feel the main problem with over engineered type systems is the same as for any over engineered library. Instead of just cleanly solving a few key issues they recreate a programming language in their types and even worse they force you to use said programming language if you want to code. The C# style type system has all guarantees I need with very few limitations, if I need more guarantees I'll just write them in code.
When you have a hammer everything looks like a nail. A language theorist trying to fix issues will of course look at changing the language first, doesn't mean he is right.
People also used to build huge castles without any power tools. That something can be done with a tool is not an argument for that tool to be efficient or even good at it.
That is your opinion though, my opinion is that type systems stricter than C# detracts rather than adds and most agree with me. People who like to discuss language theory don't, of course, since the major reasons to discuss language theory is that the popular languages don't have the features you like or that you want to specifically solve software engineering problems in the language level rather than the code level.
It's not possible to solve problems at the code level. That would require every single developer writing in that language to account for all the holes in the type systems. That's completely unrealistic. And can be seen to be disastrous in practice. I mean just walk through some python code. There are almost no None or manual type checks. These are just bombs waiting to explode.
The problem with type systems like C# and Java are that they are too strict. Look at the polymorphism mess in those languages. The entire reason people hate static typing is because of the shittiness of precisely those two languages. That's the reason we need better type systems.
Each restriction at the language level adds a cost. The cost of having simple nullable types like you do in Java or C# is worth it. The cost of trying to formalize away null errors isn't. That is what I think. Just because you can do something doesn't mean that you should, so just because you can ensure no errors of class X happens at a language level doesn't mean that enforcing that at a language level is the best solution.
> It's not possible to solve problems at the code level. That would require every single developer writing in that language to account for all the holes in the type systems.
I'm not sure what you mean with this. Of course you can fix this at a code level. Not for the entire world of course, but you can do it in the code you write.
So? People build huge programs in typed languages as well. Whether people do something one way says nothing about how that approach compares to others.
> The cost of not having null is that all initialization and generic code gets much harder to write and work with
Could you provide examples of how lack of a null value makes these so much harder?
> the benefit is that once in a blue moon you get a hard to debug null pointer error
This is like saying that the only drawback to not having smart pointers in C++ is that once in a blue moon you get a hard to debug segfault. Sure, segfaults may be more common when working with raw pointers, but there are also substantial drawbacks in terms of mental overhead due to potential uncertainties about ownership/lifetimes.
In that vein, NPE/NREs are not the only drawback to a type system with null; the additional state space means mental overhead for the programmer and an increased risk of mistakes.
In addition, introducing universal nullability into a type system entails performance penalties. Null increases the state space of a given type, so if a type uses all of its bits (e.g., int) you need to introduce indirections (java.lang.Integer) or increase the size of the type (C# Nullable<int>/int?) to shoehorn in a null value.
> Instead of just cleanly solving a few key issues they recreate a programming language in their types and even worse they force you to use said programming language if you want to code.
I'm not sure what you're trying to get at here. This seems to be a criticism of generics/similar mechanisms, but you seem to be fine with C#/similar type systems, which has generics and makes use of them?
What's especially confusing is that type systems with generics and null are precisely equivalent to type systems with generics without null, as all instances of nullable types can be replaced with Option<T>/Optional<T>/Nullable<T>/etc. (with appropriate sugar for other operations, of course). So I'm a little lost as to what the problem is.
So first, have a type all other types can be cast to, call it object and allow it to perform generic operations. Then have a type that can be cast to all other types, call it null. These two gives you a lot of the nice parts of untyped languages while still allowing for tooling like quick refactoring or name completions. When I code in a system lacking any of these I feel way slower.