I take your point, but I don't think _anything_ can defend against unknown attacks. However, we could defend against all known attacks using formal methods, wh

I take your point, but I don't think _anything_ can defend against unknown attacks. However, we could defend against all known attacks using formal methods, which is a lot better than we're doing at the moment. Further, when a new attack becomes known, I would wager that having something that is verifiable today will be easier to verify or fix in the future, as compared to a code-base that is not provable. Just because we can't achieve theoretical perfection, we should not rule out using methods that would solve many of the actual problems we encounter today. Of course, if you can find a way to defend against unknown future problems, I'm all in favor of using your method!