O Hugo Heberlin acabou de fazer um post muito bacana sobre o Voevodsky numa mailing list sobre Coq... la' vai. [[]], Eduardo
---------- Forwarded message ---------- From: Hugo Herbelin <[email protected]> Date: Sat, Oct 7, 2017 at 1:57 PM Subject: [Coq-Club] Vladimir Voevodsky To: [email protected] Dear all, Many of you already know it: one week ago, something terribly sad happened: Vladimir Voevodsky, Fields medalist and key initiator of the Homotopy Type Theory foundation of mathematics passed away at the age of 51 [1]. His visionary belief in the foundational impact of the types-as-spaces, equality-as-path correspondence [2][3], his Univalence Axiom, and his reconstruction of propositions and sets from a general notion of homotopy levels contributed to provide a new foundational look at type theory, at equality, at extensionality, and at mathematics in general. His vision and driving force contributed to connect communities of mathematicians, logicians, and computer scientists. The various events he co-organized or participated in over the last years fostered a large corpus of new results encompassing the backgrounds of researchers from these communities: higher inductive types, so natural for representing quotients types or for representing the algebraic essence of geometric structures; cubical type theory for both another view at equality based on abstracting over a dimension and for providing a computational content to univalence; and many other ideas and connections who cross-benefited to the fields above. Vladimir Voevodsky discovered Coq in the mid-late 2000. About it, he said: "I started playing with Coq while thinking about the model in Coq of homotopy types and I started to discover that I can do all kinds of things which I was working before without having any foundational investment so to speak and then I came up and I said `ok, here we have a new foundation of mathematics', we can dispose of that theory as a foundational system and do everything in this new foundation" [4]. In Coq, he started the Univalent Foundations formalization [5] about which a school and a workshop is going to be held in December 2017 [6]. The initial version of the Univalent Foundations formalization itself stimulated the development of libraries for Homotopy Type Theory (HoTT) in Coq [7], Agda [8] and Lean [9]. Homotopy Type Theory is at the core of the work of various research teams world-wide. For instance, one of them directly involved in the development of Coq is the Coq-HoTT project [10] which in particular investigates among others the meta-theory and implementation of definitional proof-irrelevance and higher inductive types in the context of Coq. Digressing about higher inductive types, I cannot resist at including one of the first e-mails that Vladimir sent on coq-club, almost exactly 8 years ago, witnessing his typical ingenuous-looking attempts at expressing essential concepts in the context of Coq (see [11] for the full thread): << Is there a way in Coq to make definitions such as: Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 . or Inductive Impl : Type := P1: Prop | P2: Prop | impl: P1 -> P2 . ? V. >> More practically, Vladimir Voevodsky also said about using Coq: "I have a lot of wishes in terms of getting this proof assistant to work better, but at least I don’t have to go home and worry about having made a mistake in my work" [2]. There is indeed a long and wide road ahead for proof assistants. Let's continue implementing our intuitions and dreams: a revolution is on the march at the frontier of computer science, logic, and mathematics, and Vladimir's spirit and endearingly fresh mindset will continue to accompany us. [1] https://www.ias.edu/news/2017/vladimir-voevodsky [2] The Origins and Motivations of Univalent Foundations, https://www.ias.edu/ideas/2014/voevodsky-origins [3] http://smf4.emath.fr/Publications/Gazette/2014/142/smf_gazette_142_87-94.pdf (p.91) [4] http://icm2014seoul.over-blog.com/videos-en-preambule.html (28'45") [5] https://github.com/UniMath/UniMath [6] https://unimath.github.io/bham2017 [7] https://github.com/HoTT/HoTT [8] https://github.com/HoTT/HoTT-Agda [9] https://github.com/leanprover/lean/wiki/HoTT-Library [10] http://coqhott.gforge.inria.fr/ [11] https://sympa.inria.fr/sympa/arc/coq-club/2009-10/msg00025.html -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para postar neste grupo, envie um e-mail para [email protected]. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6g8r4zVFX2dfq29wa%3DKdUY5sMT5p3s7YFV2onePORKiPg%40mail.gmail.com.
