Nock made me suspect Mencius is a Kabbalist. This metal and wood business confirms it.
Hoon is still far and away the most WTF part of Urbit from my perspective. Nock: brilliant. Urbit proper: obviously the right thing. Hoon: line noise or poetry? I remain totally undecided.
Eagerly awaiting comprehensive documentation of the digraphs.
> So if we had to read the above decrement, omitting the spaces (which only a real purist would pronounce), we’d say: “luslus dec sigfas cen dec bartis a tis pat sigbar soq dec soq ketcab pat wutgal tis pel zero a per tislus b tis pat barhep wutcol tis pel a lus pel b per per b buc pel b lus pel b per per.”
Kabbalist? This sounds more Holy Roller to me.
I plan to spend at least some of the upcoming weekend with Urbit. It should be interesting, to say the least.
My take on hoon is to use[2] the alphabetic names of the line noise operators to create words and use them to make a non-symbolic (if you take alphanumeric characters as non-symbolic) functional, executable conlang[3].
To me it's what Liebniz was looking for[1], but with funny looking words that make no sense to the uninitiated, which use the 'linguistic nodules' that cgyarvin is hoping to utilize, without the symbolic name decoding that using line noise requires (if you use the names in [2] rather than the line noise symbols).
I personally think hoon looks like absolute brilliance, but I can't say yet that I've had the pleasure to write anything in it, which is the best thing to take that shiny feeling away by actually trying to use it.
ace space gal < per )
bar | gar > sel [
bas \ hax # sem ;
buc $ hep - ser ]
cab _ kel { sig ~
cen % ker } soq '
col : ket ^ tar *
com , lus + tec `
doq " pam & tis =
dot . pat @ wut ?
fas / pel ( zap !
The numerous minor nitpicks I have with this scheme are a big part of what keeps me coming back to Urbit. The basic idea is so right-on that I can't help focusing on things like this: given that 2 billion people conflate "1" and "r", how on Urth did he settle on using those as primary distinguishments for every. single. brace. pair. O right, left and right.
Similarly, every c in that scheme makes me kringe. Unless those are "chab", "chen", "chol", "chom", "butch" etc. Which, affricates, meh.
This is of course the complement of damning with faint praise.
(_Gonadic combinators_? Yes - using our gonad rune,
semsig or ;~. If you are a sophisticated professor type
and understand monads, gonads may seem real familiar to
you. Out here in Urbit world we are just dumb country
peasants and all we got is gonads.
This is the South Park of system design, or at least it makes me laugh just as much. These guys are great although the software is still a bit fragile.
Ok, I just clicked on the link and what I saw there just didn't make any sense to me :-) Still doesn't now, but after reading the comments, I returned to the site and studied it more carefully. Maybe the link should point to chapter 0, not chapter 5, to have any idea about what this is about ... After reading chapter 0 now, I can understand the goal of urbit, and I think it is a great one! But note that you can work on exactly the same goal without leaving PL theory and theorem proving entirely behind you. Check out http://proofpeer.net to see how this might be possible.
That's a truly amazing effort to take on the OS problem from a theorem-proving standpoint. I of course would try to attack the same problem on a theory-indifferent substrate. But... +1 for an exciting vision of math uber alles.
Your desktop isn't wood, your folders aren't manila, and your windows aren't glass. Why balk at a submarine? It's made of the usual combination of bits and vivid metaphor.
Hoon is a very stupid little higher-order type-inference engine that does not use Hindley-Milner, category theory, etc. Higher-order functional programming is so cool it should be accessible to the majority of human beings who unfortunately happen to be bad at math. Also, layering a type system on top of an untyped data model has various practical benefits - eg, your types can be used as validators for untrusted data you got over the network.
You appear to be saying, among other things, that a noun is of a particular type if it may be passed through a function that parses and validates that, yes, those bits may be treated in that fashion.
Is that accurate? There's clearly more to it, as there's at least one conceptual leap between that notion and any kind of inference.
The type, as a set of nouns, is the range (excuse me, "codomain") of a function.
So, if we have another function and we call it with a noun of that type, we know the range of the input, we know the code in the function, we can infer the range of the output. It's not terribly rocket scientific.
This explanation falls apart for me because the third time you use the word "function", it can refer to either of the two referents you already introduced.
I think you're saying a type is the range of inputs to function1 which succeed by not crashing; given function2 and a noun in the type, we may use function1 to infer the range of values which function2 must accept? Maybe?
Range == set of outputs which the function can produce.
In any language, a type defines a set of values and some semantics for manipulating those values. It so happens that our way of defining common sets is to build a function whose range is some useful set.
Actually any gene (ie, expression) has a product range. It doesn't even need to be a function. So the range of the constant
[%foo %bar]
whatever the subject is, is always [%foo %bar], ie, the pair [7.303.014 7.496.034].
Outputs indeed. I forgot your country willingness to 'normalize' input. I suppose a bull can be a steer if you're willing to cut the balls off on the way into the pen.
An automatic castrator is an excellent safety device for your steer pen.
Generally we don't actually use these functions unless we're normalizing foreign data. Then, we do. Because anyone on the Internets can send a bull into your steer pen...
This might be an interesting project if not for the constant misguided crusading against a PL theory straw man. It's a sort of anti-intellectualism I find particularly galling, but it seems lamentably common in some nooks of the programming world.
No, I am annoyed about any situations where people criticize something for being "academic" or decry people as living in an "ivory tower". This sentiment takes many forms and is certainly not limited to programming languages!
This sentiment takes many forms indeed. Think about your stereotypes of a vanished upper class, any upper class - for instance, the pre-revolutionary French nobility.
Obviously you never met any of these people, but you will find many negative stereotypes coming to mind. Are many of them true? Perhaps they are. Was the old Versailles full of charming, brilliant, talented, wonderful people? It most certainly was.
You might also have some stereotypes of PHP programmers. Perhaps they're true as well. No set of human beings is without patterns of fault. However, the PHP programmer is a peasant and cheerfully accepts the daily rain of mockery that falls on his head. He knows he is not above being laughed at, indeed he knows he is laughable, as all human beings are in some way laughable.
The distinctive feature of a privileged class, always and everywhere, is that it can't accept being mocked. Unfortunately this always increases the temptation to mock it, which I agree is a low and unproductive pastime. But anything to make type inference seem fun...
You are absolutely right in general, but the problem with "academic" PLs is not their origin, but their current environment. Programming languages, like natural languages, may be classified by their expressiveness, but their success is measured only by their (continued) adoption.
Some PLs, are therefore academic in the same sense that Esperanto is academic, and are rightly criticized for that. They may be "perfect languages", but the fact they are not widely adopted is conclusive proof that they're a failure, at least in some respects. Sometimes this failure could be mere marketing; usually it's much more than that.
They are only a failure if adoption was a goal. I am being serious here. It takes significant time and money to get language adoption. Every major language, C++, Java, C#, Python has had significant financial and resource backing.
Often the financial backing is very conservative. It does not like to take risks. So they go with what is familiar.
Second, I can't think of a single academic I know that set out to create "the perfect language". Often one is created to explore an idea. That does not mean the language isn't incredibly valuable for the lessons it provides - but it likely was never meant to hit mass adoption.
For the record, not that it matters, Sergey Brin was born in 1973 and started a CS PhD at Stanford, specializing in OS, in 1993. I was born in 1973 and started a CS PhD at Berkeley, specializing in OS, in 1992. Alas, neither of us finished.
Intellectuals are no different from anyone else - they live in the same reality and must be judged by their results. I don't think anyone would disagree that PL theory, as a body of work, has produced a set of languages whose penetration in the real world is oddly small both given (a) the investment in these technologies, and (b) the many real advantages of typed higher-order programming.
As a general pattern, usually when I see this outcome explained, it takes the form of blaming the user. We wouldn't let anyone else get away with this excuse, so why should intellectuals be treated as a privileged class?
To be anti-intellectual is to judge intellectuals more harshly than they deserve. To be pro-intellectual, also a cognitive bias, is to judge them more leniently than they deserve. In a world whose bias is generally pro-intellectual, it's easy for a neutral assessment to seem relatively anti-intellectual, but perhaps what you are perceiving is not an exceptional bias but the absence of a systemic bias which you've grown used to.
Yes, your background isn't relevant--and Brin's even less so--but it does make for some nice anchoring.
PL theory, as a "body of work" has produced a wide range of languages ranging from Agda to Scala to Java. Some of these have actually seen use! Everything from classical music to Justin Beiber. TAPL, for example, is certainly not limited to the less popular languages: it talks about the foundation for Java-style types as well. Some of the same people working on ML and Haskell are also behind designs of Java and C#.
The point of a language like Haskell is to be expressive and useful, not to appeal to a large base population. Popularity and industry uptake are not the only measures of success. (This is, coincidentally, one of the things I don't like much about Berkeley's graduate program, or at least the systems lab I spent a bit of time in: they did seem to think industry uptake to be the only metric that mattered.)
Beyond languages, PL theory serves the role of all theory: it's the foundation upon which everything else is built. Things like the JVM memory model are based on the theory themselves and designed with tools stemming directly from that theory. Sure, the average programmer on the street is never going to use a theorem prover, but they will use the JVM where the memory model has been verified with one.
All this reminds of nothing more than the usual arguments that Linux is a complete failure because nobody uses it on the desktop. But I think that argument is not true even if you limit yourself to "Linux on the desktop is a failure": sure, not many people use Linux on the desktop, but the ones who do find it very useful and are exceptionally productive. Same principle applies to PL theory and functional programming languages.
There are many different ways to have an effect in the world, and the most obvious and direct one is not necessarily best. Even if it feels best.
s/the foundation upon which everything else is built/a foundation on which everything else can be built. If you'll accept this change, we don't disagree at all.
(Also, it is a serious overstatement to attribute Java and C# to PL theorists. Gilad Bracha is not James Gosling. PL theorists have contributed to some extensions to these languages. Typically, the extensions that confuse people and make them feel stupid.)
The difference between the foundation and a foundation is enormous, because (with your very large expensive foundation) you are asking programmers either to program without knowing the foundations of their work, or to learn a large and challenging body of mathematics.
And you know, higher-order typed programming is good enough that it's almost worth it. For most potential customers, however, learning PL theory does not seem to be worth it. Nor are they comfortable in programming in Haskell, a very powerful and complex environment, without understanding it.
It's this "the customer is just wrong" attitude that makes some of us sense an area ripe for disruption. Pride goeth before a fall.
It does. And the best I can say is that I'm genuinely interested in the results of my experiment.
It would certainly be an interesting practical experiment to try to adapt a conventional syntax to the same semantics, or even to discard Hoon and create a more conventional language targeting Nock (which Urbit would have no trouble running).
PL research just hasn't had much affect at all on mainstream programming.
It's too bad. The PL world has a lot of good ideas. It's unfortunate they try to make them totally inaccessible.
Worse still that industry has no interest in raiding the PL world. A lot of the languages that have been designed are perfectly usable by mere mortals and a real step up from languages coming out of industry.
Compare OCaml and Java in 1996. OCaml (then Caml Special Light) was clearly the better language. Why didn't anyone get to use it?
The ugly reality is that because of the actual mistakes the PL world (or even "academia" at large) makes, anything smelling of that world often is dismissed without a second glance. Even when it has genuine merit.
Tikhonj is right about this kind of "anti-intellectualism." But pro-intellectualism is a bias as well.
> I don't think anyone would disagree that PL theory, as a body of work, has produced a set of languages whose penetration in the real world is oddly small both given (a) the investment in these technologies, and (b) the many real advantages of typed higher-order programming.
I'm a PL theorist, and I disagree.
Who cares about your opinion on PL theory, its practitioners, and its textbooks? Is internalizing your hate for TAPL necessary for understanding the semantics of Urbit and related technologies? Why don't you just state succinctly what your ideas are and let them stand on their own merits.
That being said, I have no idea what your ideas are. Your website is unintelligible. Ironically, one of the things PL theory provides is a common vocabulary amongst practioners, which helps us communicate. I shouldn't have to learn a new alphabet (or in your parlance, a set of runes?) to figure out what new ideas you bring to the table. That kind of stuff is just not interesting to me. It's like if you 'rejected' English and wrote the rest of your work in Esperanto.
Am I not entitled to an opinion? You certainly are. You could tell me _why_ you disagree. And I would listen.
We may mean different things by "practitioners." I mean programmers. Unfortunately, your vocabulary is not common to programmers and shows no signs of becoming so.
Mine isn't either. But at least I've only been trying for a week. I know it seems strange to introduce new designs in the 21st century - most people assume, rightly of course, that everything worthwhile got figured out in the 20th.
> Am I not entitled to an opinion? ...You could tell me _why_ you disagree.
Why I disagree with your disparaging remarks aimed at PL theorists is irrelevant.
The Urbit documentation should say what Urbit is, why it is important, and how to use it. Your disparaging remarks do not help to answer these questions. In fact, they do the opposite by antagonizing many readers and unfortunately giving you the appearance of a crank. Therefore, you should remove the remarks.
Knocking down PL theory does not boost Urbit up.
> We may mean different things by "practitioners." I mean programmers. Unfortunately, your vocabulary is not common to programmers and shows no signs of becoming so.
This is flamebait.
> I know it seems strange to introduce new designs in the 21st century - most people assume, rightly of course, that everything worthwhile got figured out in the 20th.
This is a strawman, and a particularly odd thing to say to someone who is also interested in advancing the state of the art.
We have an asymmetry of discourse here, because you want me to take your disparaging remarks seriously. You also seem not at all concerned about your own appearance.
Yes, there is a purpose to the disparaging remarks. The purpose is to make this asymmetry apparent.
Academia in the late 20th century is something of a footnote to the great achievements of the 19th and early 20th. In this golden age of science, peer disparagement was more or less universal. It is only in the second half of the 20th, the golden age of grants as it were, that genuinely criticizing your peers becomes a faux pas, and team-building becomes the essential skill for a practicing scientist.
But wait, I'm not your peer at all. I guess I forgot that...
I find the whole hubris of this article kind of alarming, I'm not sure if the author is doing this out of some form of satire or whether he/she actually think that the "disciple of PL theory is just full of misguided imbeciles who use formal words I don't like".
The attacks on TAPL too are seemingly weird, because arguably it's one of most thudingly concrete and down to earth books on types ever written. The whole book is about applications to real world problems and reveling in the fact that one haven't read it seems very asinine.
Obviously if you have a door that needs to stay open, a thudingly concrete... never mind.
All I would say is, s/types/PL theory. Let's take your statement as true and stipulate that TAPL is in the top 1% of down-to-earthness of books on PL theory. Is it in the top 1% of down-to-earthness books on, say, Java? If not, what does this tell us about PL theory? You have read TAPL, right?
PL theory is a beautiful system and I've never said otherwise. TAPL is also very good at keeping doors open. But so are many things. PL theory is not the theory of programming, any more than TAPL is the doorstop. It is a theory of programming and a doorstop.
> Is it in the top 1% of down-to-earthness books on, say, Java? If not, what does this tell us about PL theory?
Yes I have read TAPL, it's sitting on my desk right now. I'm not even sure what you're trying so say, the fact that a book on type system design doesn't have advice on Java* seems perfectly natural to me. A book on goat husbandry doesn't have advice on Rails development. What are you trying to say?
> PL theory is not the theory of programming, any more than TAPL is the doorstop.
This is the strawmen that you're arguing against that seems bizarre to many people. PL theory is not so much about the lambda calculus and Hindley-Milner as it is about applying rigor and discipline to the study of programming languages. And yes, sometimes that involves learning the mathematical formalism.
* Chapter 19 in TAPL actually does have an implementation of Java's type system.
Right, there you are with the definite article again.
What you're asserting is that without this system of rigor and discipline, there can be no other rigorous and disciplined way of defining programming languages. For one thing, this flies in the face of everything we know about the philosophy of mathematics.
I think my way of defining programming languages is pretty rigorous and disciplined. I'll continue to think that until you or anyone can identify some sloppy ambiguities. I note also that my foundation fits on a T-shirt and yours needs a math textbook...
This is exactly the point, you may think your system is rigorous and disciplined but how do you convey that to other people with them having the same degree of certainty that you feel your system has. The answer to that is the proofs and formalization, and that is the essence of what rigor in programming language design is about.
I think you missed the point of the (poorly phrased) question. I think the intended question was "would the down-to-earthness score of TAPL fall in the top 1% of the down-to-earthness scores of Java books?"
I actually find a lot of arguments he presents compelling. However the general thrust seems to be that programming language should be accessible.
Hoon seems to fail that test.
I've yet to see how this is better than vanilla ML. I don't see that because Hoon doesn't use standard syntax or terminology. I can't just read some code and a language overview to decide if this is worth (a lot of) my time.
I think ML has a fairly steep start-up cost but is definitely understandable by regular people and has real productivity benefits.
Hoon is sufficiently obfuscated that it has an incredibly high barrier to even evaluate as a language. I don't think you need to have tons of unintelligible typing rules to make things familiar. By avoiding standard syntax and terminology, it puts an enormous burden on the potential user.
I'd like to address this obliquely with a question to urbit:
Is it always the case that the vowels may be compressed away without loss of meaning? It seems to work some/most of the time, but there is a least a %wet and %wut... I think?
Though this be method, yet there is madness to it.
Some UI burdens seem high, some are high. An interesting class of UI problem is the set of things that intuitively look difficult, but actually aren't.
Human brains are incredibly good at raw memorization of associations. Hoon has about 100 digraphs, and their internal structure isn't random. How hard is to learn 100 characters of Chinese? Perhaps easier than you think.
Nor are there no payoffs. For instance, most languages are very bad at defining large, mostly static hierarchical trees, so when it comes time to write code that generates, say, an HTML page, you reach for a special "template language" DSL. That's not a problem we have in Hoon. Also, most functional languages have a very annoying tendency to crawl off the right side of your screen and disappear, because indentation depth matches functional depth. That's also not a problem we have in Hoon.
By the way, what's with all the hate on Ben Pierce?
Take his Software Foundations book. It opened up Coq in a very practical way. No crazy typing rules or category theory. Just straight programming and simple proofs. That's a world where previously the few who entered were sucked down a rabbit hole of theory, never to return again.
I don't think so, but I wouldn't know enough to tell you. I can tell you that I am not very interested in 20th-century formal logic, at least as a way of defining programming, but you knew that. I think it seems like a logical equivalent that my approach is not very interesting from the standpoint of 20th-century formal logic.
I think I get it now. Sort of like a sequent calculus without the logic backtracking. Instead of proving anything Hoon just defaults it to something. Or crashes. :)
A language that has "cube", "face", "stem", "bulb", "coil", "foot", "battery", "gene", "gold", "iron", "ash", and "yew"...
It's not that other languages don't make up arbitrary terms as well, but it's hard to understand why a language that claims to be simple and "moronic" does it so enthusiastically, with the result that anyone trying to learn it has to first memorize a large number of terms.
Basically, I'd say, ordinary human beings are much better at memorizing words and symbols than most smart people think - and much worse at understanding highly abstract concepts.
Think of the number of things you need to memorize to be an auto mechanic. Yet there are a large, large number of people who are capable of becoming auto mechanics, but not capable of becoming Haskell programmers.
Shouldn't we compare the abilities of people vs. computers? Computers can store a lot in their memory, but it's pretty hard to make them prove theorems, whereas humans are pretty bad at memorizing anything and pretty good at abstraction.
...and since a programming language should be primarily designed for humans (or, as I actually see it, a programming language should be an interface between the human mind and the computer) and at the same time be executable by computers, choosing more memorization and less abstract concepts seems like a bad idea ...most smart people's minds find juggling abstract concepts easier and more enjoyable than memorizing rules (and when working memory is not enough to hold all the abstract concepts we're juggling, we use anything from pen and paper to other more advanced devices - just ask any mathematician), and those that don't are also those that "just don't get (or like) software", so they shouldn't be programming anyway.
I agree with your goals but not with your observations. Perhaps I'm biased by the fact that I have small children. I am regularly amazed by their ability to memorize words, numbers, symbols, etc, combined with complete incompetence at abstract concepts. Grownups are different, of course, but it's still natural that most of what I know about learning comes from my own kids.
I'm disappointed to see the depressingly common male-genetalia-centric humor in "Gonadic" combinators. I find myself agreeing with much of the forward-thinking, throw-the-past-away design of Hoon/Nock, but it's jarring to find this kind of asinine brogrammer mentality mixed in with it. Yet another sling and/or arrow of discomfort for the half of the human population that already has to put up with too much of this shit.
[EDIT] As a reply points out, Gonad is gender neutral. I still think that this humor is distasteful.
First of all, I didn't read linked article. Which is wrong of course. As usual, I'm basing on comments in this thread.
So you want to do type system without PL theory of modern age. Awesome! Seriously, interesting experiment.
Unless you already have read TaPL in which case I fear you would antagonise ideas described there.
However, there is a non-merit, non-technical problem: dismissing PL theorists is sounds like dismissing PL theory (wrong implication, but that is how humans are I believe).
And this will put you into JS/PHP/whatever-back-to-the-trees basket and your ideas will be dismissed just because of this wrong association.
Which means, that you will distorted results of your experiment.
How do you plan to alleviate that? Or I'm wrong somewhere and it is non issue?
72 comments
[ 2.8 ms ] story [ 133 ms ] threadHoon is still far and away the most WTF part of Urbit from my perspective. Nock: brilliant. Urbit proper: obviously the right thing. Hoon: line noise or poetry? I remain totally undecided.
Eagerly awaiting comprehensive documentation of the digraphs.
> So if we had to read the above decrement, omitting the spaces (which only a real purist would pronounce), we’d say: “luslus dec sigfas cen dec bartis a tis pat sigbar soq dec soq ketcab pat wutgal tis pel zero a per tislus b tis pat barhep wutcol tis pel a lus pel b per per b buc pel b lus pel b per per.”
Kabbalist? This sounds more Holy Roller to me.
I plan to spend at least some of the upcoming weekend with Urbit. It should be interesting, to say the least.
To me it's what Liebniz was looking for[1], but with funny looking words that make no sense to the uninitiated, which use the 'linguistic nodules' that cgyarvin is hoping to utilize, without the symbolic name decoding that using line noise requires (if you use the names in [2] rather than the line noise symbols).
I personally think hoon looks like absolute brilliance, but I can't say yet that I've had the pleasure to write anything in it, which is the best thing to take that shiny feeling away by actually trying to use it.
But as art, I think it's perfect.
[1] http://sunsite.utk.edu/math_archives/.http/hypermail/histori...
[2] As follows from http://www.urbit.org/2013/08/22/Chapter-4-syntax.html:
[3] https://en.wikipedia.org/wiki/Constructed_languageSimilarly, every c in that scheme makes me kringe. Unless those are "chab", "chen", "chol", "chom", "butch" etc. Which, affricates, meh.
This is of course the complement of damning with faint praise.
Previous HN discussion: https://news.ycombinator.com/item?id=6438320
This is a perfectly serious type system that infers perfectly serious types all day long. It is moronic, though.
...in a submarine.
Who's balking? I'm right there under the water. I find myself craving a destroyer, without quite knowing what I'd do with one ;)
Is that accurate? There's clearly more to it, as there's at least one conceptual leap between that notion and any kind of inference.
So, if we have another function and we call it with a noun of that type, we know the range of the input, we know the code in the function, we can infer the range of the output. It's not terribly rocket scientific.
I think you're saying a type is the range of inputs to function1 which succeed by not crashing; given function2 and a noun in the type, we may use function1 to infer the range of values which function2 must accept? Maybe?
In any language, a type defines a set of values and some semantics for manipulating those values. It so happens that our way of defining common sets is to build a function whose range is some useful set.
Actually any gene (ie, expression) has a product range. It doesn't even need to be a function. So the range of the constant
[%foo %bar]
whatever the subject is, is always [%foo %bar], ie, the pair [7.303.014 7.496.034].
You're not a big believer in airbags, are ya.
Generally we don't actually use these functions unless we're normalizing foreign data. Then, we do. Because anyone on the Internets can send a bull into your steer pen...
Mathematicians keep all three words around because each of them has its use.
Obviously you never met any of these people, but you will find many negative stereotypes coming to mind. Are many of them true? Perhaps they are. Was the old Versailles full of charming, brilliant, talented, wonderful people? It most certainly was.
You might also have some stereotypes of PHP programmers. Perhaps they're true as well. No set of human beings is without patterns of fault. However, the PHP programmer is a peasant and cheerfully accepts the daily rain of mockery that falls on his head. He knows he is not above being laughed at, indeed he knows he is laughable, as all human beings are in some way laughable.
The distinctive feature of a privileged class, always and everywhere, is that it can't accept being mocked. Unfortunately this always increases the temptation to mock it, which I agree is a low and unproductive pastime. But anything to make type inference seem fun...
Some PLs, are therefore academic in the same sense that Esperanto is academic, and are rightly criticized for that. They may be "perfect languages", but the fact they are not widely adopted is conclusive proof that they're a failure, at least in some respects. Sometimes this failure could be mere marketing; usually it's much more than that.
Often the financial backing is very conservative. It does not like to take risks. So they go with what is familiar.
Second, I can't think of a single academic I know that set out to create "the perfect language". Often one is created to explore an idea. That does not mean the language isn't incredibly valuable for the lessons it provides - but it likely was never meant to hit mass adoption.
Hence "academic". Design for idea exploration rather than widespread adoption is a crucial property of a language, and a valid target for criticism.
Intellectuals are no different from anyone else - they live in the same reality and must be judged by their results. I don't think anyone would disagree that PL theory, as a body of work, has produced a set of languages whose penetration in the real world is oddly small both given (a) the investment in these technologies, and (b) the many real advantages of typed higher-order programming.
As a general pattern, usually when I see this outcome explained, it takes the form of blaming the user. We wouldn't let anyone else get away with this excuse, so why should intellectuals be treated as a privileged class?
To be anti-intellectual is to judge intellectuals more harshly than they deserve. To be pro-intellectual, also a cognitive bias, is to judge them more leniently than they deserve. In a world whose bias is generally pro-intellectual, it's easy for a neutral assessment to seem relatively anti-intellectual, but perhaps what you are perceiving is not an exceptional bias but the absence of a systemic bias which you've grown used to.
PL theory, as a "body of work" has produced a wide range of languages ranging from Agda to Scala to Java. Some of these have actually seen use! Everything from classical music to Justin Beiber. TAPL, for example, is certainly not limited to the less popular languages: it talks about the foundation for Java-style types as well. Some of the same people working on ML and Haskell are also behind designs of Java and C#.
The point of a language like Haskell is to be expressive and useful, not to appeal to a large base population. Popularity and industry uptake are not the only measures of success. (This is, coincidentally, one of the things I don't like much about Berkeley's graduate program, or at least the systems lab I spent a bit of time in: they did seem to think industry uptake to be the only metric that mattered.)
Beyond languages, PL theory serves the role of all theory: it's the foundation upon which everything else is built. Things like the JVM memory model are based on the theory themselves and designed with tools stemming directly from that theory. Sure, the average programmer on the street is never going to use a theorem prover, but they will use the JVM where the memory model has been verified with one.
All this reminds of nothing more than the usual arguments that Linux is a complete failure because nobody uses it on the desktop. But I think that argument is not true even if you limit yourself to "Linux on the desktop is a failure": sure, not many people use Linux on the desktop, but the ones who do find it very useful and are exceptionally productive. Same principle applies to PL theory and functional programming languages.
There are many different ways to have an effect in the world, and the most obvious and direct one is not necessarily best. Even if it feels best.
(Also, it is a serious overstatement to attribute Java and C# to PL theorists. Gilad Bracha is not James Gosling. PL theorists have contributed to some extensions to these languages. Typically, the extensions that confuse people and make them feel stupid.)
The difference between the foundation and a foundation is enormous, because (with your very large expensive foundation) you are asking programmers either to program without knowing the foundations of their work, or to learn a large and challenging body of mathematics.
And you know, higher-order typed programming is good enough that it's almost worth it. For most potential customers, however, learning PL theory does not seem to be worth it. Nor are they comfortable in programming in Haskell, a very powerful and complex environment, without understanding it.
It's this "the customer is just wrong" attitude that makes some of us sense an area ripe for disruption. Pride goeth before a fall.
Doesn't this apply to syntax as well?
It would certainly be an interesting practical experiment to try to adapt a conventional syntax to the same semantics, or even to discard Hoon and create a more conventional language targeting Nock (which Urbit would have no trouble running).
PL research just hasn't had much affect at all on mainstream programming.
It's too bad. The PL world has a lot of good ideas. It's unfortunate they try to make them totally inaccessible.
Worse still that industry has no interest in raiding the PL world. A lot of the languages that have been designed are perfectly usable by mere mortals and a real step up from languages coming out of industry.
Compare OCaml and Java in 1996. OCaml (then Caml Special Light) was clearly the better language. Why didn't anyone get to use it?
Tikhonj is right about this kind of "anti-intellectualism." But pro-intellectualism is a bias as well.
I'm a PL theorist, and I disagree.
Who cares about your opinion on PL theory, its practitioners, and its textbooks? Is internalizing your hate for TAPL necessary for understanding the semantics of Urbit and related technologies? Why don't you just state succinctly what your ideas are and let them stand on their own merits.
That being said, I have no idea what your ideas are. Your website is unintelligible. Ironically, one of the things PL theory provides is a common vocabulary amongst practioners, which helps us communicate. I shouldn't have to learn a new alphabet (or in your parlance, a set of runes?) to figure out what new ideas you bring to the table. That kind of stuff is just not interesting to me. It's like if you 'rejected' English and wrote the rest of your work in Esperanto.
We may mean different things by "practitioners." I mean programmers. Unfortunately, your vocabulary is not common to programmers and shows no signs of becoming so.
Mine isn't either. But at least I've only been trying for a week. I know it seems strange to introduce new designs in the 21st century - most people assume, rightly of course, that everything worthwhile got figured out in the 20th.
Why I disagree with your disparaging remarks aimed at PL theorists is irrelevant.
The Urbit documentation should say what Urbit is, why it is important, and how to use it. Your disparaging remarks do not help to answer these questions. In fact, they do the opposite by antagonizing many readers and unfortunately giving you the appearance of a crank. Therefore, you should remove the remarks.
Knocking down PL theory does not boost Urbit up.
> We may mean different things by "practitioners." I mean programmers. Unfortunately, your vocabulary is not common to programmers and shows no signs of becoming so.
This is flamebait.
> I know it seems strange to introduce new designs in the 21st century - most people assume, rightly of course, that everything worthwhile got figured out in the 20th.
This is a strawman, and a particularly odd thing to say to someone who is also interested in advancing the state of the art.
Yes, there is a purpose to the disparaging remarks. The purpose is to make this asymmetry apparent.
Academia in the late 20th century is something of a footnote to the great achievements of the 19th and early 20th. In this golden age of science, peer disparagement was more or less universal. It is only in the second half of the 20th, the golden age of grants as it were, that genuinely criticizing your peers becomes a faux pas, and team-building becomes the essential skill for a practicing scientist.
But wait, I'm not your peer at all. I guess I forgot that...
I'm afraid I don't have anything else to add to this discussion. Good luck with your endeavors.
The attacks on TAPL too are seemingly weird, because arguably it's one of most thudingly concrete and down to earth books on types ever written. The whole book is about applications to real world problems and reveling in the fact that one haven't read it seems very asinine.
All I would say is, s/types/PL theory. Let's take your statement as true and stipulate that TAPL is in the top 1% of down-to-earthness of books on PL theory. Is it in the top 1% of down-to-earthness books on, say, Java? If not, what does this tell us about PL theory? You have read TAPL, right?
PL theory is a beautiful system and I've never said otherwise. TAPL is also very good at keeping doors open. But so are many things. PL theory is not the theory of programming, any more than TAPL is the doorstop. It is a theory of programming and a doorstop.
Yes I have read TAPL, it's sitting on my desk right now. I'm not even sure what you're trying so say, the fact that a book on type system design doesn't have advice on Java* seems perfectly natural to me. A book on goat husbandry doesn't have advice on Rails development. What are you trying to say?
> PL theory is not the theory of programming, any more than TAPL is the doorstop.
This is the strawmen that you're arguing against that seems bizarre to many people. PL theory is not so much about the lambda calculus and Hindley-Milner as it is about applying rigor and discipline to the study of programming languages. And yes, sometimes that involves learning the mathematical formalism.
* Chapter 19 in TAPL actually does have an implementation of Java's type system.
What you're asserting is that without this system of rigor and discipline, there can be no other rigorous and disciplined way of defining programming languages. For one thing, this flies in the face of everything we know about the philosophy of mathematics.
I think my way of defining programming languages is pretty rigorous and disciplined. I'll continue to think that until you or anyone can identify some sloppy ambiguities. I note also that my foundation fits on a T-shirt and yours needs a math textbook...
Here, you can look at my axioms and identify anything unrigorous or undisciplined about them:
https://github.com/urbit/urbit/blob/master/Spec/nock/5.txt
A bunch of people have written compatible implementations from the spec, which is the RFC world's general sanity test.
Hoon seems to fail that test.
I've yet to see how this is better than vanilla ML. I don't see that because Hoon doesn't use standard syntax or terminology. I can't just read some code and a language overview to decide if this is worth (a lot of) my time.
I think ML has a fairly steep start-up cost but is definitely understandable by regular people and has real productivity benefits.
Hoon is sufficiently obfuscated that it has an incredibly high barrier to even evaluate as a language. I don't think you need to have tons of unintelligible typing rules to make things familiar. By avoiding standard syntax and terminology, it puts an enormous burden on the potential user.
Is it always the case that the vowels may be compressed away without loss of meaning? It seems to work some/most of the time, but there is a least a %wet and %wut... I think?
Though this be method, yet there is madness to it.
Human brains are incredibly good at raw memorization of associations. Hoon has about 100 digraphs, and their internal structure isn't random. How hard is to learn 100 characters of Chinese? Perhaps easier than you think.
Nor are there no payoffs. For instance, most languages are very bad at defining large, mostly static hierarchical trees, so when it comes time to write code that generates, say, an HTML page, you reach for a special "template language" DSL. That's not a problem we have in Hoon. Also, most functional languages have a very annoying tendency to crawl off the right side of your screen and disappear, because indentation depth matches functional depth. That's also not a problem we have in Hoon.
So... you pay, definitely. But you also receive.
Take his Software Foundations book. It opened up Coq in a very practical way. No crazy typing rules or category theory. Just straight programming and simple proofs. That's a world where previously the few who entered were sucked down a rabbit hole of theory, never to return again.
I may of course simply be looking through a bottle (and constrained by backwards-tracking logicians).
All of this is starting to smell of an Incompleteness Theorem of Programming Languages.
It's not that other languages don't make up arbitrary terms as well, but it's hard to understand why a language that claims to be simple and "moronic" does it so enthusiastically, with the result that anyone trying to learn it has to first memorize a large number of terms.
Think of the number of things you need to memorize to be an auto mechanic. Yet there are a large, large number of people who are capable of becoming auto mechanics, but not capable of becoming Haskell programmers.
...and since a programming language should be primarily designed for humans (or, as I actually see it, a programming language should be an interface between the human mind and the computer) and at the same time be executable by computers, choosing more memorization and less abstract concepts seems like a bad idea ...most smart people's minds find juggling abstract concepts easier and more enjoyable than memorizing rules (and when working memory is not enough to hold all the abstract concepts we're juggling, we use anything from pen and paper to other more advanced devices - just ask any mathematician), and those that don't are also those that "just don't get (or like) software", so they shouldn't be programming anyway.
[EDIT] As a reply points out, Gonad is gender neutral. I still think that this humor is distasteful.
On the other hand, the identity dialogue defaults unwary bros to %lady, which certainly ought to cause a little wailing and gnashing of teeth.