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

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 https://compcert.org [2] https://www.youtube.com/watch?v=9y1dLDnS4uE https://www.youtube.com/watch?v=9y1dLDnS4uE