I think it also dosen't really matter, in practice. While it would be nice to have a language where, if it compiles, its provably correct (for some definition o

I think it also dosen't really matter, in practice. While it would be nice to have a language where, if it compiles, its provably correct (for some definition of correct, defined by whatever the language states, I guess), we don't need that extreme to be useful. I've personally found myself dissatisfied with dynamically typed languages after spending the bulk of the past ten years writing in them (Clojure and Python mainly), because the kinds of errors that I most commonly find in my own code are ones that even basic static types like in Java or even C++ can detect (basic type mismatches) while in dynamic languages, to catch these early, the unit tests need to have exercised that particular case. The problem with that is it puts the burden of thinking of and testing for these cases on me, but we all know that exhaustive tests are rare and hard to maintain. Property-based testing helps, but again, it depends on the data generated whether or not a type mismatch will get tested. Statically typed languages prevent this type of bug, this makes them useful to me, even if they can't prove the absence of all bugs or can't prove that a program won't halt.