The creator of Rust in his own words:

“ Introducing: Rust Rust is a language that mostly cribs from past languages. Nothing new. Unapologetic interest in the static, structured, concurrent, large-systems language niche, Not for scripting, prototyping, or casual hacking, Not for research or exploring a new type system, Concentrates on known ways of achieving: More safety, More concurrency, Less mess, Nothing new? Hardly anything. Maybe a keyword or two, Many older languages better than newer ones: e.g., Mesa (1977), BETA (1975), CLU (1974) … We keep forgetting already-learned lessons., Rust picks from 80s/early 90s languages: Nil (1981), Hermes (1990), Erlang (1987), Sather (1990), Newsqueak (1988), Alef (1995), Limbo (1996), Napier (1985, 1988).”

If modern PL research is trying to take credit for the latest hot programming language (which I doubt they are, it’s only internet commentators who have nothing to do with PL research who argue with me. Actual PL researchers don’t care about Rust), they should be embarrassed.

Thank you for linking latest PL research, it has been a while since I’ve gone through it, glad to see nothing has changed. Ask yourself, how many of those talks in day 1, have accompanying code? is it even 25%?

For giggles I decided to peruse through “Normal bisimulations by Value”. A 54 page dense paper with theorems, equations and lemmas. Lol, what are we even doing here? You can also notice that they don’t bother justifying their research in the intro or the abstract, claiming relevance to any actual programming language. They themselves realize it’s just math, and PL researchers has become a euphemism for math. Frankly, even one such paper being accepted to a PL conference tells me something is going awry in the field, but if a majority of papers are like this, then the field is a wasteland, that only serves to grind young talented minds into spending their lives chasing academic prestige with no value to society.

> Ask yourself, how many of those talks in day 1, have accompanying code? is it even 25%?

57 out of 93 papers (61%) published at POPL 24 have an artifact available. Note that this may also be automated proofs etc, it's not necessarily "running code".

But I also think focusing on POPL as a representation of the PL community isn't entirely fair. POPL is the primary conference focused on type systems within the PL community. It's a niche within a niche. Conferences like OOPSLA, ECOOP, or ICFP are much broader and much less likely to be so focused on mathematical proofs.

[1] https://dl.acm.org/toc/pacmpl/2024/8/POPL

I asked Claude to go through all paper names and estimate how many have code vs how many are proofs:

“Based on my analysis, I estimate: - ~35-40 papers (roughly 35%) likely have significant accompanying code - ~55-60 papers (roughly 65%) are primarily theoretical/mathematical proofs “

I suspect even the remaining 35% doesn’t have much to do with programming languages, and I don’t think these stats change much for other conferences.

> I don’t think these stats change much for other conferences.

I'd severely doubt that: there is a large difference in focus on theory vs practice between conferences. POPL really is one of the more theoretical conferences. At a conference like ECOOP, you're unlikely to see many proofs (I'd guess at most 20% of papers, based on personal experience).

I did the same thing for ECOOP 2024: https://2024.ecoop.org/track/ecoop-2024-papers#program

Claude estimates 10 papers related programming languages and its features and 27 related to theory, verification etc.

One sub-field of PL research is the ability to formally specify programs, and thus understand their meaning and prove their correctness. A great project that is based on lots of theoretical foundations and practical implications is compcert [1]. They wrote a C compiler and proved that it translates C code to equivalent assembly code. You couldn't even state the problem without all the maths, let alone prove it. I'd argue that having correct compilers is worth the effort.

I assume "Normal bisimulations by Value" talks about equivalence relations between concurrent programs. If you want to prove correctness properties of concurrent programs or cryptographic protocols, this is one of the tools. It's not because there's no code and only maths that it's not relevant.

> Actual PL researchers don’t care about Rust

Not true, I just watched this video a few days ago about Rust semantics [2]. How would you prove that a Rust program making use of unsafe construct is actually safe? what does safe even mean? how to describe rigorously the behavior of the rust type checker? AFIAU there's not even an informal spec, let alone a formal one. How are you supposed to write correct program or compiler if the language isn't specified?

> Rust is a language that mostly cribs from past languages. Nothing new.

Doesn't mean that Rust isn't influenced by academic languages and ideas. Anybody who knows Haskell or OCaml see the direct influence.

Research isn't industry. A lot of what is produced may have no direct applications but may in the future. This is the point, it's research. Also it's not because you don't see the connections between research and application that they don't exist. Lots of people working on these industrial tools have an academic background and bring their knowledge into the equation.

> If modern PL research is trying to take credit for the latest hot programming language (which I doubt they are, it’s only internet commentators who have nothing to do with PL research who argue with me. Actual PL researchers don’t care about Rust), they should be embarrassed.

You're the one explaining that Rust didn't benefit from academic research which is obviously not the case.

[1] https://compcert.org [2] https://www.youtube.com/watch?v=9y1dLDnS4uE