>>12
Designing functions to only depend on their input and have well-designated output(s), and which usually don't change their input has proven a useful rule of the thumb for me, regardless of programming language. It does help a lot when testing. While most of us don't use lazy evaluation, currying, and fancy closure tricks too often, the design principles lead to more robust programs in general. Such style of programming also fits well with bottom-up programming in languages which support interactive development. I don't know if there's that much high-level impact, but it helps a lot when it comes to the bulk of the code. I tend to whip up some imperative things sometimes when it comes to interconnecting components, while keeping simpler components designed in a functional style.
I don't claim that anything is "provably" correct, since the languages I tend to use are C and Lisp, however if I were to use Haskell or ML(which I do know to some degree), you could say that a whole class of typing errors are removed, but that does nothing to protect against human logic errors, which are much more dangerous and tricky overall. If you actually want to "prove" that the application does what you want it to do, it's possible to do it in some cases via theorem provers, but the process always seemed very tedious to me, and in most cases a waste of effort unless someone pays you to do it, or is a requirement of the project.