If you have to do tests to verify your program (not everything can be proven after all) then the cost would indeed skyrocket. For instance, you need to account for every combination of inputs (a potentially infinite set) and behavior may depend on some hidden unknown variables.
You may be interested in one of my old posts about the curry-howard isomorphism the comments are pretty good too. I should also point out though, that even pure FP languages don't really exploit this property. For instance when dividing by 0, but also good old overflow problems.
We're a place where coders share, stay up-to-date and grow their careers.
We strive for transparency and don't collect excess data.