Pony is made for a more typical scenario where every failure case is a new, untested error path, and history shows that general developers handle errors badly. Pony makes a heroic effort to remove the error path from the language semantics entirely: every failure is explicitly annotated in the code, and has to be handled there. This is much better for the typical developer, allowing them to produce very robust code without NASA's degree of investment towards it. Giving Pony a special unwinding mode just for division by zero would be very dangerous, because this is a new path that only exists for a rarely-encountered sort of error; you cannot assume a sudden shutdown is going to do less damage.
Having Pony present the error cases inline on division by zero would certainly be safer, but there is a degree of disproportionality here: most divisions are impossible to go wrong in this way, and I suspect most of the rest are benign or would be quickly caught by the check after. Since Pony aims to compete against incumbents that are generally less safe in this regard (C++ has UB, Python has exceptions but makes it hard to handle them correctly, etc.), a compromise seems sensible.