The Coq mailing list

[Martin Escardo <m.escardo AT cs.bham.ac.uk>]

In other words, choose your proof assistant as a function of what you 
want to talk about *and* how you want to talk about it. Martin

On 06/03/2020 21:05, Martin Escardo wrote:
> The troubling aspect of proof assistants is that they not only implement 
> proof checking (and definition checking, construction checking etc.) but 
> that also that each of them proposes a new foundation of mathematics.
>
> Which is sometimes not precisely specified, as it is the case of e.g. 
> Agda. (Which is why I, as an Agda user, I confine myself to a 
> well-understood subset of Agda corresponding to a (particular) 
> well-understood type theory.
>
> For mathematically minded users of proof assistants, like myself, this 
> is a problem. We are not interested in formal proofs per se. We are 
> interested in what we are talking about, with rigorously stated 
> assumptions about our universe of discourse.
>
> Best,
> Martin
>
> On 06/03/2020 17:39, James McKinna wrote:
> > Jason Gross, on Tue, 03 Mar 2020, you wrote:
> >
> > > So I'm asking these mailing lists: why do we base proof assistants on
> > > dependent type theory?  What are the trade-offs involved?
> > > I'm interested both in explanations and arguments given on list, as 
> > > well as
> > > in references to papers that discuss these sorts of choices.
> >
> > Jason,
> >
> > With apologies to Richard Hamilton, to paraphrase your question:
> >
> >    "just what is it about dependent type theory which makes today's 
> > proof assistants so different, so appealing?" (*)
> >
> > It's a great question, and lots of people, quite naturally, have 
> > replied with lots of competing/overlapping answers. I'd like to open 
> > out the discussion a bit, conscious that in doing so, Jeremy or others 
> > may wish to pull rank on history/philosophy of mathematics/science..., 
> > and aware that it might not find favour with all readers of these lists.
> >
> > TL:DR:
> >
> > -- the Kolmogorov (1931) 'Aufgabe' interpretation of intuitionistic 
> > logic (**), predating 'formulae-as-types' by 30--40 years;
> >
> > -- times (and Kuhnian paradigms) change; so does mathematics, and with 
> > it, mathematicians (or perhaps better: vice versa); with apologies to 
> > the Wiener Secession (***), "Der Zeit, ihre Mathematik; der 
> > Mathematik, ihre Freiheit";
> >
> > -- what is a proof assistant for, anyway? if you ask that question, 
> > you might find how/why the answer biases towards (or away from!) a 
> > particular foundation;
> >
> > -- what is it about dependent type theory, anyway? Thorsten and 
> > Jeremy, among others, have made excellent points in this regard: the 
> > benefits of parametrised/indexed typing, type inference (esp. wrt 
> > implicit arguments, and (algebraic) structure), to which I would add: 
> > the analysis of equality, the distinction between theorem-proving for 
> > well-formedness vs. 'salient' proofs, and the observation that 
> > (although nowhere does it seem that de Bruijn actually ever said this 
> > in the collected Automath) "the ordinary language of mathematics is 
> > intrinsically dependently typed";
> >
> > -- with a nod to Freek and Josef, "what might it be about 
> > (Tarski-Grothendieck) set theory which makes yesterday's proof 
> > assistant (Mizar), or tomorrow's (Egal) so appealing?" In particular, 
> > the ability of each those systems to support the kind of fine-grained 
> > typing supported by "type-theory-based proof assistants", 
> > simultaneously with set-theoretic/uni-typed foundations...
> >
> > More anon, I hope,
> >
> > James McKinna
> >
> > (*)https://en.wikipedia.org/wiki/Just_what_is_it_that_makes_today%27s_homes_so_different,_so_appealing%3F 
> >
> >
> > (**)http://homepages.inf.ed.ac.uk/jmckinna/kolmogorov-1932.pdf
> >
> > (***)https://en.wikipedia.org/wiki/Vienna_Secession

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe