[JadeNB]

> Hence we can work around the theorem, by either turning the questions we care about into trivial questions, or by turning questions of the function into questions about the implementation.

You're quite right that my omission of 'non-trivial' makes the theorem as stated wrong; sorry!

I like your statement of the second work-around (elaborated below (https://news.ycombinator.com/item?id=11260034)), as (essentially) what type systems do, especially with the emphasis on why it must be over-conservative.

Although your statement of the first work-around is technically correct, I think that it is important to emphasise (as you clearly know, but others may not) how useless it is (on the program level): questions of this sort are necessarily about the language, not about the program.