From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.0.20 with SMTP id 20mr2021754lja.9.1465820090508; Mon, 13 Jun 2016 05:14:50 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.71.75 with SMTP id u72ls66249lja.35.gmail; Mon, 13 Jun 2016 05:14:49 -0700 (PDT) X-Received: by 10.25.201.129 with SMTP id z123mr159560lff.10.1465820089767; Mon, 13 Jun 2016 05:14:49 -0700 (PDT) Return-Path: Received: from mail-wm0-x22e.google.com (mail-wm0-x22e.google.com. [2a00:1450:400c:c09::22e]) by gmr-mx.google.com with ESMTPS id c135si176075wme.2.2016.06.13.05.14.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 13 Jun 2016 05:14:49 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2a00:1450:400c:c09::22e as permitted sender) client-ip=2a00:1450:400c:c09::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2a00:1450:400c:c09::22e as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-wm0-x22e.google.com with SMTP id m124so76409471wme.1 for ; Mon, 13 Jun 2016 05:14:49 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=f1W4ZdYjbTODPOj6BVOX9F4l5c+wIU37E6b/Pvpy4rE=; b=yWAa2o+C0/dRZiFHEMGKBV4h8SmvID/lSHCp0ZzXKOG0029QJAlkHh+5SL5XRpZQca AU4WgisBsQrH7DhYncQ9dwuee2tGzPV+xMwuVJZT+Ne2LwU+qe5VxaU3GD9oYkpgUy+I jYBVuFzrCJyIq6tVdROV0W5HBKWGNfWt/CLZW6lUFGWDD2nlo+S6Y14GczpPlW9SKc0Y Pd1f9Xjb4IZmJHpHH2xt7Ck7bJbjAlkFP+he/9/I05xawr3GhOUyIYp/dWYUyfxb6K32 2287IA9ZFg44UrGzhEsGsgLP11yxFq3hVC8SFgWxtIPksyF6WV/JFCBP6TxQ4kDEUdyL tiYQ== X-Gm-Message-State: ALyK8tIabsiYxA8T4sNU/ajgD+eJI5ByLJSHUxqxH4FRNCEUvMdDIEAIxj/vVY0WlSVTFDjy24PSLyXj8FdXdA== X-Received: by 10.194.238.234 with SMTP id vn10mr812801wjc.127.1465820089405; Mon, 13 Jun 2016 05:14:49 -0700 (PDT) MIME-Version: 1.0 Received: by 10.194.143.38 with HTTP; Mon, 13 Jun 2016 05:14:29 -0700 (PDT) In-Reply-To: References: From: Bas Spitters Date: Mon, 13 Jun 2016 14:14:29 +0200 Message-ID: Subject: Re: [HoTT] How to make software without money To: Vladimir Voevodsky , Jeremy Avigad Cc: James Cheney , Andrej Bauer , "HomotopyT...@googlegroups.com" , Vladimir Voevodsky Content-Type: text/plain; charset=UTF-8 Regarding proof assistants in teaching, let me mention the very nice work by Jeremy Avigad: https://avigad.github.io/logic_and_proof/ On Mon, Jun 13, 2016 at 2:00 PM, Vladimir Voevodsky wrote: > I think the key step that needs to be done is to start to teach mathematics > using proof assistants similarly to how the Software Foundation initiative > does it for programming languages. > > It may be at first a graduate course in constructive mathematics e.g. in > constructive algebra. > > Due to the way the motivational structure of mathematical learning is > organized it would be very good and may even be necessary for such a course > to succeed to have several unsolved *conjectures* or *problems* to attract > students. > > I know of one such problem - to find a constructive proof of > Merkurjev-Suslin theorem about K_2/l . Constructive here might mean simply a > proof that does not use the axiom of choice but I believe that to find such > a proof one has to learn real constructive algebra such as the constructive > description of the algebraic closure of a field (one can assume that it has > decidable equality). > > I also believe that finding a constructive proof pf this theorem will open > the way to the correct formulation and proofs of many questions related to > the structure of Galois cohomology that we at the moment have no idea how to > approach. > > I have a feeling that there are also many such questions in number theory > where having a constructive proof would mean achieving a much higher level > of understanding of the structures involved and ultimately to the solutions > of problems that are open in classical mathematics. > > Vladimir. > > > > > > > On Jun 12, 2016, at 4:20 PM, James Cheney wrote: > > Hi Andrej, > > This is a problem in many scientific disciplines, not just (formalized) > mathematics. It is beginning to be understood that software development and > maintenance needs to be recognized as a scholarly activity in order to make > it more likely that software needed to reproduce and understand research > results is available and preserved > > https://figshare.com/articles/There_s_No_Such_Thing_As_Irreproducible_Research_Software_Credit_Edition_/3159295/1 > > and in the UK at least, the Software Sustainability Institute is trying to > support scientists in a range of disciplines to develop better software: > > http://software.ac.uk/ > > Also in the UK, the Alan Turing Institute is supporting "research software > engineers" whose job it will be to turn promising researchware developed by > ATI fellows/students into reusable/documented/tested packages. So far it > seems that the powers that be view the ATI as primarily about big data and > machine learning, though. The UK has no analogue to INRIA, nor the US as > far as I know; I think the closest analogues are the national labs but (at > least w.r.t verification and formalized mathematics) they are much less > visible than INRIA. > > It would be great to put the problems of formalized mathematics in the > picture for such organizations. > > In addition to the recent Coq-related efforts mentioned by others, one > should consider the Isabelle/HOL and ACL2 communities. Isabelle/HOL does get > used in industry, e.g. NICTA/Data61's formalization of sel4 kernel. See > talks by J Moore on ACL2 and by Gerwin Klein on sel4 at the recent Royal > Society discussion meeting on "verified trustworthy software systems" > > https://royalsociety.org/events/2016/04/software-systems/ > > There are also (relative) success stories in mathematics, e.g. the GAP > system: > > www.gap-system.org/ > > None of this is to say that software credit and maintenance (and development > to the level of maturity needed for acceptance in the mathematical > community) is a solved problem, but there are other solution attempts that > can be considered to better understand the problem. Fundamentally, what is > needed is resources, whether this means money from funding agencies, > investment capital, or donations of free time from open source contributors. > In each case, persuasion and leadership is needed, but what form this takes > seems very situation-dependent and there is no guarantee that the needed > model will fit anyone's pre-existing vision of a "successful [academic] > career". > > --James > > PS. I also enjoyed the comic. > > > On Sun, Jun 12, 2016 at 9:28 AM, Andrej Bauer > wrote: >> >> On Sun, Jun 12, 2016 at 10:04 AM, Andrej Bauer >> wrote: >> > http://www.smbc-comics.com/index.php?id=4127 >> >> And now for something completely different: >> http://wstein.org/talks/2016-06-sage-bp/bp.pdf >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.