On: Why does a Turing-complete type system make type c...

[paulddraper]

Exactly.

It's like giving up on math proofs just because Godel says not all stuff can be proved or disproved.

[johncolanduoni → paulddraper]

In fact literally the same problem! Seeing the connection explained[1] was probably the most enlightening thing I've ever seen for both results.

[1]: http://www.scottaaronson.com/blog/?p=710