It would seem that, even though these languages weren't made from soup to nuts in academia, they mostly incorporated ideas therefrom; for instance, Ruby and (eventually) Python got closures that had been pioneered by Scheme. There's still plenty of valuable work to be done trying out ideas that will eventually be incorporated and popularized elsewhere.
And of course, there are still languages like Haskell that have carved out a nice niche, despite their recent vintage and academic roots.
Yeah, in Python design discussions I see academic papers cited with some frequency. So all's not lost -- the research is doing something. There is a lot of useless PL research but that's just the nature of exploring new ideas (though, not to ignore real problems with academia, some of which the field of PL research is particularly afflicted with).
"No field has been more infested by irrelevant formalisms than that of programming languages - also known as "PL research." So when I say Guy Steele isn't a PL researcher, what I mean is that he's not a bureaucrat."
I read basically all of the Lua papers and I think they're a great model for how to do programming language research. They use a real language for a testbed of their ideas. For example, there was a great paper that went over the history of coroutines and different options for designing and implementing them. There was also a great one about PEGs and a formal treatment of the implementation of the lpeg parsing VM. Somehow I feel that this kind of research wouldn't be respected at big name American CS universities, which is a shame, because it's exceedingly valuable.
That linked article is from 2007. Interestingly, the stuff that the author mentions as useless (proof carrying code) is now basically The Way that developers handle code that has security, reliability, or robustness requirements.
- Microsoft has long used a formal driver verifier to prove liveness and protocol properties associated with device drivers
One amazing piece of work going on right now in compilers is by Xavier Leroy, who cares a lot about formally proving that your compiler and its optimizations respect the semantics of the language (i.e. that its execution on hardware is within the range of possible executions specified by the original input language). Without the decades of work on formalization, semantics work, theorem provers, etc. the community wouldn't have a chance of tackling those problems today.
Certainly, if you read the proceedings of POPL or even some ICFP papers, you might wonder where it's going. And even the authors might admit to the same. But until you've fully explored the issues that come up when you try to merge (shameless example from my own work) effect types, region types, concurrency, parallelism, and transactions, it's hard to know what sets of language features can be safely combined in a way that programmers can modularly reason about and a toolchain can implement efficiently and correctly.
I don't think what Native Client does is the same as "proof carrying code". From what I gather, if it used proof carrying code, then it would do some verification on the receiving side at "compile time", and no sandbox for runtime checks would be necessary.
My understanding is that Native Client works with a combination of a special compiler toolchain (on the sending side) and runtime checks on the receiving side.
You are correct --- PCC (AFAIK) has not come about in the sense of carrying along a proof object that a formal verifier can validate is both correct and corresponds to the code payload.
As the other commenter pointed out, the SLAM tools are part of the Windows Device Driver Development Kit. The last time I talked to the kit's dev manager (~2003), they were talking about making it mandatory that you pass the formal verification in order to have your driver signed by Microsoft. Since those signatures are then verified at driver installation time, that feels very close to it!
I have to confess I'm only familiar with the publications on Native Client and not the actual product. From what I'd read, I understood that the verifier did some basic static analysis to prove that all possible executions did not validate some properties. In that case, no proof object is required, as the source code itself is the proof object. Assuming, of course, that they're actually doing the stuff talked about in the papers and in practice don't just "grep for dangerous instructions."
And of course, there are still languages like Haskell that have carved out a nice niche, despite their recent vintage and academic roots.