Please see Rice’s Theorem.
I’m not at all familiar with Rice’s Theorem, and from a quick read, it does seem applicable. However, I’m not sure where it breaks taint analysis.
Are you implying that this approach will report falsely tainted variables, or that it is impossible to prevent false negatives? I believe the former is acceptable (as long as the language provides an escape hatch), and that the latter is unacceptable.
AFAIK, the plan is to enforce access lists when necessary.
Proofs/witnesses form a sort of informal access list which gets “checked” as the transaction is executed. I don’t see how this would be avoidable.
How will developers know if their access lists are complete? If an earlier transaction in the block can invalidate your access list, I think that’s a bug in your contract and we should endeavor to prevent it.
An alternative we considered was to introduce new syntax to give us the properties we want, but this would have too many disadvantages.
What disadvantages? Was there a write-up or post about it? I’d love to learn more about it.