The Coq mailing list

[Jeremy Avigad <avigad AT cmu.edu>]

I'd like to post a correction to my previous correction regarding the origins of the use of implicit arguments in dependent type theory. In fact, Section 7.2 of the 1985 paper on the Calculus of Inductive Constructions by Thierry Coquand and Gérard Huet gives a very clear presentation of the idea of using implicit arguments:

  https://www.sciencedirect.com/science/article/pii/0890540188900053

Thierry Coquand pointed out to me that Appendix 9 of the thesis of Jutting (1977) describes a system AUT-SYNT that is a variation of Automath with implicit arguments. This appendix is reproduced in the book on Selected Papers on Automath:

  https://www.google.com/books/edition/Selected_Papers_on_Automath/6pObdqwF0coC

It's nice to have the opportunity to call attention to these important sources.

Best wishes,

Jeremy

On Mon, Mar 9, 2020 at 8:55 PM Jeremy Avigad <avigad AT cmu.edu> wrote:

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.