6 ms·
“You can’t do it in general” is the bathwater.
by quickthrower2 3y ago
“You can’t do it in general” is the bathwater.
- waynecochran 3y agoYeah 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 agoMore 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 agoOtherwise you’d give up having types and linters because god forbid they might prove a program will halt!