3 ms·
> 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 cou
by jarrett 13y ago
> 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 13y agoYes, 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".