<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">
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.
<div><br>
</div>
<div>Cheers,</div>
<div>Gerwin<br id="lineBreakAtBeginningOfMessage">
<div><br>
<blockquote type="cite">
<div>Begin forwarded message:</div>
<br class="Apple-interchange-newline">
<div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;">
<span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif; color:rgba(0, 0, 0, 1.0);"><b>From:
</b></span><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif;">June Andronick <june.andronick@proofcraft.systems><br>
</span></div>
<div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;">
<span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif; color:rgba(0, 0, 0, 1.0);"><b>Subject:
</b></span><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif;"><b>Re: An Isabelle Foundation?</b><br>
</span></div>
<div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;">
<span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif; color:rgba(0, 0, 0, 1.0);"><b>Date:
</b></span><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif;">11 January 2025 at 02:09:38 AEDT<br>
</span></div>
<div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;">
<span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif; color:rgba(0, 0, 0, 1.0);"><b>To:
</b></span><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif;">Lawrence Paulson <lp15@cam.ac.uk><br>
</span></div>
<div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;">
<span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif; color:rgba(0, 0, 0, 1.0);"><b>Cc:
</b></span><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif;">isabelle-dev <isabelle-dev@in.tum.de>, Fabian Huch <huch@in.tum.de>, Andrei Popescu <andrei.h.popescu@gmail.com>, Dmitriy Traytel <traytel@di.ku.dk>, Manuel Eberl
<eberlm@in.tum.de>, Gerwin Klein <kleing@unsw.edu.au>, Chelsea L Edmonds <C.L.Edmonds@sheffield.ac.uk>, Christian Urban <christian.urban@kcl.ac.uk>, Mohammad Abdulaziz <mohammad.abdulaziz8@gmail.com>, AFP Submit <afp-submit@in.tum.de>, "Peter Lammich" <lammich@in.tum.de>,
Jim Grundy <jmgruj@amazon.com>, "Mulligan, Dominic" <dommul@amazon.co.uk>, Norbert Schirmer <nschirmer@apple.com><br>
</span></div>
<br>
<div>
<div>Thanks Larry.<br>
<br>
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.<br>
<br>
Cheers<br>
June<br>
<br>
<blockquote type="cite">On 10 Jan 2025, at 15:16, Lawrence Paulson <lp15@cam.ac.uk> wrote:<br>
<br>
Dear colleagues, <br>
<br>
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.<br>
<br>
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.<br>
<br>
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.<br>
<br>
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.<br>
<br>
Larry<br>
<br>
</blockquote>
<br>
</div>
</div>
</blockquote>
</div>
<br>
</div>
</body>
</html>