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.
back
1 comments
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).