>>14
Since we don't seem to have hypercomputation, that's basically the biggest fucking understatement in /progn/.
It's more complex than you think.
For one thing, read this:
http://en.wikipedia.org/wiki/Turing_degree , as far as I understand this means that you can accidentally make a static type system that is not only undecidable, but also undecidable for a TM with a TM-halting oracle. Of course it would not be able to resolve undecidable problems in practice, but it would be more expressive at least.
The second, more intriguing option is the existence of a computability class strictly more powerful than TM and strictly less powerful than TM + TM-halting oracle (which is usually meant by hypercomputation). I don't see any immediate reasons for such thing not to exist, or maybe even be physically plausible.