You are correct that the requirements are different, but not exactly for the reasons you mention. Users of those languages use them to prove theorems, and the theorems you get are correct with respect to the arithmetical theory used. Programmers may want some error condition when dividing by zero, because that's what they believe their users expect (say, the program drives some actuator, and bad things may happen if division by zero is not detected). So yeah, the justification for this behavior needs to be different.