Re: [HoTT] Re: How to make software without money

[James Cheney <james....@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 3196 bytes --]

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 <andrej...@andrej.com>
wrote:

> On Sun, Jun 12, 2016 at 10:04 AM, Andrej Bauer <andrej...@andrej.com>
> 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.
>

[-- Attachment #2: Type: text/html, Size: 4399 bytes --]