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).