4 ms·
The writer says as much toward the end of their article: > trying to prove that the output changes is the same as trying to prove that the program finishes wri
by acbabis 11y ago
The writer says as much toward the end of their article:
> trying to prove that the output changes is the same as trying to prove that the program finishes writing. Thus it is theoretically undecidable.
- catnaroek 11y agoThen what exactly is the point to testing? Prove it for once and for all!
- acbabis 11y agoThat's fair. I think it makes more sense to write a function you know is functional and then test for expected output. I'm not sure under what circumstances you wouldn't be sure if your code was functional.
- catnaroek 11y agoI can think of situations where a compiler couldn't figure out on its own that your code is purely functional. For example, when you do dynamic programming, you internally use mutation (memoizing previous results) to speed up the evaluation of a recursive pure function. Outside parties shouldn't be able to see anything impure going on. Lazy evaluation is a special case of this idea. But I can't think of any situation where the programmer shouldn't know beforehand whether the procedure he or she's implementing evaluates a pure function.
- AnimalMuppet 11y agoI can agree that "prove it" is preferable, in theory. But the amount of code for which we can actually prove any property we care about is much smaller than the amount of code we wish to write. An automated approach, even if not perfect, is often better than "no proof at all", and also better than "no code at all" (or "you can't have that code until I get around to proving it", which amounts to the same thing).