The real problem with what you've said, is that "finding the mathematical meaning of the abstractions you're using" is an incredibly hard processes, and almost nobody succeeds at it. And even then, you have to map these abstractions to hardware in a way that doesn't leak. And the only way to do that is to implement the machine itself (or a special hard-to-find-subset of it). Those are the only abstractions capable of leak-free modeling.