[Agda] Why dependent type theory?

[Gabriel Scherer]

In this nice quote, foundations are considered from the perspective of
expressive power:
  What if we find mathematics that *cannot* be formalized with our choice
of foundations?
In our experience with proof assistants, the discussion is generally not
about expressive power (the possibility to formalize something at all) but
about convenience, which in practice determines feasability:
  What if we find mathematics that cannot be formalized *in practice* by
our proof assistant, due to our choice of foundations?

It is not obvious to me whether this impact of foundations on practical
usability of proof assistants is going to stay, or whether it is a problem
of youth that will go away as we develop better assistants. I would rather
hope the latter: that we can build proof assistants that are flexible
enough to conveniently support a very broad range of mathematics.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200309/4a9eb0f2/attachment.html>