In the spirit of some general discussions like this one, I'm opening this thread with the intention to gather opinions on what are the open challenges and hot topics in research on programming languages. I hope that the discussion might even bring to surface opinions regarding the future of research in programming languages.I believe that this kind of discussion will help new student researchers, like myself, interested in PL, as well as those who are already somewhat involved.
Research and open challenges in Programming Language Theory
pl.programming languages;open problem;research practice
I think the overall goal of PL theory is to lower the cost oflarge-scale programming by way of improving programming languages andthe techincal ecosystem wherein languages are used.Here are some high-level, somewhat vague descriptions of PL researchareas that have received sustained attention, and will probablycontinue to do so for a while.Most programming language research has been done in the context ofsequential computation, and by now we have arguably converged on acore of features that are available in most modern programminglanguages (e.g. higher-order functions, (partial) type-inference,pattern matching, ADTs, parametric polymorphism) and are wellunderstood. There is as yet no such consensus about programminglanguage features for concurrent and parallel computation.    Related to the previous point, the research field of typing systemshas seen most of its activity being about sequential computation.Can we generalise this work to find tractable and useful typingdisciplines constraining concurrent and parallel computation?As a special case of the previous point, the Curry-Howardcorrespondence relates structural proof theory and functionalprogramming, leading to sustained technology transfer between computerscience and (foundations of) mathematics, with e.g. homotopy type theory beingan impressive example. There are many tantalising hints that it can beextended to (some forms of) concurrent and parallel computation.Specification and verification of programs has matured a lot inrecent years, e.g.  with interactive proof assistants like Isabelleand Coq, but the technology is still far away from being usable atlarge scale in everyday programming. There is still much work to bedone to improve this state of affairs.Programming languages and verification technology for novel forms of computation. I'mthinking here in particular of quantum computation, and the biologically inspired computational mechanisms, see e.g. here.Unification. There are many approaches to programming languages,types, verification, and one sometimes feels that there is a lot ofoverlap between them, and that there is some more abstract approachwaiting to be discovered. In particular, biologically inspired computational mechanisms are likely to continue to overwhelm us.One problem of PL research is that there are no clear-cut openproblems like the P/NP question where we can immediately say if aproposed solution works or not. 