The Coq mailing list

[Jeremy Avigad <avigad AT cmu.edu>]

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.