I like Haskell etc. a lot, but I've found that in the very early stages of the project, it's quite important to allow incorrect code and illegal state because you don't know what "correct" means yet. New products are almost always built by making sure the happy path works and not worrying about anything else, because if you worry about anything else, it will take you that much longer to bring something to market.

Languages that prove correctness have the unfortunate position of being most useful once the project has already grown big. At that point, the programming language used has already been decided, and it's usually whatever was popular for toy projects 10 years ago.

I do think we'll see more languages that take the "immutable by default" route, but allow escape hatches for when you really need to break the rules. Even when prototyping, most of your data structures can be immutable, you just occasionally need to monkey-patch something or alter some state from inside a loop.