[Agda] Why dependent type theory?

[Martin Escardo]

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