On Thursday, 19 June 2014 at 18:25:00 UTC, Tobias Pankrath wrote:
It's not. Since the resources to verify a property are limited, too.If I need to enumerate all possible program states, there will always exists a program that can run on my box but will not be verifiable on it (since I lack the resources).
Nobody have said you should enumerate all possible states. There's a significant difference between a proof and an algorithm.
