Hacker News Reader

Comment by pron | Hacker News Reader

> I am surprised you seek to attack them as "cults".

I don't call people who actually study and understand math as a cult. Those people don't usually make outlandish claims that "if only people applied some math magic dusts, writing correct programs would be easy," because they know the really difficult challenges (after all, it is complexity theory, a mathematical theory of sorts, that tells us that verifying programs is very, very hard). But that's not what I see in the FP community. I see mathiness, not math. I also see cultish adoration; the lambda calculus was discovered, not invented? Come on! It's not only wrong, but it's a kind of religious adoration. I call cults cult.

View on HN

I don't think you can dismiss a platonic view of mathematics as simple cultish adoration and wrong.

There's many problems with the platonic world of ideals and a long history of arguments and counter arguments, but definitely nothing is settled and most working mathematicians have an intuitive feeling of platonism and that there is a 'right' solution to be found out there.

It has nothing to do with the Platonic view of mathematics, that I don't try or wish to dismiss at all. Even if the real numbers are real and, say, complex numbers were discovered, the lambda calculus was still very much invented. The lambda calculus is a formal system, an artificial language, first described in a paper in which the author, Alonzo Church, talks about the arbitrariness and aesthetics involved in inventing a formal system, and ironically, specifically talks about the process of invention in that context: https://news.ycombinator.com/item?id=20699465

So claiming that the lambda calculus was invented is 1. factually wrong, 2. fosters a deep misunderstanding of what formal systems are, 3. encourages a mystical view of mathematics. So it is at once wrong and mystical, and so I find it cultish.

Note that when, say, discussing the use of complex analysis researchers don't usually spend time on the claim that complex numbers were discovered. But some FP luminaries do, as part of their (perhaps unintended) mission to instill awe and admiration toward their favorite programming style at the expense of understanding.

oh I don't think that's fair. the view that mathsy things are discovered not invented is hugely widespread amongst many people who know what they're talking about. I don't know what I'm talking about, and I think such matters are invented not discovered. but I do think Haskell is a great language that will drastically improve the quality of maybe even any project that doesn't need c-like efficiency. these concepts are independent.

Creating a formal system, an artificial language, is not a mathematical discovery and it has nothing to do with "math things." There are interesting "math things" one can discover about Python, but no one would take you seriously if you say Python was discovered rather than invented, and no one who knows the history of logic would take seriously any claim that the lambda calculus was discovered. The person who invented the lambda calculus said it was invented in the very paper he presented it, so no, the people who say it was discovered do not know what they're talking about, at least not on that matter.

Lambda calculus is a lot simpler than Python. It bares a striking similarity to Gentzens natural deduction rules and is essentially isomorphic to it. It is also very well studied and its properties are well known. Hence it makes an excellent basis for a programming language. The idea that Lambda calculus was discovered and not invented was recently entertained by Phil Wadler. Given his academic credentials, I think we can assume he knows what he is talking about.

Why can we assume that? Is he an expert on the history of logic? That he's an expert in an adjacent field doesn't make him at all an expert on that. If you listen to his talks and compare with the actual texts he mentions you'll see that he's wrong.

And the similarity is not "striking" at all. It's by design. It is only striking if you don't know the actual history of how these formal systems developed. A couple of years ago I composed an entire anthology on the subject: https://pron.github.io/computation-logic-algebra

Reply on news.ycombinator.com