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 programm

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-logic.html#/semantics https://ucsd-progsys.github.io/liquidhaskell-tutorial/02-log... * SMT Solver Language Integration Cryptol: https://github.com/GaloisInc/cryptol https://github.com/GaloisInc/cryptol * Session Types Scribble: http://www.scribble.org/ http://www.scribble.org/ * Dependent Types Agda: https://en.wikipedia.org/wiki/Agda_(programming_language) https://en.wikipedia.org/wiki/Agda_(programming_language) Idris: http://www.idris-lang.org/ http://www.idris-lang.org/ * Effect typing Koka: https://research.microsoft.com/en-us/um/people/daan/madoko/doc/koka-effects-2014.html https://research.microsoft.com/en-us/um/people/daan/madoko/d... * Formal verification Coq: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html TLA+: http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html 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.