Research and open challenges in Programming Language Theory 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.
I think the overall goal of PL theory is to lower the cost of
large-scale programming by way of improving programming languages and
the techincal ecosystem wherein languages are used.

Here are some high-level, somewhat vague descriptions of PL research
areas that have received sustained attention, and will probably
continue to do so for a while.


Most programming language research has been done in the context of
sequential computation, and by now we have arguably converged on a
core of features that are available in most modern programming
languages (e.g. higher-order functions, (partial) type-inference,
pattern matching, ADTs, parametric polymorphism) and are well
understood. There is as yet no such consensus about programming
language features for concurrent and parallel computation.    
Related to the previous point, the research field of typing systems
has seen most of its activity being about sequential computation.
Can we generalise this work to find tractable and useful typing
disciplines constraining concurrent and parallel computation?
As a special case of the previous point, the Curry-Howard
correspondence relates structural proof theory and functional
programming, leading to sustained technology transfer between computer
science and (foundations of) mathematics, with e.g. homotopy type theory being
an impressive example. There are many tantalising hints that it can be
extended to (some forms of) concurrent and parallel computation.
Specification and verification of programs has matured a lot in
recent years, e.g.  with interactive proof assistants like Isabelle
and Coq, but the technology is still far away from being usable at
large scale in everyday programming. There is still much work to be
done to improve this state of affairs.
Programming languages and verification technology for novel forms of computation. I'm
thinking 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 of
overlap between them, and that there is some more abstract approach
waiting 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 open
problems like the P/NP question where we can immediately say if a
proposed solution works or not.