You raise some good points but
maximum' :: (Ord a) => [a] -> a
maximum' [] = error "maximum of empty list"
maximum' [x] = x
maximum’(x:xs) = maximum’(xs)
In Haskell is logically wrong, and type checks. If you want probably correct software you need a theorem prover and it’s a whole new level of difficulty, that most of us can’t afford.
While true, that with some assumptions and a type system on par with the Haskell’s type system you can go a long way when refactoring ( I would highly recommend the https://www.cs.ox.ac.uk/publications/books/functional/
book to get an idea of what it’s about), it’s not a way to prove your software is correct.
We also have some pretty great tools to insure correctness : dialyzer + prop check + unit tests can go a long way.
Not to say that you’re wrong to want a strong/static type system. I wish I had it when working with elixir or erlang, but then again, the benefits of the os_like ecosystem and the simplicity of these languages compensate the lack of static typing for me.
