[flagged]
Lean, coq, isabelle define integer division by zero to be zero. E.g. https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
So by case analysis either:
- I am a moron, and so are the developers of lean, coq and isabelle
- Most of the responders to this thread are failing to think for themselves
- Responders all think "number" must mean "real number"
Reading through the various responses, it's looking somewhat likely that "number" means "real number" for most people here. And divide zero on the reals is not well formed. Which is weird given it's a programming themed board and your language is far more likely to give you integers mod word size and floating point than real numbers.
By "number" I mean "the number your computer can represent", which appears to have been accidental trolling on my part. The reference to a mechanical calculator struggling was perhaps insufficient.
I believe most of us doing systems programming and building control systems use IEEE 754, so it's surprising to see a conflicting suggestion. I'd say the biggest thing is that programmers need to be aware of how 1/0 is handled, as 0, infinity, or an exception can all cause undesired results.
> The idiomatic way to do it is to allow garbage inputs like negative numbers into your square root function, and return garbage outputs. It is in the theorems where one puts the non-negativity hypotheses.
The equivalent condition here would be for everyone to include "zero-ness" checks on their numeric inputs. But that's awful, because whereas everyone agrees that nullptr is a meaningless pointer, zero is in fact a perfectly good integer/float whatever. So now you have something worse than null pointers- which have course caused us a huge amount of pain ever since being inflicted on the world
So x / 0 = 0 is still a terrible, terrible, idea. But introduce something like the floating-point equivalent of NaN, and say x / 0 = NaN, and now your outputs will at least be obviously wrong, instead of just silently wrong
In Lean, the zero check is still there, just not in the arithmetic operator itself but in the various division related theorems you need to use in order to do anything useful with the division. But in C/Java/Python/whatever, there are no such guardrails, so 0 or 37 or whatever bogus value is returned from a division by zero will propagate to the rest of the program and cause subtler and harder-to-find bugs.