Item — HN Reader

The issue is that you can’t generally determine whether a statement is “buggy” in that way, because under the assumption that you could, you can construct another paradox.

Regarding programming languages, it means that for any programming language with a non-trivial type system, either there will be correctly typed programs that however fails the type checker, or there will be ill-typed programs that cause the type checker to run into an infinite loop.

1 comments

> The issue is that you can’t generally determine whether a statement is “buggy” in that way, because under the assumption that you could, you can construct another paradox.

You can't always determine if a program is going to finish either because that would require infinite number of operations is some cases (so it would be a program that never finishes as well). So the analogy still stands.

The reason you can't always determine if a program is going to finish is due to the undecidability of the halting problem, which is equivalent to Gödel’s first incompleteness theorem (you can prove one from the other). But that's not merely because programs might run into an infinite loop or recursion. It's deeper than that.