Hey! I heard that Lean thinks 1/0 = 0. Is that true?
Yes. So do Coq and Agda and many other theorem provers.
[...]
But doesn’t that lead to confusion?
It certainly seems to lead to confusion on Twitter. But it doesn’t lead to confusion when doing mathematics in a theorem prover. Mathematicians don’t divide by 0 and hence in practice they never notice the difference between real.div and mathematical division (for which 1/0 is undefined). Indeed, if a mathematician is asking what Lean thinks 1/0 is, one might ask the mathematician why they are even asking, because as we all know, dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work.
Schlagwort: Programmieren
Leanorris.
Obvious deficiencies.
There are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies. The first method is far more difficult.
Thinking in Unix.
I’m a practitioner. I’m off to write programs with any excuse or activity.
Penguindroid.
But is Android not already Linux on mobile?
We could answer this question. However, it would not be printable on the public Interwebs, so you won’t find the answer in this post.
Ca(r)ton.
Kartonkatzen können Leben retten.
Sabrina Burtscher: Was hat die Kartonkatze mit Informatik zu tun? (Science Slam Metropol 2017)