[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".