<div dir="ltr">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:<div><br></div><div>  <a href="https://www.sciencedirect.com/science/article/pii/0890540188900053">https://www.sciencedirect.com/science/article/pii/0890540188900053</a></div><div><br></div><div>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:</div><div><br></div><div>  <a href="https://www.google.com/books/edition/Selected_Papers_on_Automath/6pObdqwF0coC">https://www.google.com/books/edition/Selected_Papers_on_Automath/6pObdqwF0coC</a></div><div><br></div><div>It's nice to have the opportunity to call attention to these important sources.</div><div><br></div><div>Best wishes,</div><div><br></div><div>Jeremy</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Mar 9, 2020 at 8:55 PM Jeremy Avigad <<a href="mailto:avigad@cmu.edu">avigad@cmu.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Friends, <div><br></div><div>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: <a href="https://dl.acm.org/doi/10.1145/263699.263742" target="_blank">https://dl.acm.org/doi/10.1145/263699.263742</a>. The Pollack article is here: <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.7361" target="_blank">http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.7361</a>.</div><div><br></div><div>I feel bad for disseminating false history! I will correct the footnote in the arXiv version of the survey.</div><div><br></div><div>Best wishes,</div><div><br></div><div>Jeremy</div><div><br></div><div>  </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Mar 9, 2020 at 2:30 AM Gabriel Scherer <<a href="mailto:gabriel.scherer@gmail.com" target="_blank">gabriel.scherer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>In this nice quote, foundations are considered from the perspective of expressive power:</div><div>  What if we find mathematics that *cannot* be formalized with our choice of foundations?</div><div>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:</div><div>  What if we find mathematics that cannot be formalized *in practice* by our proof assistant, due to our choice of foundations?</div><div><br></div><div>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.<br></div></div>
</blockquote></div>
</blockquote></div>