What does it mean for a language to be statically typed?

Question

My understanding is that it means that one can potentially write a program to formally prove that a program written in a statically typed language will be free of a certain (small) subset of defects.

My problem with this is as follows:

Assume that we have two turing complete languages, A and B. A is presumed to be 'type safe' and 'B' is presumed not to be. Suppose I am given a program L to check the correctness of any program written in A. What is to stop me from translating any program written in B to A, applying L. If P translates from A to B then why isn't PL a valid type checker for any program written in B?

I'm trained in Algebra and am only just starting to study CS so there might be some obvious reason that this doesn't work but I would very much like to know. This whole 'type safety' thing has smelt fishy to me for a while.

Answer 1

If you can translate every B' (a program written in B) into an equivalent A' (which is correct if B' is), then language B enjoys just as much "type-safety" as language A (in a theoretical sense, of course;-) -- basically this would mean that B is such that you can do perfect type inferencing. But that's extremely limited for a dynamic language -- e.g., consider:

if userinput() = 'bah':
    thefun(23)
else:
    thefun('gotcha')

where thefun (let's assume) is typesafe for int argument, but not for str argument. Now -- how do you translate this to language A in the first place...?