| 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. |