Without doubt we should attempt to include constructivists and other philosophies of mathematics, and this does mean that the base logic will have to be pretty simple. This could be further weakened to be essentially first-order, but admitting bound function variables in order to handle axiom schemes and descriptions. Mathematics done in simple base logics is not encrypted at all. If we are to support several different schools of mathematics, then there is the risk that the database will contain many duplicated proofs. This certainly happens with Isabelle.
Much work needs to be done towards relating proofs done in different formal systems.