We're talking about definitions, so you may continue to refer to 'functions' however you like, but from a functional programming perspective, I'm going to posit

We're talking about definitions, so you may continue to refer to 'functions' however you like, but from a functional programming perspective, I'm going to posit that it is useful to distinguish between functions and 'impure' functions. :) I think your position is that because there is an escape hatch in languages like Haskell, that negates the usefulness of equational reasoning. I'll argue this isn't true, in the same way it's useful to pretend ⊥ doesn't exist and that we don't bork our unbound recurison or whatnot. Once we do that, we now can reason about our functions as if they exist as arrows in a cartesian closed category (of types). This is incredibly useful. We just have to restrict ourselves to a subset of the language. We still get that same benefit even if part of our program call impure functions. This is the reason we want to model as many side effects as we can in the types (an IO monad or Task in Scala). I saw your twitter convo, I don't know what you mean by this: >"If we define functions as pure, then functional programming doesn't exist outside of extreme specialist applications." All kinds of Haskell applications are built with side effects. Are you under the impression UnsafePerformIO is the only way to interact with the world in Haskell?