[Agda] An article by Jean-Yves Girard

[Andreas Abel]

Well Girard is a genius, and myriades of researchers have tried to 
understand his ideas (e.g. the whole Geometry of Interaction community).

Understanding Girard's papers is not any easier that reading medieval 
treatises on alchemy:  The uninitiated ones (like us) need an interpreter.

On 2020-04-21 22:06, Philippe de Rochambeau wrote:
> 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
> 
> 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 
>> <mailto: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
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>