Regarding the last paragraph from the article, about lock-in: as long as the chosen foundations are strong enough to reason about proofs themselves (as formal

Regarding the last paragraph from the article, about lock-in: as long as the chosen foundations are strong enough to reason about proofs themselves (as formal objects), it doesn't really matter. For example, suppose mathematics gets locked-in to a proof verifier based on Logic A, and I want to work from Logic B. Rather than prove Theorem T using Logic B, what I can do is prove Theorem T* using Logic A, where T* is the theorem: "Logic B proves Theorem T".