4 ms·

"Philip Wadler believes that typed lambda calculus was discovered not invented" https://corecursive.com/021-gods-programming-language-with-philip-wadler/ https

• pron 7y ago
  Well, he's wrong: > We do not attach any character of uniqueness or absolute truth to any particular system of logic. The entities of formal logic are abstractions, invented because of their use in describing and systematizing facts of experience or observation, and their properties, determined in rough outline by this intended use, depend for their exact character on the arbitrary choice of the inventor. That's the American logician Alonzo Church (1903-1995) in his 1932 paper, A Set of Postulates for the Foundation of Logic, in which he expresses his disagreement with Wadler and also invents the (untyped) lambda calculus [1]. You can find this passage and many more in a 300-page anthology of (mostly) primary sources that I composed over a year ago [2], many of them describing the meticulous, intentional invention of various formalisms over the centuries, as well as aesthetic concerns which have led some to prefer one formalism over another (e.g. the invention of a logical algebra by Boole, and its later amendment into what we know as the Boolean algebra, by Jevons, Peirce and Schröder to make it more pleasing). In fact, Alan Turing's 1937 paper directly demonstrates the essence of computation and the "accident" of formalisms, which are linguistic, aesthetic, subjective formulations of a fundamental, non-linguistic idea (as Gödel said, when he called Turing's discovery a miracle, it does not just show that one formalism is equivalent to another, but uncovering the essence of all formalisms at once). Wadler is not an authority on the history of logic, and his perspective (which, unlike his actual academic work, is not based on serious scholarship), combined with his guru stance, is one of the causes for the deep confusion among functional programmers about FP and mathematics, and fosters a mystical adoration of mathematics, one of whose symptoms are nonsensical statements like "based on mathematics," rather than understanding. I wish he'd stop doing that, as I don't think it's helpful. [1]: In that paper the lambda calculus appears as a proof calculus for a logic that was later proven unsound. The calculus itself was then extracted and used in Church's more famous 1936 paper, An Unsolvable Problem of Elementary Number Theory in an almost-successful attempt to describe the essence of computation. That feat was finally achieved by Turing a few months later. [2]: https://pron.github.io/computation-logic-algebra https://pron.github.io/computation-logic-algebra