An Isabelle Foundation?

[Lawrence Paulson]

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