[scott_s]

I'm not quite sure what you mean. Being able to "express the program" (which I take to mean a human writes the program) is independent of being able to statically verify what it does.