Comment by JonChesterfield | Hacker News Reader

Comment by JonChesterfield | Hacker News Reader

Parent Full thread

JonChesterfield

Neither. I guess we'll try argument from authority. A sibling post called out pony.

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.

This is a much clearer argument to me. Theorem provers can be used to ensure certain constraints are met for all possible inputs. It doesn't matter to a theorem prover if 1/0=0, 1/0=infinity, or 1+1=3 so long as you can show the system stays within its constraints. It's not a question of math, it's about what you can prove the machine will do.

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.

Ok now we're talking: important clarifications. Neat read on the type systems. But this part is extremely important:

> 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

Thanks for an interesting read. I don't think it's a convincing argument for general purpose languages, though.

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.

Reply on news.ycombinator.com