checkedint call removal

[via Digitalmars-d]

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.