Re:Kotlin: A Language with a Bright Future
by pron on Wednesday November 22, 2017 @05:04AM
(#15755666)
P.S.
This quote explains the crucial aesthetics component of formal systems:
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... [T]here exist, undoubtedly, more than one formal system whose use as a logic is feasible, and of these systems one may be more pleasing or more convenient than another, but it cannot be said that one is right and the other wrong.
The quote is from a 1932 paper called A Set of Postulates for the Foundation of Logic, in which Alonzo Church first introduced the formal system that would become his lambda calculus.
"Pleasing or convenient" is aesthetics, and the thing Church tried to make pleasing or convenient when he later turned his (inconsistent) logic into a universal computation calculus was how people in the 1920s and '30s thought of computation in the context of mathematics. In more modern, computer science terms, that thing was sequential, batch computation, namely something that takes a value and produces a value. I think that most programs written today are not sequential; if not concurrent or distributed, they are at least interactive, and while they may contain a great number of sequential computation bits, those bits are not the tricky, subtle or complex things about them, and therefore form the part of least concern (even if they form the majority of lines of code).
On the other hand, in the '70s and '80s, more modern formal systems were invented that incorporate cleanly, elegantly and simply all (or, most importantly, the trick) parts of computation into a mathematical framework. Part of the reason why so much emphasis is placed on lambda calculi by contemporary logicians (AKA programming language theorists) is precisely that this calculus is so well studied because it so old. But programmers aren't logicians, and so they do not require the oldest and best understood formal system, designed to optimize concerns that they may not share.
It's true that many paradigms can be embedded as DSLs in functional languages, but that's not helpful. That a language achieves its goals doesn't mean its host is equally appropriate.
This quote explains the crucial aesthetics component of formal systems:
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... [T]here exist, undoubtedly, more than one formal system whose use as a logic is feasible, and of these systems one may be more pleasing or more convenient than another, but it cannot be said that one is right and the other wrong.
The quote is from a 1932 paper called A Set of Postulates for the Foundation of Logic, in which Alonzo Church first introduced the formal system that would become his lambda calculus.
"Pleasing or convenient" is aesthetics, and the thing Church tried to make pleasing or convenient when he later turned his (inconsistent) logic into a universal computation calculus was how people in the 1920s and '30s thought of computation in the context of mathematics. In more modern, computer science terms, that thing was sequential, batch computation, namely something that takes a value and produces a value. I think that most programs written today are not sequential; if not concurrent or distributed, they are at least interactive, and while they may contain a great number of sequential computation bits, those bits are not the tricky, subtle or complex things about them, and therefore form the part of least concern (even if they form the majority of lines of code).
On the other hand, in the '70s and '80s, more modern formal systems were invented that incorporate cleanly, elegantly and simply all (or, most importantly, the trick) parts of computation into a mathematical framework. Part of the reason why so much emphasis is placed on lambda calculi by contemporary logicians (AKA programming language theorists) is precisely that this calculus is so well studied because it so old. But programmers aren't logicians, and so they do not require the oldest and best understood formal system, designed to optimize concerns that they may not share.
It's true that many paradigms can be embedded as DSLs in functional languages, but that's not helpful. That a language achieves its goals doesn't mean its host is equally appropriate.