As you pointed out, such a proof does not mean that it is not operationally possible to derive a contradiction using axioms and rules of inference.
Instead our confidence in the consistency of a powerful strongly-typed theory is because there is just one model of the axioms of the theory up to a unique isomorphism, which formalizes the concept of "truth" that you mentioned in your post.
I looked up your papers... Then I noticed you have also worked on paraconsistent logic. So to just boldly go on a completely new tangent and ask a question I have long sought to ask: do you know a good introduction text for paraconsistent logic, for a graduate level computer science student?
Actually, powerful strongly-typed theories used in Computer Science can prove their own consistency!
See the following article for for how this is done:
https://papers.ssrn.com/abstract=3603021
As you pointed out, such a proof does not mean that it is not operationally possible to derive a contradiction using axioms and rules of inference.
Instead our confidence in the consistency of a powerful strongly-typed theory is because there is just one model of the axioms of the theory up to a unique isomorphism, which formalizes the concept of "truth" that you mentioned in your post.
For example, see the following article:
https://papers.ssrn.com/abstract=3457802