In fairness, its pretty hard to explain what MIP*=RE to a layman (or even to tech people if the comments on hn are any indication). At least the intro kind of evokes the feeling of what the problem is about, even if its pretty corny.
Just imagine, you're about to get a proof that some program halts and just before you verify it you are eaten by a grue.
Just imagine, you're about to get a proof that some program halts and just before you verify it you are eaten by a grue.