Well, it's not Harel all by himself who decides that a problem is unsolvable. Some problems of computer science are known as "undecidable", meaning that no algorithm --- no matter how sophisticated or ran on your latest Beowulf cluster of 1000 workstations --- could EVER solve them. And you can establish this impossibility with a formal mathematical proof (generally proceeds as follows: if an algorithm could be found to solve the problem, then it leads to a contradiction). The best-known such problem is the so-called "Halting Problem", i.e. does there exist a computer program that can tell whether another computer program will terminate in a finite number of steps given a certain input? Does not exist; you can prove the inexistence.

Other problems are "intractable", meaning that even though a solution exists in theory, it would take so long to compute that we will all be deeply buried in our graves (and the Sun will have blown up) before your all-mighty Beowulf cluster comes up with the solution. (There are approximation techniques for many intractable problems, that are able to find "good enough" solutions, and yes this is a very active area of research in computer science right now).

So Harel "does not decide by himself". And if you want to waste money solving an undecidable problem, it's your money, not mine... :-)