On Tuesday, 29 July 2014 at 10:40:33 UTC, John Colvin wrote:
In a correct program (a necessary but not sufficient condition
for which is to not violate it's asserts) it is the same.
Define a correct program.
This is a correct program:
S = full specification ( say in prolog or haskell )
P = implementation in an imperative language
A = valid input
TheoremProver( S(x) == P(x) for all x in A )
Yes, in that case you can take any theorems derived from S
applied to P and use them for optimization.
In all other cases, injecting theorems more or less randomly into
P and then testing them for a small subset of A will never lead
to correct theorems pertaining to P. Thus they cannot be used for
optimizing P either.
