Since I'm being downvoted, let me clarify for the “hackers”.
By “pure”, I mean lacking unaccounted side effects (including crashing and non-termination).
I take a rather strong view, as you can tell, of what it means to “support” pure functional programming. That is, I think it is insufficient to show that your code lacks appeals to falsehood and rampant non-termination. Because your code is linked with other code from other sources, it must be shown that appeals to falsehood and rampant non-termination are in fact _impossible_.
(By “rampant non-termination” and “appeals to falsehood”, I mean the use of circular reasoning. This is distinct from structural recursion and coinduction, which can be used to do REPLs and servers.)
So yes, Virginia, there is indeed a Pure Functional Programming. But you can't do it in Haskell.
> So yes, Virginia, there is indeed a Pure Functional Programming. But you can't do it in Haskell.
True, but if you want to get as close to purity as possible whilst actually writing usable software Haskell is the answer. I'd love it if Agda was actually a fully fledged programming language, but currently it is not.