You seem to be saying that developers can make logic errors despite expressive types. Of course that’s true—type systems are a first pass to absolve us from the

You seem to be saying that developers can make logic errors despite expressive types. Of course that’s true—type systems are a first pass to absolve us from the trivial errors that otherwise waste our time. I don’t agree that lazy programmers will add optionality to please compilers rather than fix their program logic. In languages where optional types are ubiquitous, you usually see people avoiding needless optionality, because it’s simply easier.