>We have some formal verification, it's called typed systems. Very limited, I know.
Very limited.
In my many years of experience doing software professionally, the serious bugs, that is, the ones that took us more than one day of debugging (after such a bug was able to be reproduced), were the ones that had nothing to do with types but with
* bad understanding of the business rules
* bad fundamental implementation of the problem domain
* misuse / incorrect use of an API or libraries
* API/library behaviour different from what the documentation says.
No type system will save you from them. Type systems don't verify how the code does the correct thing. They only verify that the types moved between functions/modules satisfy certain conditions. Big deal.
Where code reusability implies that your functions should apply to the widest type of circumstances (and thus increasing the scope in which they can be reused), type systems go fundamentally against to this goal, enforcing your functions to go very specific on what they're able to accept and return.
Dynamically typed systems allow for faster coding, and also allow for interactive development which allows for faster, easier testing of individual components as they are developed. Also, the very best dynamically typed systems also allow for redefining / uploading updated function definitions while the code is running, which greatly increases development & testing speed (emphasis added.)
This is not just a claim, this is my personal experience after about 23 years of programming where 90% of those years were spent using statically typed systems.
As for speed, for highly optimized code Java, Haskell, and F# are basically in the same ballpark. Which is, very good speed. Well, Common Lisp (dynamically typed language) is not only in the same ballpark, but faster than them in some cases.
You know what i'm going to choose.
Or, different take on this: If i was going for absolute speed i'd be hacking in C, where no Hindley-Milner type checker gets in the way of clever tricks for gaining that extra bit of performance you need on that tight loop.