The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Le mar. 3 mars 2020 à 22:31, Jason Gross <jasongross9 AT gmail.com> a écrit :

> Which bottlenecks are you referring to? Are they intrinsically tied to dependent types, or they are related to the treatment of propositions and equality in systems such as Coq?

The main bottleneck that I'm referring to here (though not the only one of my thesis) is the one that is due to the fact that arbitrary conversion problems can happen during typechecking. 

Deciding equality in math is undecidable anyway, so whatever the
underlying theory (set, types) you will fall short of automating equality

decision. Do you have any clue that this problem is better treated in

other framework than in (dependent) type theory? Or is it simply that

equality problems become much more frequent?

I think DTT has one clear advantage to this respect: it is easy to
draw the line between what you consider as "administrative tasks"

(that you leave to the type checker to check), and what you maintain

on the "needs proof" side. In non dependent theories every computation

is a proof so the frontier between both is imprecise (and may vary from

a mathematician to another).