John Regehr on "Use of Assertions"

[Ola Fosheim Grøstad]

On Wednesday, 5 September 2018 at 19:35:46 UTC, Meta wrote:
> I don't disagree. I think the only sane way to use asserts as 
> an optimization guide is when the program will abort if the 
> condition does not hold. That, to me, makes perfect sense, 
> since you're basically telling the compiler "This condition 
> must be true past this assertion point, because otherwise 
> program execution will not continue past this point". You're 
> ensuring that the condition specified in the assert is true by 
> definition. Not having that hard guarantee but still using 
> asserts as an optimization guide is absolutely insane, IMO.

Yes, if you have an advanced optimizer then it becomes dangerous. 
Although a prover could use asserts-with-a-hint for focusing the 
time spent on searching for proofs. It would be way too slow to 
do that for all asserts, but I guess you could single out some of 
the easier ones that are likely to impact performance. That would 
be safe.

There are some cases where "assume" makes sense, of course. For 
instance if you know that a byte-pointer will have a certain 
alignment then you can get the code gen to generate more 
efficient instructions that presume a certain alignment or if you 
can tell the compiler to "assume" that a region of memory is 
filled with zeros then maybe the optimizer can skip 
initialization when creating objects...

And it kinda make sense to be able to autogenerate tests for such 
assumptions for debugging. So it would be like an 
assert-turned-into-assume, but very rarely used...

This would be more of an expert tool for library authors and 
hardcore programmers than a general compiler-optimization.