[jarrett]

> can never account for data that are provided only after compilation

It seems to me they could. Suppose my program depends on external input D. That input could be a file it loads, keyboard input, network input, or anything else. Could I declare that I expect D to have properties P? And then, could the language force me to implement a code path for cases where D does not satisfy P? An example of such a code path would be to print an error message and then terminate the program.

[JadeNB]

Yes, this is a good point. I hope that what I meant was reasonably clear, but a more precise would have been something like "cannot prove certain assertions about data that are provided only after compilation".