9 ms·

(disclaimer: I'm the author of the blog post). The argument the other way is that if a mathematician sees this convention, their reaction is likely to be "that'

(disclaimer: I'm the author of the blog post). The argument the other way is that if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'", and any attempt to defend this by saying "it makes perfect sense viewed through the lens of type theory" runs the risk of the response "well I won't be doing my mathematics in type theory then". In the comments to the blog post (and in personal emails) people have suggested that instead of trying to defend the idea that 1/0=0 (which is what I was trying to do, given that I am now very much used to it) I should instead be complaining to the Lean designers to make the front end "work more like a mathematician expects". However this is difficult, because talking to mathematicians it becomes clear that they have different opinions about what "actually happens" when you put garbage in.

e79 6y ago
What would “halt and catch fire” look like for a proof assistant? If I’m trying to prove a theorem that performs division over the reals, would it then have to mechanically prove that there cannot exist any inputs that would result in division by zero? Isn’t that then itself a theorem that I’d have to explicitly define using tactics?
- thaumasiotes 6y ago
  Well, if you're doing a proof and (for example) you want to cancel x in the numerator of a fraction with x in the denominator, you then apply the constraint x ≠ 0 to every subsequent step of the proof. (You may then do a separate proof in the case that x = 0, if you want to prove something for all x including 0.)
  - zozbot234 6y ago
    That's actually needed for a real proof. One should keep in mind that y = ax is not injective if a=0, so that "cancel a variable" step you're thinking of is most likely incorrect without that side-condition.
    - thaumasiotes 6y ago
      ...yes?
garmaine 6y ago
Except that's a false dichotomy. Sqrt() could instead return Enum { Real | Complex } and the typing enforces that the surrounding math handles the appropriate cases (or proves that negative input is not allowed). Likewise for division by zero, etc.
- Tainnor 6y ago
  Sure, but imagine that every time you divide, the result may be optional. At least in a general purpose language that would clutter the code with optional handling even in cases where you know (but the compiler doesn't) that the value absolutely can't be zero. Relatedly, there is value to non-local error handling (i.e. unchecked exceptions), catching logical errors at a local level makes little sense.
  - garmaine 6y ago
    There's a couple of points to be made to that. First, we should be extending our hardware numerics to support the extended real number line, inclusive of infinity, in a way which causes a lot of these exceptions to disappear. Division by zero should result in an inf, not an exception or NaN. Second, those exceptions which can't be eliminated DO need to be handled anyway. To say "but then we'd have to handle a bunch of exceptional cases everywhere!" is exactly the point. They do need to be handled. Finally, language and compiler improvements can make handling exceptional cases easier. E.g. let numerical methods specify domain and range requirements and have these be compiler-enforced. Then the implementation is freed from handling exceptional conditions that only arise with inputs outside of its declared domain.
    - Tainnor 6y ago
      I feel you're missing the point: - Division by zero resulting in Inf could be fine in some cases, but might also lead to issue in other situations. The "calculate a slope through two separate points" is a good example: the slope through a single point is either undefined or the derivative, but it's not infinity. In any case, division by zero is sufficiently "weird" or "corner case-y" that you'd want to pay special attention to it. And if the runtime blows up in your face and tells you something is wrong, that can in many cases be better than to continue with wrong values (compile-time checks are always better, but not always feasible). - First, it's not true that all exceptions need to be handled. This heavily dependens on the use case. If you're an app developer, then the app crashing might be a better (!) alternative than e.g. corrupting data, if it happens rare enough. After all, the user can just restart the app. Even if you write a server side app, you may get away with crashing, as long as you have a supervisor or so restarting unhealthy processes/instances. I'm not saying, crashes are good behaviour, but im some cases they are better behaviour than some of the alternatives (and in any case, no code is ever crash-proof, you can always have OOM, stack overflow, etc.). This is the concept of fault tolerance: you might not know which bugs happen, but you want to be able to recover from them somehow. In fact, if I'm not mistaken, Erlang basically takes this philosophy to an extreme. - Even if you handle exceptions, you don't necessarily want to handle them locally. This is why many languages have unchecked exceptions. You're free to declutter a huge chunk of your application of error handling that would be extremely tedious, and just handle the (rare) exception at the top-level, or whatever intermediate layer best knows how to deal with it. Sometimes you just want to assert something about the state of your program that the compiler doesn't know and throwing an unchecked exception in case the condition is violated and only handling it at the topmost layer of your application is a perfectly reasonable decision.
enriquto 6y ago
> if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'" mathematician here. The expression 1/0 is not "obviously" halt and catch fire. Extended real numbers (either projectively or affinely) are a well-known thing. If you see the expression 1/0 or 1/f(x) where f(x) may take the 0 value you do not halt and catch fire; you assume that the operations are taking place in a place where they make sense. A very common usage is when f(x)=0 for a zero-measure set of x, and then 1/f(x) has dirac masses at these points (weighted by the absolute value of the derivative of f). On the other hand, I agree that "type theory" would sound like a ridiculously unnecessary abstraction to most of us.

e79 6y ago

What would “halt and catch fire” look like for a proof assistant? If I’m trying to prove a theorem that performs division over the reals, would it then have to mechanically prove that there cannot exist any inputs that would result in division by zero? Isn’t that then itself a theorem that I’d have to explicitly define using tactics?

thaumasiotes 6y ago
Well, if you're doing a proof and (for example) you want to cancel x in the numerator of a fraction with x in the denominator, you then apply the constraint x ≠ 0 to every subsequent step of the proof. (You may then do a separate proof in the case that x = 0, if you want to prove something for all x including 0.)
- zozbot234 6y ago
  That's actually needed for a real proof. One should keep in mind that y = ax is not injective if a=0, so that "cancel a variable" step you're thinking of is most likely incorrect without that side-condition.
  - thaumasiotes 6y ago
    ...yes?

garmaine 6y ago

Except that's a false dichotomy. Sqrt() could instead return Enum { Real | Complex } and the typing enforces that the surrounding math handles the appropriate cases (or proves that negative input is not allowed). Likewise for division by zero, etc.

Tainnor 6y ago
Sure, but imagine that every time you divide, the result may be optional. At least in a general purpose language that would clutter the code with optional handling even in cases where you know (but the compiler doesn't) that the value absolutely can't be zero. Relatedly, there is value to non-local error handling (i.e. unchecked exceptions), catching logical errors at a local level makes little sense.
- garmaine 6y ago
  There's a couple of points to be made to that. First, we should be extending our hardware numerics to support the extended real number line, inclusive of infinity, in a way which causes a lot of these exceptions to disappear. Division by zero should result in an inf, not an exception or NaN. Second, those exceptions which can't be eliminated DO need to be handled anyway. To say "but then we'd have to handle a bunch of exceptional cases everywhere!" is exactly the point. They do need to be handled. Finally, language and compiler improvements can make handling exceptional cases easier. E.g. let numerical methods specify domain and range requirements and have these be compiler-enforced. Then the implementation is freed from handling exceptional conditions that only arise with inputs outside of its declared domain.
  - Tainnor 6y ago
    I feel you're missing the point: - Division by zero resulting in Inf could be fine in some cases, but might also lead to issue in other situations. The "calculate a slope through two separate points" is a good example: the slope through a single point is either undefined or the derivative, but it's not infinity. In any case, division by zero is sufficiently "weird" or "corner case-y" that you'd want to pay special attention to it. And if the runtime blows up in your face and tells you something is wrong, that can in many cases be better than to continue with wrong values (compile-time checks are always better, but not always feasible). - First, it's not true that all exceptions need to be handled. This heavily dependens on the use case. If you're an app developer, then the app crashing might be a better (!) alternative than e.g. corrupting data, if it happens rare enough. After all, the user can just restart the app. Even if you write a server side app, you may get away with crashing, as long as you have a supervisor or so restarting unhealthy processes/instances. I'm not saying, crashes are good behaviour, but im some cases they are better behaviour than some of the alternatives (and in any case, no code is ever crash-proof, you can always have OOM, stack overflow, etc.). This is the concept of fault tolerance: you might not know which bugs happen, but you want to be able to recover from them somehow. In fact, if I'm not mistaken, Erlang basically takes this philosophy to an extreme. - Even if you handle exceptions, you don't necessarily want to handle them locally. This is why many languages have unchecked exceptions. You're free to declutter a huge chunk of your application of error handling that would be extremely tedious, and just handle the (rare) exception at the top-level, or whatever intermediate layer best knows how to deal with it. Sometimes you just want to assert something about the state of your program that the compiler doesn't know and throwing an unchecked exception in case the condition is violated and only handling it at the topmost layer of your application is a perfectly reasonable decision.

enriquto 6y ago

> if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'" mathematician here. The expression 1/0 is not "obviously" halt and catch fire. Extended real numbers (either projectively or affinely) are a well-known thing. If you see the expression 1/0 or 1/f(x) where f(x) may take the 0 value you do not halt and catch fire; you assume that the operations are taking place in a place where they make sense. A very common usage is when f(x)=0 for a zero-measure set of x, and then 1/f(x) has dirac masses at these points (weighted by the absolute value of the derivative of f). On the other hand, I agree that "type theory" would sound like a ridiculously unnecessary abstraction to most of us.