QED should urge systems to become more cooperative so that e. g. theories, formulas, proofs are reusable (which only in the most optimistic case means 'translatable'). When this has been achieved, we may examine the graph of connections that has emerged and classify its nodes.
Certainly, systems that get their proofs passed through the most tough basic proof checkers will be especially honored. This will - among others - strengthen the path from Typed Theorem Provers through Heavy Duty Theorem Provers to Basic Theorem Provers.
Ingo Dahn