I agree in general and also take issue with the "we can never prove interesting things about our programs" statements that are sometimes uttered, but it is surp

I agree in general and also take issue with the "we can never prove interesting things about our programs" statements that are sometimes uttered, but it is surprisingly easy to write certain programs that nobody to this date knows whether they terminate, such as: "find the least even number > 2 that cannot be written as the sum of two primes". :)