Consider the following program (in pseudopython, not solidity) function transfer_on_counterexample(int n): # assume n is a counterexample until proven o

Consider the following program (in pseudopython, not solidity) function transfer_on_counterexample(int n): # assume n is a counterexample until proven otherwise goldbach_counterexample = true # run through all numbers less than n for prime1 range(n): if is_not_prime(prime1): continue # do it again for another one for prime2 in range(n): if is_not_prime(prime2): continue # check if conjecture is satisfied if prime1 + prime2 == n: # this number does not refute the goldbach conjecture goldbach_counterexample = false return # didn't find p1+p2? goldbach's conjecture is false. # provide a finder's fee if goldbach_counterexample == true: transfer_ethereum() The above program is guaranteed to halt after about O(n^2 * sqrt(n)) (depending on how great the is_not_prime function is). However, it is unknown if there is any input that causes `transfer_ethereum` to be executed. So if I find a counterexample, I can compute how much gas I need to pay to win my finder's fee. So sure, it runs in finite time for a given input, but you have to guarantee it won't ever execute the transfer_ethereum function for all inputs if you want to ensure you never pay out. And that, in general, for a general program (even if guaranteed to halt) is equivalent to the halting problem. Now, I believe that solidity has an upperbound on the size of it's inputs, so the parameter space is bounded, and we return to your original argument that it is a large, but exhaustible, search space.