Just like no car will ever be able to transfer hundreds of people across an ocean.
That is not the purpose of static types, instead they offer a basic guarantee on correctness, a minimal correctness proof on the structures of the program and in particular a sanity check on your logic to see if the structures implied by your types are in fact inhabited (excluding bottom type).
Or say if the type diagrams on a series of function you are trying to use commute.
If your static type system includes dimenions / physical units, you can spot a lot of typos in formulas. (Of course, you will also be required to add some conversion factors, when you want to express something like "Open as many connections as the sum of number of hard disks plus number of users.")
You're right. I didn't consider this too. Have you tried a language with units?
I've tried it in F# and seen it in Frink. I found it cool but havent found a need for it. I suspect that is at least partially due to being used to not having it in a language.
A friend of mine hacked up his Lisp, with lots of macros, of course, to check units at compile time. I haven't really used his system, but he was quite keen on it.
Yep, someone here added a type check to Ruby, there are some functions through the codebase that check each argument but I've not seen any real life benefit.
First, this is taken outside of context. Second, you're trying to disprove wrong thesis.
Let's take this again into context first.
In the proper context our wrong formulae will be brought up by running functional tests by field expert (or even earlier, by programmer itself). Functional tests, as opposed to unit tests, checks validity of the program as a whole in relation to problem it should solve. So they are much fewer and quite often all external.
So this is actually no-problem.
Let me reconstruct that implicit thesis you're trying to disprove.
As I can suggest from my experience and your nickname, you're trying to disprove thesis that "types solve all problems".
But real people use types not to solve all their programming-related problems, but to solve as many of them as they see fit for the task at hand.
All software processes revolve around simple thesis: the cost of defect elimination is proportional to the time between defect introduction and defect discovery. PSP/TSP, ALL Agile processes, etc.
Type systems greatly reduce that time. As do REPL and unit-tests. But, compared to unit tests, they require much less effort from programmer.
So, yes, we all need testing. Type systems, though, reduce areal of tests to where they naturally belong.
PS
In my opinion, programmer should seek strongly typed language with REPL.
No type checking will ever get that this is simply the wrong formula, computes as (2 * a) + b and was supposed to be 2 * (a + b) .