3 ms·

The risk is not that a contract will run forever, but that it may be intractable to exhaustively predict all possible outcomes or prove much of anything about a

The risk is not that a contract will run forever, but that it may be intractable to exhaustively predict all possible outcomes or prove much of anything about a contract even given the computational time afforded to it.

gfodor 9y ago
Sure, that isn't due to the halting problem though. It's certainly trivial to show that any solidity program running on the ethereum VM will halt. What you're saying is that the current ether VM languages don't have much in the way of formal proofs to support understanding their behavior, but that is an area of active work afaik and doesn't fall out from the halting problem.
- readams 9y ago
  It actually is related to the halting problem. Rice's theorem is the directly relevant result though. Formal verification of more constrained systems is possible though.
  - deleted 9y ago
    [deleted]
- archgoon 9y ago
  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.

gfodor 9y ago

Sure, that isn't due to the halting problem though. It's certainly trivial to show that any solidity program running on the ethereum VM will halt. What you're saying is that the current ether VM languages don't have much in the way of formal proofs to support understanding their behavior, but that is an area of active work afaik and doesn't fall out from the halting problem.

readams 9y ago
It actually is related to the halting problem. Rice's theorem is the directly relevant result though. Formal verification of more constrained systems is possible though.
- deleted 9y ago
  [deleted]
archgoon 9y ago
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.