On 06/19/2014 09:06 PM, "Ola Fosheim Grøstad"
<ola.fosheim.grostad+dl...@gmail.com>" wrote:
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.
I don't think it is that significant. They are basically the same except
that the proof is typically more strongly typed and you cannot actually
execute a proof by excluded middle in the general case.
