That sounds (close to) impossible. How would you tell if a given piece of code sorts a list properly? There are a million and one sorting algorithms and the static analyzer would have to be really smart to be able to check that reliably.
The fact that the general problem is impossible does not mean that the entire area of study is useless.
and restricted languages such as Spark http://en.wikipedia.org/wiki/SPARK_(programming_language)