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.

See http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond... for some interesting stuff.