Lambda the Ultimate

Of course, types are Actors that can be used in computations just like other Actors.

But parametrized types require special treatment and rules.

I think you mean to say that types are actors in ActorScript. There are many type systems where types are simple types, and values are values, and there are no actors at all.

Some of the above are possible even without dependent types. For example, Rossberg's 1ml unifies functions and functors (type constructors) and allows you to treat list as a value of type type -> type, while desugaring into plain System F_ω (heavily utilizing existential quantifiers and higher-kinded types).

As for types like array[float, 3], I'd prefer something like refined types with an automatic theorem prover instead of full-blown dependent types.

Much has been written about the downsides of gamification, but at least it does add some positive feedback to a discussion. Many of those empty conversations could be:
* Yes, that is very interesting but personally I have no comment to make.
* That's a load of rubbish, I have no interest in that at all.
* I like what is being said but I agree with the viewpoint being expressed so there is no way to join in without a somewhat empty "me too!" +1.
Where, currently there is no real way to tell these states apart.

I agree completely with your observations on the literature at large, and the underlying causes for its current state. I also really like reading the contributions that gasche makes, although frequently I fall into one of two of the states above, and thus don't really add anything.

What kind of mechanism (social or technical) would add some positive feedback to the discussions on LtU without falling into the trap of reinforcing groupthink / gamifying the site?

The context of a discussion can make all the difference in how developable it is. The first mention of my fexpr research on LtU (that I know of), a straightforward sharing of the Kernel web page I was maintaining, didn't generate much discussion (though it did result in my becoming aware of, and ultimately joining, LtU :-). From time to time fexprs/Kernel were relevant to discussions and I'd make small comments when they seemed pertinent; but the deep, interesting discussion of the issues involved that I'd have liked to have didn't occur until about three and a half years later, with a topic on first-class environments. So, patience and looking at things from different angles can eventually pay off.

[Note, I'm looking just at what it took for that particular theme to get discussed in depth.]

To clarify, I think that having no comment to make is perfectly fine (whether one is interested in the work or not), and I am not particularly troubled by the fact that most discussions are very quiet for this likely reason. Having stimulating discussions of the presented work is always great, but we should not expect it to be the default state.

(We could also afford a lot more of "I don't know about X and thus don't understand point Y, can anyone provide extra details?" comments than we have today.)

… and while I personally could benefit in a few cases from the "don't understand" point, I would consider it a shame if LtU became a PL version of stack exchange.

LtU is intimidating at first, and although that may dissuade the casual browser, it's what makes the place unique. For non-academic members (and possibly for those in academia) it's necessary to read the papers (in my case, sometimes multiple times) to even begin to get a grasp of what's going on, and that's far too much like hard work for the majority of “internautes”. I often find myself thinking "I'm way out of my league here", but try and follow along anyway - the voyage can be as interesting as the final destination.

It would be hard to call C# an acedemic language, or , for that matter, C++, F#. They came from companies, often involved some non PhDs, and anyways, were driven in solving problems vs. investigations of the possible. Are bell labs, Microsoft research, Xerox park like universities with acedemic research projects? Not really. Is Anders an acedemic trying to publish papers or an experienced language designer? The answer to that is easy. Was Don Syme doing research when he designed F#, or was he designing a language to fill a need?

Also, foundationally speaking, you don't need clearly defined semantics at the onset, and plenty of languages are used successfully without them. That is not to say they aren't useful, but necessary is a much higher bar! Of course, when we start talking about Rust and BitC that are claiming some extra degree of safety, then it is kind of a different ballgame. But there also has to be value in those semantics, they have to pay off or it is just cargo culting tedium. E.g. What would Swift gain from more formal work? Beyond full employment for PL researchers, what is in it for programmers? Why not invest it better tooling instead?

The rigor fad seems to have started when GLS was put on to do the JLS along with Gilad Bracha. But as far as I can tell, only C# (out of the production languages) has gotten similar attention given work from people in MSR (along with Mads). No one else really has the resources for it, and even Scala lacks much in terms of formal specification. So swift is not really an exception at all, rather it is the same process that new languages start and get big have always followed.

I'll question that "usable" is equivalent to "has lots of users", and I'll question that "research" is a value in itself.

Let's go for "lots of users": With the right budget, it might be quite easy to get lots of users: use only tried and tested ideas, keep everything as simple as possible, write documentation, maintain backwards compatibility, practice some form of marketing, hire people to write GUI libraries, run on lots of platforms, provide acceptable performance, fill a gap...

You can see how this recipe over time leads to languages that become less and less usable: as usage increases, new gaps are identified and revisions become necessary... I think it might be rational for a company to evaluate the results of research activity in economical terms, and that will lead to decisions that may or may not be pleasing to researchers and likewise such evaluation may have been too shortsighted and thus important developments are missed or picked up too late by "the" industry.

The whole discussion here is bound to be rendered a bit more obsolete (or imprecise) by the next appearance of some research output in an "applied" language, or the next research paper that solves a problem that was only found in "industry" language X.

There are programmers (and programming situations) where a spec will be preferable to all sorts of tooling, and then there are tools that will make inherent language shortcomings bearable. There is also a lot to be said about free and open source software and how it builds a body of research that one probably would not call academic but it contributes to the body of human knowledge in a very similar way.

Too many acronyms. Needs lowercase.

Guy L. Steele, Java language specification, Microsoft research.

Great. Thanks.

Typing on tablets leads to shortcuts.

Yeah, I've seen you do it more often. It makes your posts hard to read sometimes, though.

It's summer and China lacks daylight savings time, I wake up at 4am in the morning and have nothing to do but post to LtU from bed using an iPad.