<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">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">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">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>