It depends on your system model (e.g. do you consider memory corruption to be a valid threat), but it could be. In practice, actually establishing that proof pu

It depends on your system model (e.g. do you consider memory corruption to be a valid threat), but it could be. In practice, actually establishing that proof purely in code is almost always impractical or doesn't address the full problem space. You use hardware to help out and limit the amount of code you actually have to validate.