4 ms·

Proving that two programs are the same is not decidable either.

scarmig 3y ago
Proving that two real numbers are the same is not decidable either. Despite that, there are some real numbers that we can prove are equal to each other (rarely).
quickthrower2 3y ago
“You can’t do it in general” is the bathwater.
- waynecochran 3y ago
  Yeah I am not clever enough to come up with a baby worth throwing out. Restricted to lexical scope seems pretty reasonable. Maybe someday this will compile: let mut viridian = Colour(52, 161, 128); let x = &mut viridian; let y = &mut viridian; if find_counter_example_to_Reimann_Hypothesis { do something with x and y }
  - pyrale 3y ago
    More like you're arguing that there is no baby in the bath you want to throw out. Coming back to your previous comment: > This (i.e. proving a variable is never used) is impossible in general since it is equivalent to the halting problem. Many useful provers/programs don't suffer from the halting problem. Just because you're given a turing machine doesn't mean you can't use a subset of it with different properties.
    - quickthrower2 3y ago
      Otherwise you’d give up having types and linters because god forbid they might prove a program will halt!
andrewflnr 3y ago
Just to make it explicit, checking an existing proof is very decidable, given a reasonable programming language. Now getting that proof does pose some practical difficulties, but it would doubtless be built up by fairly simple proofs derived from user-supplied editing steps; a bit of a pain, but not Halting-complete.
layer8 3y ago
By that logic, one could never do a refactor and be confident it didn’t change program behavior. Luckily, a program and it’s refactored version aren’t two arbitrary, unrelated programs. You can generally prove if the transformations that convert one into the other keep the semantics unchanged. Conversely, one should only ever apply transformations for which this is true.

Proving that two real numbers are the same is not decidable either. Despite that, there are some real numbers that we can prove are equal to each other (rarely).

quickthrower2 3y ago

“You can’t do it in general” is the bathwater.

waynecochran 3y ago
Yeah I am not clever enough to come up with a baby worth throwing out. Restricted to lexical scope seems pretty reasonable. Maybe someday this will compile: let mut viridian = Colour(52, 161, 128); let x = &mut viridian; let y = &mut viridian; if find_counter_example_to_Reimann_Hypothesis { do something with x and y }
- pyrale 3y ago
  More like you're arguing that there is no baby in the bath you want to throw out. Coming back to your previous comment: > This (i.e. proving a variable is never used) is impossible in general since it is equivalent to the halting problem. Many useful provers/programs don't suffer from the halting problem. Just because you're given a turing machine doesn't mean you can't use a subset of it with different properties.
  - quickthrower2 3y ago
    Otherwise you’d give up having types and linters because god forbid they might prove a program will halt!

andrewflnr 3y ago

Just to make it explicit, checking an existing proof is very decidable, given a reasonable programming language. Now getting that proof does pose some practical difficulties, but it would doubtless be built up by fairly simple proofs derived from user-supplied editing steps; a bit of a pain, but not Halting-complete.

layer8 3y ago

By that logic, one could never do a refactor and be confident it didn’t change program behavior. Luckily, a program and it’s refactored version aren’t two arbitrary, unrelated programs. You can generally prove if the transformations that convert one into the other keep the semantics unchanged. Conversely, one should only ever apply transformations for which this is true.