Hacker News Reader

> has there been any useful Programming Language that has come out of PL research/ Academia in the last 20 years?

The goal of PL research is not, usually, to produce languages that see commercial adoption but to produce ideas that industry adopts. You cannot say a language like Rust is not influenced by PL research.

No, I can very strongly claim that I doubt any of the modern languages like Rust, Go etc have been influenced by the trainwreck, that is programming language research.

PL research today is actually the study of something called “type theory,” whose relation to the act of building programming languages is the same relation a math PhD has to a carpenter. You will be a great mathematician if you do PL research but I would prefer if you do it in the maths department and not con us into believing it has something to do with programming languages. This is apparently what undergrads are taught in a compilers course: https://x.com/deedydas/status/1846366712616403366 I rest my case. (imagine the grad course syllabus)

On the fringes, you might find research groups who are doing interesting useful stuff in programming languages, but that is an exception to the rule. Which is probably why, you never hear any of the new language developers ever cite programming language research.

There is much more to PL research than "type theory". Look for instance at POPL 2024 program [1].

Also Rust has been influenced by type theory. Rust first compiler was written in OCaml and the influence of OCaml/Haskell (and many other languages [2]) is pretty clear.

Goal of PL research isn't to design programming languages but academic research has a lot of influence on programming languages.

[1] https://popl24.sigplan.org/program/program-POPL-2024/ [2] https://news.ycombinator.com/item?id=34704772)

Edit: regarding https://x.com/deedydas/status/1846366712616403366?mx=2 these are just the formal specs of a type checker. Nothing magic or very complicated there, it's just a notation. Anyone who can understand and implement a type checker should be able to understand this notation as well.

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

Have you ever talked to the people who design those languages? Because they will disagree with you about as strongly. And, of course, they are in a position to be correct.

1. TypeScript (and Dart, which influenced it) would not exist without the research on gradual and optional typing. Many other of the type system features in TypeScript – like type inferencing, intersection and union types, and type-level programming (e.g. conditional types) – find their origin in PL research, and were uncommon in mainstream but common in academic programming languages before TypeScript appeared.

2. Similarly, mypy was created by Jukka Lehtosalo as part of his PhD [1] and part of a wave of research in applying gradual typing to dynamically typed programming languages.

3. Rust's ownership types and borrowing are based on PL research, such as linear logic / linear types. Same for traits. Early Rust even had typestates.

4. Several of the core developers of Rust, Go, TypeScript, C#, Dart, Scala, have a PhD in PL or a background in research.

5. Generics are another feature that was heavily researched in academia (admittedly a longer time ago) before becoming part of mainstream programming languages.

So I completely disagree with you: most modern languages have been heavily influenced by programming language research. In fact, I'd be hard-pressed to find a modern PL that hasn't been in some way influenced by PL research.

(One thing I agree with in your comment, is that current PL research focuses too heavily on type systems and should look more at other interesting PL features. My recommendation to InkCanon would therefore be to look broader than type systems. The problem with research on type systems is that, because it looks math-y, it feels more like "science" and hence "cures impostor syndrome". But cool stuff can be real science too!)

[1] https://mypy-lang.org/about.html

Ask yourself this, has there been any useful Programming Language that has come out of PL research/ Academia in the last 20 years?

Scala

There are several assumptions here tangled together here

1) Use is sufficient, but not necessary for impact. Theory of relativity, a lot of QM, etc has had only uses in real world edge cases, but have enormous value. The value function for impact, so to speak, includes more than just use.

2) There is the structure of academia and it's incentives, the average behavior of people in it, and it's outcomes. I don't necessarily have to bow to it's incentives, nor behave like the average person in there. Academia is also sufficiently large and fractal that you can find people less interested in the incentives and more in some thing they obsesses about.

PL has had some interesting, although sometimes unheard of, real world uses. CUDA for example. A significant chunk of PL now focuses on ML. Awhile back a company called Monoidics got acquired my Facebook for work on static bug finding with formal methods. Rust has been pretty influenced by PL concepts. New languages like WASM are formally verified from the ground up, and there are exciting opportunities for that.

I have considered slinging my resume to more research oriented companies, but hearsay from people is that the golden age is over. Under FOMO and stock market pressure, these companies are eradicating the kind of freewheeling research they used to and dumping money into ML and ML hardware. Not to mention it's a bit of a dice roll and a circus to get a job at such companies nowadays as a fresh graduate.

The only group under low pressure, free to do anything they want in Academia are tenured profs who have established themselves well or grad students who don’t care at all about remaining in Academia (and presumably have NSF fellowship or similar so that they don’t need to listen to their advisor either). Everyone else needs to grind, profs without tenure are arguably under the highest pressure, PhDs who want to stay in academia have high pressure etc. If your prof is tenured but not established and is struggling for grant money, even he is under high pressure to publish and win grants, something I learnt the hard way. The grant acceptance rate is what, like 20% these days.

My 2 cents, you will be more likely to encounter creative coders who are passionate about a field in the right industry team than Academia. Unfortunately getting into the right industry team is also a grind, and you likely won’t get there right out of undergrad, but within 10 years, if you put effort and grind, you can get there. I think it’s better odds and more fun than going to academia, but your mileage may vary.

> A PhD is a program to compete for academic prestige

That's true for some people but others have different motivations, such as learning useful skills so they can gain the ability to work on interesting problems in a given field.

Doing a PhD in PL can also help you get the kind of jobs you mentioned, and achieve more once you're there. For me, the most valuable I thing I got out of the process was extensive exposure to the literature, which has been useful in a range of contexts.