A recent conversation with Mark Miller resulted in distinguishing the following viewpoints on language design.

Features of certain languages, such as the types for variables and parameters, permit a compiler to find all type errors at compile time. Such rigidities may permit efficient compiled code, but such checks result in refusal to compile program that would indeed never produce the run time error.

Consider a routine R with parameter x. Code in the routine invokes method M on x. Upon some calls to R, x is bound to an object with no method M and the routine is smart enough to avoid the code that invokes M. A static type scheme would most likely refuse to compile the code and some other arrangements would be necessary. To be absurd it is like disallowing division because the programmer may not be smart enough to avoid dividing by zero. On the other hand this refusal to compile supports type safety with efficient compilation. The extra overhead for the programmer may be described as a burden of proof to the end of fast safe code.

Java attempts to be categorical regarding compile time errors. The language specification attempts to specify exactly which errors a compiler must report, and, accordingly, when it must close its eyes and remain silent on an error which is sure to happen. There are advantages to this view but it has greatly extended the bulk of the formal definition of Java as in the chapter on definite assignment that specifies exactly how much checking must be done to ensure that variables will always acquire a value before they are used.

Recently a C compiler refused to compile if(0) return x.m; because the structure x lacked a field m. The source was produced by a preprocessor. I could find no easy fix.