Annotations for zeroing the stack of "sensitive" functions which deal in transient secrets

[rpjohnst]

@CAD97

Your argument is basically that the formalization effort needs to consider practical uses and lend itself towards comprehensibility. Nobody disagrees with you there.

This may be the real disconnect- @Centril does seem to disagree, and suggests we exclude some tools and scenarios because they are hard or impossible to specify this way. That suggestion is what gets this kind of pushback, and arguments about "systems programming."