Dependent types and homotopy type theory for general purpose programming. I am definitely excited about it, but not really sure if those hopes will ever materialize as some useful (even in the limited scope) technology.