Sure, but as of July 2015 the programming languages (e.g. Agda, Idris) that can give full specifications of their own programms, are experimental, not mainstream.

«Which is usually as interesting as the program itself.» And ten times as hard to write. Not just saying that — I spend most of my time in Agda, and even simple things are rather difficult. But I think this will improve as we learn the right way to look at things.