[mnarayan01]

> I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible.

Guessing you're plenty clever...just didn't think about it enough :)

Simply transform a program into one which halts on a type error rather than whatever else it might be doing. Done.

[samatman]

Consider the case of a simple type system, where any statement in the language is of either type "true" or type "false"....

[jessaustin]

This proof is missing a few steps, at least if it's meant to convince slow thinkers like myself. b^)