Those tend to be the mistakes that I take for granted any seasoned programmer can detect and fix almost instantaneously and effortlessly. (Of course, not because programmers are superhuman, but rather because Hindley-Milner is the bare minimum a high-level language should have.) It's pathetic that we're still discussing these in 2017.
> Yes, in some cases those properties can only be verified by proving some invariant equivalent to the Collatz conjecture.
I have yet to see a useful program whose correctness is contingent on the Collatz conjecture being true. But I have seen lots of programs that are much easier to verify by hand than using a type system.
> I'm not too worried if it can't prevent me from invalidating invariants, so long as it can prevent me from making simple mistakes that are obvious in retrospect.
I'm not worried either. I'm just saying that “allow anything to be modified anytime, anywhere” is counterproductive. But if you really want to do it, you can do that in ML and Haskell too: just stuff all your top-level definitions into mutable cells.
Evidently most language creators find it difficult to integrate both interactive programming and static typing, which suggests to me that the problem is not easy. Or maybe there just isn't enough overlap between the groups who value one or the other.
> just stuff all your top-level definitions into mutable cells
That seems like it could be part of a potential solution, but it would require rewriting the program so that everything is implicitly wrapped in the IO monad. And it still doesn't handle the case were you want to add to an existing data type.
Interactivity is one thing. Randomly redefining things is a-whole-nother thing. ML and Haskell are interactive. They just don't stuff absolutely everything in mutable cells like most dynamic languages do.
> That seems like it could be part of a potential solution, but it would require rewriting the program so that everything is implicitly wrapped in the IO monad.
You can't have it both ways: either you have effects and accept that you have effects, or don't have effects and accept that you don't have effects. (IOW, lying is bad.)
Those tend to be the mistakes I make when programming interactively in Python. Forgetting to put a single value into a one-element list. Forgetting to check for None. Misspelling a key in a dictionary. Swapping the order of two arguments in a function call.
Yes, in some cases those properties can only be verified by proving some invariant equivalent to the Collatz conjecture. I'd conjecture that most instances could still be solved by an appropriate type system. I'm not too worried if it can't prevent me from invalidating invariants, so long as it can prevent me from making simple mistakes that are obvious in retrospect.