The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hello,

My short answer: dependent type theory is a good compromise to formalize 
"informal reasonings in naive set-theory" with a computer. Because it 
combines two key-features:
- types are values: you can compute on types and for example, define a 
family of types indexed by naturals.
- typechecking remains decidable.

If you compare this to untyped set theory (like promoted by Lamport), 
then membership in set-theory is undecidable, and I do not know whether 
there is a clear notion of computation in the logic...

Regards,

Sylvain.


Le 03/03/2020 à 23:45, Martin Escardo a écrit :
> Dependent types are good for pure mathematics (classical or 
> constructive). They are the natural home to define group, ring, metric 
> space, topological space, poset, lattice, category, etc, and study them. 
> Mathematicians that use(d) dependent types include Voevodsky (in Coq) 
> and Kevin Buzzard (in Lean), among others. Kevin and his team defined, 
> in particular, perfectoid spaces in dependent type theory. Martin
>
> On 03/03/2020 19:43, 
> jasongross9 AT gmail.com
>  wrote:
> > I'm in the process of writing my thesis on proof assistant performance 
> > bottlenecks (with a focus on Coq), and there's a large class of 
> > performance bottlenecks that come from (mis)using the power of 
> > dependent types.  So in writing the introduction, I want to provide 
> > some justification for the design decision of using dependent types, 
> > rather than, say, set theory or classical logic (as in, e.g., 
> > Isabelle/HOL). And the only reasons I can come up with are "it's fun" 
> > and "lots of people do it"
> >
> > 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.
> >
> > Thanks,
> > Jason
> >
> > _______________________________________________
> > Agda mailing list
> > Agda AT lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda

--
Lors de son assemblée générale annuelle le 13/02/2020, le laboratoire 
Verimag a décidé, à l'unanimité des présents, de soutenir la motion du 
CPCN du CNRS sur les "dispositions attendues de la LPPR" du 17 janvier 
2020 (http://www.c3n-cn.fr/attendusLPPR) et de demander:
- la création massive d'emplois statutaires dans l'ESR pour résorber la 
précarité galopante de ces dernières décennies;
- une augmentation forte des crédits de base des laboratoires pour leur 
permettre de faire de la recherche scientifique plutôt que de la 
recherche de financement;
- le retrait du projet de réforme des retraites, qui met en péril le 
principe de solidarité entre générations par l'incertitude sur le niveau 
des pensions.