From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.248.4 with SMTP id i4mr8861310ywf.20.1465744828177; Sun, 12 Jun 2016 08:20:28 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.140.21.209 with SMTP id 75ls996151qgl.79.gmail; Sun, 12 Jun 2016 08:20:27 -0700 (PDT) X-Received: by 10.140.81.208 with SMTP id f74mr8803348qgd.30.1465744827654; Sun, 12 Jun 2016 08:20:27 -0700 (PDT) Return-Path: Received: from mail-it0-x236.google.com (mail-it0-x236.google.com. [2607:f8b0:4001:c0b::236]) by gmr-mx.google.com with ESMTPS id u4si438877itc.3.2016.06.12.08.20.27 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 12 Jun 2016 08:20:27 -0700 (PDT) Received-SPF: pass (google.com: domain of james....@gmail.com designates 2607:f8b0:4001:c0b::236 as permitted sender) client-ip=2607:f8b0:4001:c0b::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of james....@gmail.com designates 2607:f8b0:4001:c0b::236 as permitted sender) smtp.mailfrom=james....@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-it0-x236.google.com with SMTP id e5so27555048ith.0 for ; Sun, 12 Jun 2016 08:20:27 -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=iHHJi1boDvZT8VdfP98chhEcWyebm5Xbu173JzsNO4U=; b=xv5umNvF7DpR8awlD3A4Wfn8x3e1m+fJCdB0eF7x4To3N3NJctDq6iuiKvRe5Kxl7x yjSoftyDpMxikOW9iyEwyBgMoeCi4g5rY7IEQ8NjfjtFf3FXABiePY6XyJKEhvurwNWC aOUSfS2OffKM+WLZ/dXQfiwy1BtBqoDQC0LI+yKcdcFtsJ6yq87mBdM1oD864vjjWcai h/YRhJRZmZfwXf7b4EovdKpJXc7bHKl1x3Hm4UI6+h53P+9Cr7rAIcGyBq0uNcLRbc95 QZSl0sgjF1+JVCoTzsBh7I/H+eLUwt1PX/XRAXw2cgotbhM9KhUKjkkz768y9uR7uTT9 em5w== X-Gm-Message-State: ALyK8tJCfTjurJR28oszIzjr2qi4hLg1MkR+GP7IK+X9cf23PvQ73j2eeE7Gwjq1imiV530KltADPEtxPFH60w== X-Received: by 10.36.39.199 with SMTP id g190mr10847823ita.53.1465744827346; Sun, 12 Jun 2016 08:20:27 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.21.69 with HTTP; Sun, 12 Jun 2016 08:20:26 -0700 (PDT) In-Reply-To: References: From: James Cheney Date: Sun, 12 Jun 2016 16:20:26 +0100 Message-ID: Subject: Re: [HoTT] Re: How to make software without money To: Andrej Bauer Cc: "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary=001a1147c4bac3f6a70535164fd5 --001a1147c4bac3f6a70535164fd5 Content-Type: text/plain; charset=UTF-8 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. > --001a1147c4bac3f6a70535164fd5 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Hi Andrej,

This is a prob= lem in many scientific disciplines, not just (formalized) mathematics.=C2= =A0 It is beginning to be understood that software development and maintena= nce needs to be recognized as a scholarly activity in order to make it more= likely that software needed to reproduce and understand research results i= s available and preserved

https://figshare.com/articles/There_s_No_Such_Thing_As_Irreproduci= ble_Research_Software_Credit_Edition_/3159295/1

and in the= UK at least, the Software Sustainability Institute is trying to support sc= ientists 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 develop= ed by ATI fellows/students into reusable/documented/tested packages.=C2=A0 = So far it seems that the powers that be view the ATI as primarily about big= data and machine learning, though.=C2=A0 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.=C2=A0

It would be great to put= the problems of formalized mathematics in the picture for such organizatio= ns.

In addition to the recent Coq-related efforts men= tioned by others, one should consider the Isabelle/HOL and ACL2 communities= . Isabelle/HOL does get used in industry, e.g. NICTA/Data61's formaliza= tion of sel4 kernel.=C2=A0 See talks by J Moore on ACL2 and by Gerwin Klein= on sel4 at the recent Royal Society discussion meeting on "verified t= rustworthy 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 n= eeded for acceptance in the mathematical community) is a solved problem, bu= t there are other solution attempts that can be considered to better unders= tand the problem.=C2=A0 Fundamentally, what is needed is resources, whether= this means money from funding agencies, investment capital, or donations o= f free time from open source contributors. In each case, persuasion and lea= dership 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-e= xisting vision of a "successful [academic] career".

--James

PS. I also enjoyed the comic.

=

On Sun, Jun 12, 2016 at 9:28 AM, Andrej Bauer <andrej...@andrej.com> wrote:
On Sun, Jun 12, 2016 = at 10:04 AM, Andrej Bauer <andre= j...@andrej.com> wrote:
> http://www.smbc-comics.com/index.php?id=3D4127

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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTyp= eThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--001a1147c4bac3f6a70535164fd5--