Dear dwohnitmok,
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: