5 ms·
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 com
by yodsanklai 2y ago
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/ https://popl24.sigplan.org/program/program-POPL-2024/
[2] https://news.ycombinator.com/item?id=34704772 https://news.ycombinator.com/item?id=34704772)
Edit: regarding https://x.com/deedydas/status/1846366712616403366?mx=2 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.
- sashank_1509 2y agoThe 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.
- JW_00000 2y ago> 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 https://dl.acm.org/toc/pacmpl/2024/8/POPL
- sashank_1509 2y agoI 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.
- JW_00000 2y ago> 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).
- sashank_1509 2y agoI did the same thing for ECOOP 2024: https://2024.ecoop.org/track/ecoop-2024-papers#program 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.
- 2y ago