Like most things, the kernel of tomorrow's ideas is already here. On the scale of the next five years, these ideas will give rise to what the future of programming will look like:

* Refinement types

Liquid Haskell: https://ucsd-progsys.github.io/liquidhaskell-tutorial/02-log...

* SMT Solver Language Integration

Cryptol: https://github.com/GaloisInc/cryptol

* Session Types

Scribble: http://www.scribble.org/

* Dependent Types

Agda: https://en.wikipedia.org/wiki/Agda_(programming_language)

Idris: http://www.idris-lang.org/

* Effect typing

Koka: https://research.microsoft.com/en-us/um/people/daan/madoko/d...

* Formal verification

Coq: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html

TLA+: http://research.microsoft.com/en-us/um/people/lamport/tla/tl...

This is the general trend, generally making more composable abstractions and smarter compilers and languages that can reason about more of our programs for us.