Post #1846754

@MartinEscardo Yeah, this is a difficult issue... I don't think it is actually realistic for one system to implement the kind of flexibility you are advocating, which is why, I assume, this suggestion has got nowhere so far. There's of course the decades-long graveyard of projects that attempt to implement a logical framework of some kind that can then be instantiated with different type theories, and whereas this approach has been very successful in the world of HOL, I am much more skeptical about its prospects in the world of dependent type theory — whose implementation isn't really modular. Important properties of the system that make implementation both possible and efficient are not easily abstracted over. For better or for worse, a single proof assistant must implement just a single type theory well. This is why the matter of *neutrality* that you have been raising for a long time is so important: if a good system must implement just one type theory at a time, then it needs to be a neutral enough type theory that people can use it to do a variety of things.