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 no

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.