On Saturday, 2 August 2014 at 05:07:58 UTC, Chris Cain wrote:
Thus when you assert something is true and the compiler can't immediately disprove you, it must follow what you say.
The compiler can be much better about proving things about a program than programmers probably are, especially if subtle details of the language specification need to be taken into account, because this is mostly a mechanical thing, which computers are really good at, and humans are not. If the compiler cannot prove something, it will usually err on the safe side (let's assume an error free compiler).
I think whole program optimization is a much better strategy. With that, the compiler can actually prove what you just have to assume if you use manual assertions. Of course, it doesn't work across library boundaries, but I would see those as external interfaces, so it's probably acceptable.
