I think, the most interesting field now is dependent types. Researches have achieved substantial progress in the last 10 years: * Large mathematical theorems w

I think, the most interesting field now is dependent types. Researches have achieved substantial progress in the last 10 years: * Large mathematical theorems were proved in Coq (Feit Thompson Theorem) * An optimizing C compiler with correctness proof was created (http://compcert.inria.fr/ http://compcert.inria.fr/) If this stuff gets to mainstream and I think, it will get there in 5-10 years, we will have unprecedently reliable and secure systems.