[Agda] Why dependent type theory?

[Martin Escardo]

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