>Stronger assumptions at compile time allows for higher quality code
this depends very heavily on your definition of higher quality code. I really hate this new trend in language discussions of declaring subjective benefits to be objective.
Stronger compile-time assumptions, by definition, reduce the scope of runtime dynamism, which, for many people is an important feature of say dynamic languages.
Stronger assumptions at compile time are part of a trend of attempting to verify programs formally ahead of time, which is not the only way to produce robust software, but seems to be increasingly treated as such.
What can you do with runtime dynamism that I can’t do with a language using a strong type system with dependant types? You need to know _something_ about the dynamic data else you can’t do anything with it and that starts to suggest there’s a structure you can declare, right?
And what methods do you think are as capable as formal verification? What I mean by that includes formal specification, property based testing, theorem provers etc.
Edit: This reads argumentative but that’s not what I wanted, I’m genuinely interested.
They are, as are pre- and post-conditions; they're not, however, a breakthrough in language design by any means.
https://en.wikipedia.org/wiki/Eiffel_(programming_language)