The Coq mailing list

[James McKinna <james.mckinna AT ed.ac.uk>]

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


--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.