[Agda] [Coq-Club] Why dependent type theory?

[Jeremy Avigad]

Friends,

In a footnote in a survey article I mentioned in this thread, I wrote that
Amrokaine Saibi credited Peter Aczel with the idea of using
implicit arguments in dependent type theory. James McKinna pointed out to
me that I got this wrong: Saibi explicitly credits Randy Pollack for that.
The Saibi article is here: https://dl.acm.org/doi/10.1145/263699.263742.
The Pollack article is here:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.7361.

I feel bad for disseminating false history! I will correct the footnote in
the arXiv version of the survey.

Best wishes,

Jeremy



On Mon, Mar 9, 2020 at 2:30 AM Gabriel Scherer <gabriel.scherer at gmail.com>
wrote:

> 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/d614d6cf/attachment.html>