1/0 = 0

I very strongly object to this convention, as both a programmer and a mathematician.

A basic theorem is that for any field we must have that a/b = c/d if, and only if, ad = bc. See theorem 2 in this classic text here for a proof[1]

So if 1/0 = 0, then we also have 1/0 = 0/1, which implies 1 x 1 = 0 x 0 which is a contradiction. But then we also have 1/0 = 0/x for any x, hence we also have shown x=0 for any x, which is an infinite number of contradictions. Is this a problem which is addressed in the post that I missed?

By the way, I have spent more time than it's polite to discuss in public studying the topic of dividing by zero, and also what 0/0 means. If you are also interested in this topic, the best youtube video is by Mathologer and I highly recommend it to everyone. See here [2]

[1] https://books.google.com/books?id=3ApEDwAAQBAJ&lpg=PP1&pg=PA...

[2] https://www.youtube.com/watch?v=oc0M1o8tuPo

You have a point, but I think this is a difference in the target markets. NASA can afford to have a thoroughly-tested, redundant, quickly-accessible failure path that restarts and reinitializes the process, and their processes are so thoroughly tested that they can expect their production instances not to have any software failures.

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.

In the mathematical sense, a Field is a Commutative Ring with the added constraint that the multiplicative operation has inverses for every non-zero element.

Floating point doesn't even form a Ring, because the operation is not associative[0]. Coq, for instance, defines the operation for QArith, which are the rational numbers. The representation is a pair (Z, positive), where Z is an integer and positive is a positive number (i.e., 1,2,...). QArith does form a field in the usual sense.

Integers are not a Field (unless you pick Z/p for some prime p), and machine words, signed or unsigned are even less of a mathematical object with the usual operations. So you can do almost anything you want to them from a programming perspective, including 1/0 = 0.

As Hillel writes, what to do will make sense in some settings, but not in others. You may want MAX_INT in some situations, and 0 in others. And this requires a check, partiality or not. Rejection of the case x/0 has more to do with the notion that it is usually a corner case where you want the programmer to think about what the result should be.

[0] The reason is that any addition can incur information loss, and the further away from 0 you are, the more information is lost. Thus, the order in which you add values matter.

I'm curious what you mean by this: there is nothing "privileged" about the system of arithmetic that we usually use and this alternate definition.

The math that we all learn up through highschool is a system with a carefully chosen set of axioms that happen to be useful in most cases and has become the default system, but there isn't some intrinsic property of it that makes it "math" and alternate consistent set of axioms "not math".

You can check for 0 and throw in those cases, and then propagate the error path appropriately. And as they've already said in this thread, they will be providing a checked arithmetic in the standard library to do that for you.