While defining x/0 = 0 is sound, it has tradeoffs, as OP acknowledges. In "Papers with computer-checked proofs" (2024), D. J. Bernstien wrote:
> There is a claim ... that “dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work”, but in fact a mathematician is permitted to deduce b ≠ 0 from c = a/b, since a/b is undefined for b = 0. Redefining the notation to allow b = 0 breaks this. Unless it occurs to the author to state a conclusion c = a/b and a conclusion b ≠ 0, the proof assistant won’t check that b ≠ 0, whereas the reader will think that this has been checked.
I suspect that D.J. Bernstein's preferred apples are of the silicon variety, but I could be mistaken. He is from New York, one of the early states where Honeycrisps were grown, but Long Island, which doesn't have much agriculture.
> There is a claim ... that “dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work”, but in fact a mathematician is permitted to deduce b ≠ 0 from c = a/b, since a/b is undefined for b = 0. Redefining the notation to allow b = 0 breaks this. Unless it occurs to the author to state a conclusion c = a/b and a conclusion b ≠ 0, the proof assistant won’t check that b ≠ 0, whereas the reader will think that this has been checked.
https://cr.yp.to/papers/pwccp-20240727.pdf