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.

Yes, it is impossible. See: Halting problem.

The thing about program verification is that everyone knows that of course it is in general impossible. However, I am not writing a simulator. Most of the code I write does not actually take advantage of the power of a Turing machine.

The fact that the general problem is impossible does not mean that the entire area of study is useless.

see: dependent typing http://en.wikipedia.org/wiki/Dependent_type

and restricted languages such as Spark http://en.wikipedia.org/wiki/SPARK_(programming_language)

I'm pretty sure that Pex [1] does the static analysis on these things. It's C#, but should be close enough for you to get the idea.

[1]: You can play with it here: http://www.pexforfun.com/