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.
