Every technical text needs to be read using some common sense. Once you give this away, you can justify everything.
back
1 comments
Sure, but the common sense I (and I think I can safely say the compiler writers) are applying is "when the spec says 'the program might do anything', then there is no meaningful difference to the user whether or not we guarantee that everything up to that point was executed correctly". Who cares whether we transferred money from account A to account B when the program is then going to transfer 5 times as much from account B to account A and gift our competitor half of our money while it's at it.
I'm not sure if I agree with your interpretation of the spec, but even if that's the technically correct interpretation, arguing that things went wrong because the compiler miscompiled the program and that it didn't do the things it was supposed to before it was allowed to do literally anything... just isn't an interesting argument. Things went wrong because your program was wrong.
The spec says there are no restriction on the behavior. But now going on saying that when there are no restriction on behavior the term "behavior" now includes impossible things like time travel or magic instead of something any actual machine could possible do, this seems far fetched to me.
Regarding the second point. Sure the program went wrong because it was wrong. But the damage it can do when something went wrong when this can affect previous behavior is much higher. Being able to prove partial correctness of a program is a useful feature (e.g. when a transaction completed correctly you can be sure that and error in the logging function afterwards does not undo this).