Post #1846752

2026-04-29 21:30 UTC

@jonmsterling I've been advocating for Agda (in particular) to allow us to choose *which* type theory we want to work with, safely, of course. This is particularly important when I say, in a paper, that I formalized my results (given in mathematical vernacular) in Agda. Of course it is also great to incorporate all sorts of ideas in e.g. Agda, even unsound ones. But the point is that soundness alone doesn't fit my bill. There are all sort of sound systems that are sound alone but unsound when combined. I want a proof assistant that allows me to control what kind of mathematics I am talking about.

Replies (2)

@cbaberle@mathstodon.xyz 2026-04-29 23:21

@MartinEscardo *through gritted teeth* working on it! @jonmsterling

Open ##1846753
@jonmsterling@mathstodon.xyz 2026-04-30 08:11

@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.

Open ##1846754