Comment by remon
2 days ago
"Controversial: Flix defines division by zero to equal zero." Wait what. Can I read up on the motivation somewhere?
2 days ago
"Controversial: Flix defines division by zero to equal zero." Wait what. Can I read up on the motivation somewhere?
The FAQ (https://flix.dev/faq/#:~:text=Dividing%20by%20zero%20yields%...) links to https://www.hillelwayne.com/post/divide-by-zero/, which is more about Pony, but links to https://xenaproject.wordpress.com/2020/07/05/division-by-zer... which properly explains that it's helpful for proof assistants to define division by zero, with particular reference to Lean. Really it's defining a division-like function (Lean calls it real.div) that disagrees with division in this one way, and then making "/" use it. It's unclear to me if this is sensible in a general purpose programming language that isn't a proof assistant.
Ah thanks for the insights and references. And yes I'm still curious why this definition of div/0==0 is needed in the context of Flix
Gotta be honest, this isn't very inspiring : "Wait, division by zero is zero, really? Yes. But focusing on this is a bit like focusing on the color of the seats in a spacecraft."