Fwd: An Isabelle Foundation?

[Gerwin Klein]

It looks like June's reply hasn't actually made it to the list, so forwarding it here for those who were not otherwise in the recipient list.

Cheers,
Gerwin

Begin forwarded message:

From: June Andronick <june.andronick at proofcraft.systems>
Subject: Re: An Isabelle Foundation?
Date: 11 January 2025 at 02:09:38 AEDT
To: Lawrence Paulson <lp15 at cam.ac.uk>
Cc: isabelle-dev <isabelle-dev at in.tum.de>, Fabian Huch <huch at in.tum.de>, Andrei Popescu <andrei.h.popescu at gmail.com>, Dmitriy Traytel <traytel at di.ku.dk>, Manuel Eberl <eberlm at in.tum.de>, Gerwin Klein <kleing at unsw.edu.au>, Chelsea L Edmonds <C.L.Edmonds at sheffield.ac.uk>, Christian Urban <christian.urban at kcl.ac.uk>, Mohammad Abdulaziz <mohammad.abdulaziz8 at gmail.com>, AFP Submit <afp-submit at in.tum.de>, "Peter Lammich" <lammich at in.tum.de>, Jim Grundy <jmgruj at amazon.com>, "Mulligan, Dominic" <dommul at amazon.co.uk>, Norbert Schirmer <nschirmer at apple.com>

Thanks Larry.

Just a quick clarification for now: going through LF is what we chose to do to launch the seL4 Foundation, but it certainly has its pros and cons, and I don’t recall saying that I’m advising the Isabelle Foundation to necessarily go through the same route. It does help lightening the burden of figuring things out at creation, but it comes with constraints, in particular financially (whereas we didn’t experience being forced to work differently with the user community for instance). I’m happy to share our experience working with LF with interested people.

Cheers
June

On 10 Jan 2025, at 15:16, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

Dear colleagues,

Some of us have been talking about how to keep things going after the recent retirement of Tobias and myself and the withdrawal of resources from Munich. I've even heard a suggestion that Isabelle would not be able to survive for much longer. We should be concerned: not because Isabelle is some lovely old relic but because it represents the state of the art on every dimension. Our main competition is Lean, which for all its popularity is far behind on automation, performance, scalability and legibility, making it unsuited for the kind of large projects that can be tackled in Isabelle. Everyone seems to agree that the solution is to create some sort of foundation such as already exists for Lean, Coq, seL4, etc. Amazon have been pushing for this because of their reliance on Isabelle internally. The point of such a foundation is to attract industrial funds that would help us hire people to complete necessary tasks. We might also be able to attract substantial computing resources.

It's taken months to try to clarify what such a foundation would look like and how it would work. It was June Andronick who, back in October, advised us to go through the Linux Foundation (LF), which they were using to manage the seL4 Foundation. She stressed a key advantage: that they maintain a firewall between funders and developers, assuring the independence of the open source project. We had a meeting with them a couple of months ago and they seemed interested in such a thing going ahead. On the other hand, some of us, notably Makarius and Fabian Huch, had concerns about the LF and would prefer that we created our own independent organisation. Generally these concerns were that the LF would try to dictate policies to us, e.g. that we would be forced to work with the user community differently than now. It's worth remembering that the LF has no power to force us to do anything and their only sanction is to walk away. In essence, their key requirement is simply that we are a bona fide open source project, which we certainly are. Fabian mentioned that he would not want to accept funds for military projects: the LF representative stated that we have the right to exclude certain sectors, giving as an example a video app that excluded the pornography sector.

Whether we go with the LF or not, we need a new host university. Our connections with Munich and Cambridge gave a steady supply of students and postdoctoral researchers, many of whom became key developers. The point of going through the LF or a similar organisation is that it would take on administrative tasks that would be too burdensome for a full-time academic. I hope that possibly one of you would be in a position to head this thing, with no duties apart from being a convenor from time to time, and bringing PhD students in as Tobias did for so many decades. Of course people would continue to apply for research grants as now.

I'm not sure how to organise this discussion. I'm sending this to as many people involved in the development of Isabelle as I could think of, but feel free to share. Perhaps those who are interested in getting involved somehow could reply to me so that I can set up a mailing list.

Larry



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250115/cee12277/attachment.htm>