How to make software without money

[Andrej Bauer]

Apologies for a slightly off topic post, but I think it is relevant to
many people on this list.

I just looked at some slides by William Stein, the author of Sage (an
open-source alternative to Mathematica) at
http://www.smbc-comics.com/index.php?id=4127

The conclusion is: it's impossible to make good quality software in
academia because there isn't enough money and because making software
doesn't give one any academic credit.

I am afraid formalization of math might fall into the same category,
unless we somehow elevate it to a "true science" level. A great deal
has been done in this respect recently by projects lead by Gonthier,
Hales and Voevodsky, but is it enough? Are we even making a dent?

At my department, for instance, the folk knowledge propagated from one
generation to another is that "someone" formalized "Landau's book" (I
suppose it was the Automath formlaization of Landau's Grundlagen der
Analysis by Jutting) which proves that "it can be done" but is
otherwise an intellectually barren exercise without academic value. I
still remember one of the professors saying this to the whole class
when was an undergraduate.

With kind regards,

Andrej

[Andrej Bauer]

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

[andré hirschowitz]

Hi,

I have been thinking to this issue for years (decades?). In France we have this research agency INRIA which has been supporting the Coq project for decades, leading to a fairly "good quality software" (in my opinion). Say twenty years ago, the Coq project was targetting the computer science community and was not ready to "attack" the mathematical community. From this side, the picture seems much better nowadays.

A possible strategy toward the investment of the mathematical community is as follows:

------------------------

1- create a body tying (part of) this community with for instance (part of) the Coq project (and/or the Agda project, about which I know little).

2- obtain specific funding from a Research Agency (NSF, CNRS?) for partly formalized PhD fellowships, together with companion funding for the technical support (eg from the Coq team) to the (partial) formalization.

3- obtain good applications, coming from ouside this community.

4- select the winning applications regarding both the interest of the naked thesis, and the feasability of the (partial) formalization.

5- help collectively the success of each selected project.

6- Write assessments in particular for the formalization efforts of these newage doctors, so that they win positions whenever they deserve.

---------------------------

I leave it here.

ah

--
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.

[Andrej Bauer]

While the efforts expanded on Coq and Agda are truly impressive and
chivalrous, both pieces of software compare poorly to something like
Mathematica in terms of software quality (documentation, professional
GUI design, technical support, cloud support, etc.) This is not a
criticism of the Coq and Agda teams, just an observation which in
Slovene could be summarized by the phrase "that's the music you get
for the money you paid".

Also, I am not trying to start a war with the lurking Knights of the
Open Source. I am just saying we have no idea how to bring open-source
mathematical software to the level of professional software without
sacrificing the careers of several PhDs and at least one tenured
professor.

With kind regards,

Andrej

[Joyal, André]

Dear Andrej,

I am not an expert in software, but Agda and Coq offer something
that Mathematica and Maple dont have: a calculus of proofs.

Regards,
-André

________________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Andrej Bauer [andrej...@andrej.com]
Sent: Sunday, June 12, 2016 7:05 AM
To: andré hirschowitz
Cc: HomotopyT...@googlegroups.com
Subject: Re: [HoTT] How to make software without money

[Ben Sherman]

I feel that I should mention some recent developments that are relevant to this discussion, at least with respect to Coq.

Firstly, Paul Steckler recently joined MIT. He works full-time, as an engineer, towards improving Coq as a software system for its users (see the job posting here: https://groups.google.com/forum/#!topic/fp-syd/wiff-ks5yVw). I don't know exactly where the funding for his position comes from.

Secondly, Yves Bertot announced earlier this week at the DeepSpec workshop in Princeton (http://deepspec.org/events/) the creation of the Coq Consortium, which will be an organization dedicated to the improvement of Coq as a software system for its users. Industrial and academic institutions can pay an annual fee to the Coq Consortium, which will serve to fund full-time engineers to work on improving the Coq system, and these engineers will prioritize the goals of those who fund them. I think the details are still being worked out. (Again, I am not knowledgable about what funding sources academic institutions can use to pay into the Consortium.)

The goal is that with the Coq Consortium, INRIA researchers will be freed to focus on research-relevant aspects of Coq, and Coq users will be able to use a software system whose quality can only be made possible by the attention of full-time engineers. I am personally hopeful that this strategy will work favorably for all those involved!

[James Cheney]

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.

[Timothy Carstens]

In the computer business, technologies which solve essential problems tend to survive; extensible technologies which solve essential problems tend to grow.

When you look at the largest open source projects, the majority of the actual code tends to come from people working in large companies that depend on the tech stack. Linux, for example, has benefited enormously from IBM's investment of engineering-hours into the project. Ruby on Rails is another example, as are many other web-related frameworks.

The SAGE math environment was a noble effort to displace MAGMA and similar systems, which were benefiting from code contributions from academia, but which remained commercial and not widely available. Later SAGE would evolve to compete with Mathematica and other math suites. Unfortunately, the essential problem being solved was a matter of taste-in-licensing, which is not always essential-enough for a project to take hold.

Coq, Agda, Lean, etc, all solve an essential problem, namely that of providing a theory of higher-order machine-checked proofs. The implementations tend to be extensible, at least for experts. Different segments of the CS and math community are becoming aware of these tools and producing new, impressive artifacts all the time. Overall it's a small community, but it's growing. At the very least, the diversity of artifacts demonstrates that these tools are expressive-enough to be useful in many domains, not just in principle but in practice.

Though it is currently difficult to apply these methods to problems of interest in industry, progress in the field of program logics is real and has lead to real tools (Infer, at least) with real users. The ability to prove properties of programs inevitably leads to the desire to prove properties of fairly technical programs, and in that way a bridge to more abstract, less-computery branches of math will emerge. An ecosystem will form, and pure research which contributes to this ecosystem will begin to take on its own appeal. Other paths to industry-awareness may exist, this is just the one I've been tracking.

In my opinion, patience will be rewarded.

-t

[Vladimir Voevodsky]

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.

[Bas Spitters]

Regarding proof assistants in teaching, let me mention the very nice
work by Jeremy Avigad:
https://avigad.github.io/logic_and_proof/