The difference between theory and practice, is that in theory there is no difference, but in practice - there is.
So far, every "provably secure design" I've seen ended up being insecure in practice due to the things people abstract away.
I'm not saying it's impossible, but I have not seen it done perfectly thus far.
We've seen more success by having many many iterations and widespread usage of common designs and patterns. These are not perfectly secure by any means, but they are secure enough against common threats to make it functionally equivalent until we figure it out.
I just feel that our proven insecure system, with default authority, is a really bad foundation to have settled upon. We couldn't have picked a worse default.
Okay, name the "provably secure designs" that were actually proven and validated by a competent security standard such as the Orange Book Level A or Common Criteria EAL 6/7 that turned out to be insecure in practice.
Most people who say that point to designs that were never proven and never validated against anything meaningful, but I am open to seeing a actual example.
So far, every "provably secure design" I've seen ended up being insecure in practice due to the things people abstract away.
I'm not saying it's impossible, but I have not seen it done perfectly thus far.
We've seen more success by having many many iterations and widespread usage of common designs and patterns. These are not perfectly secure by any means, but they are secure enough against common threats to make it functionally equivalent until we figure it out.