This does not prevent you from proving the program correct by hand. Regrettably that is rarely done, but could in principle be done regardless of the type system of the language. Of course that would require you to write a specification of the of the features you want to implement, which might be messy depending on your problem domain.
I'm not sure what this has to do with me. Again, I never said you can't prove programs correct. I simply stated how I work: I don't run my code nearly as often as I would when working in C.
