Well, I kind of agree with this. Also in type theory there are axioms/assumptions hidden in the implementation. I myself made an implementation of the Calculus

Well, I kind of agree with this. Also in type theory there are axioms/assumptions hidden in the implementation. I myself made an implementation of the Calculus of Constructions (https://github.com/chrisd1977/system https://github.com/chrisd1977/system) with the goal of having a foundation that is as small as possible while it still being practical to prove large parts of mathematics. I do have to say that it turns out the the foundation is a little bit larger than I would have preferred. I am in particular a bit disappointed that I needed to create a type hierarchy. I.e., the most basic sets have type Type(0) which has Type(1) which has type Type(2) and so on. I am also not completely liking some of the axioms that I had to add, in particular regarding to equality. I kind of like your idea of having trusted extensions to provers. I was myself thinking along the lines of taking the foundation that I got in my Calculus of Constructions project and see if it can be put on a smaller set theory foundation. I.e., prove it in ZFC, presumably with inaccessible cardinals added.