[Agda] An article by Jean-Yves Girard

[Philippe de Rochambeau]

Hi all,

this discussion has been going round in loops for the past two days about about a very tiny part of Girard’s Logique 2.0 article: the abstract and the first paragraph of a 27-page article. We’ve talked about snakes, and mustard watches, and a bit about topos theory,  mostly based on the superficial interpretation of the article’s « cover » , to paraphrase an old English saying. Then Xuanrui cried out: « give Girard a chance! », just like the child in Andersen’s tale.

I’m not a specialist in anything, and even less a school-master giving lectures, but I believe that it's worth reading at least one of Girard’s articles (in English) in your lifetime, even if you only understand 20% of it, especially if you are interested in logic and programming.

Furthermore, if Abadi and Hindley and probably many other researchers worldwide, have quoted him over the past decades, this guy’s must have interesting things to say.

https://girard.perso.math.cnrs.fr/Accueil.html <https://girard.perso.math.cnrs.fr/Accueil.html>

Cheers and no bad feelings,

Philippe

PS if you read the article about Mustard Clocks, which is available on his Homepage, please don’t interpret it at first degree :-)


> Le 21 avr. 2020 à 21:13, Martin Escardo <m.escardo at cs.bham.ac.uk> a écrit :
> 
> 
> 
> On 21/04/2020 14:24, mechvel at scico.botik.ru <mailto:mechvel at scico.botik.ru> wrote:
>> On 2020-04-21 15:54, Xuanrui Qi wrote:
>>>> The result was that simple notions
>>>> and proofs were reformulated in a complex way, and the proofs have
>>>> become many times larger and many times more complex.
>>> 
>>> I'm afraid many people on this list would not agree with this
>>> statement. From what little I know about topos theory, many proofs can
>>> be greatly simplified using topos theory. Ingo Blechschmidt, for
>>> example, used topos theory to simplify many proofs in algebraic
>>> geometry [1]. Ingo himself might be on this list, so I won't say too
>>> much about his work. But this is a divergence.
>> I just transfer the opinion of a certain expert in logic who is aware of the topos
>> approach. He referred this way to a certain dissertation. This was in about 1995.
> 
> One should avoid giving opinions about things one doesn't understand. In particular, one should avoid transferring opinions.
> 
> Toposes are very nice and elegant and useful and precisely explained in the literature, so that if you want to understand them, you can. I have used them and I will continue to do so.
> 
> I am not sure about mustard watches, but then I am not an expert and hence I refrain from giving an opinion. However, I do agree that the abstract and the introduction of the given article in this thread don't give enlightening explanations. And this is part of the reason I am not an expert on this subject - whenever I try to have a go at it, I don't get anywhere by reading the published work - perhaps you need to be initiated in person to be able to grasp it - or perhaps I just didn't get it and it is my fault, which I don't discard as a possibility.
> 
> Best,
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200421/a855acf9/attachment.html>