[Barrin92]

>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.

[exdsq]

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.