We must fund intellectual infrastructure for the long term › Funding intellectual infrastructure using research grants [013H]

In a traditional research grant proposal, one describes a scientific vision instrumented by several key deliverables that can be achieved in anywhere from the space of a year to several years.

There are three main problems with research grants as far as the funding of intellectual infrastructure.

Problem 1. Inadequate timescale of research grants [013J]

Research grants are usually time-limited (for example, five years tends to be on the longer side for grants), whereas the sustainable intellectual infrastructure that can actually be safely adopted in critical areas must be funded stably on the scale of decades rather than years.

Problem 2. Unquantified impact of intellectual infrastructure [013K]

Funding is, as a rule, devoted to projects that promise (1) significant and (2) essentially predictable intellectual contributions. Intellectual infrastructure typically does not yield a direct intellectual contribution, but when neglected for too long can impede these intellectual contributions in invisible ways. Funders of research grants are, however, reluctant to fund what they cannot quantify.

Problem 3. “implicit” production of intellectual infrastructure [013L]

Because intellectual infrastructure is nearly always developed by a combination of volunteer labour and student labour, funders are reluctant to devote resources to what they anticipate will be done anyway without their intervention—or, given that many PhD studentships are sponsored by such bodies, there may be a perception that the existing model is already adequately funding the production of intellectual infrastructure.

Context

    We must fund intellectual infrastructure for the long term [013G]

    How can we effectively and sustainably fund the intellectual infrastructure for generational human advancement? Intellectual infrastructure—which I would define to encompass the tools used to develop, teach, and learn science—is mistreated by essentially all extant funding models that I am aware of.

    To be clear, when I speak of “tools” I mean not only software (like Lean, Coq/Rocq, Agda, Isabelle, Forester, SageMath, or Mathematica)—but also more broadly intellectual tools like the nLab and The Stacks project whose main aim is not necessarily to contribute new ideas but to consolidate what is known in order to lay the groundwork for the future.

    Funding intellectual infrastructure using research grants [013H]

    In a traditional research grant proposal, one describes a scientific vision instrumented by several key deliverables that can be achieved in anywhere from the space of a year to several years.

    There are three main problems with research grants as far as the funding of intellectual infrastructure.

    Problem. Inadequate timescale of research grants [013J]

    Research grants are usually time-limited (for example, five years tends to be on the longer side for grants), whereas the sustainable intellectual infrastructure that can actually be safely adopted in critical areas must be funded stably on the scale of decades rather than years.

    Problem. Unquantified impact of intellectual infrastructure [013K]

    Funding is, as a rule, devoted to projects that promise (1) significant and (2) essentially predictable intellectual contributions. Intellectual infrastructure typically does not yield a direct intellectual contribution, but when neglected for too long can impede these intellectual contributions in invisible ways. Funders of research grants are, however, reluctant to fund what they cannot quantify.

    Problem. “implicit” production of intellectual infrastructure [013L]

    Because intellectual infrastructure is nearly always developed by a combination of volunteer labour and student labour, funders are reluctant to devote resources to what they anticipate will be done anyway without their intervention—or, given that many PhD studentships are sponsored by such bodies, there may be a perception that the existing model is already adequately funding the production of intellectual infrastructure.

    Funding intellectual infrastructure on the FRO model [013I]

    An interesting and encouraging development is the emergence of the Focused Research Organisation model, which recognises and aims to solve Problem [013K] and Problem [013L]. For example, the most excellent Lean Focused Research Organization describes their mission as follows:

    We are excited to share the news of the Lean Focused Research Organization (FRO)! A new nonprofit dedicated to advancing the Formal Mathematics revolution, we aim to tackle the challenges of scalability, usability, and proof automation in the Lean proof assistant. Our 5-year mission is to empower Lean towards self-sustainability. Please check our current roadmap for details. (Lean FRO, Mission)

    I think that this is a great development indeed, and it will be good for Lean and therefore good for our community. But I think that the FRO model cannot address Problem [013J]—the inadequate timescale. Even the reference to “self-sustainability” in the Lean FRO mission statement suggests an assumption that there is anything “self-sustaining” whatsoever about the infrastructure that makes scientific and intellectual progress possible.

    It is one thing (a very good thing indeed) to solve usability problems and address pain points that prevent institutional and industrial adoption of intellectual tools in the near term. I have every reason to believe that the Lean FRO will be be very successful in this area (and they have made great strides already). An FRO naturally does not aim to solve all problems, and we should certainly not judge them on that unrealistic basis; but we should use the experience to better understand where the gaps are in our current models for the funding and production of intellectual infrastructure.

    Problems with the bimodal theory/practice cycle [013M]

    The bimodal “practice—then theory—then practice” model presupposed by the dichotomy between traditional research grants and focused research organisations and other short-term “moon-shots” neglects the dialectical interplay between theory and practice, in ways that can have real consequences for human intellectual advancement. Indeed, it seems to me that the model of dividing funding between traditional research grants and FROs is based on the idea that progress occurs in a two step cycle:

    1. First the “real science” reaches the point where it is strong enough that it could be applied in a practical way, but this application would be impossible to achieve within the research grant funding model.
    2. So an FRO is spun up to pick up where the science left off, and develop the application to the point that it can be practically adopted in institutions and industry.
    3. (Repeat!)

    I do not think that the cycle above can lead to sustainable intellectual infrastructure, which requires (1) a more responsive interplay between theory and practice, and (2) long-term continuity of lessons and advances that cannot be achieved on the current model of “once or twice per decade post-mortems” in the form of successive research grant and FRO proposals.

    Unsustainable tool enhancement is a barrier to progress [013N]

    I am going to say something strange, and I hope that I will not be misunderstood.

    By concentrating an immense amount of funding into “developing the application” without regard for the evolving theoretical basis and sustaining the development over a timescale of decades, we can unintentionally and disastrously raise the bar for high-impact advances by increasing product inertia in unsustainable ways. For example, I would estimate that it costs upwards of £1–2M to create an excellent IDE—so when a five year program results in an excellent IDE for a specific language along the understandably narrow mission of an FRO, the funders may have unintentionally raised the financial baseline for any future transformative impact by at least £1M.

    We do not need to make any guesses or conjectures as to whether increased inertia is a likely outcome of these new funding models—as this has already occurred, incontrovertibly, as a consequence of the existing industrial-adoption-based model of production of programming languages, where a large corporation can put millions of funding into a language of relatively low quality (and thus raise significantly the usability of the tooling) to the point that making a competently designed language meet the minimum standard for adoption would cost far more than is possible to fund on the academic model.

    Obviously the solution to this problem is not to slow the march of tool enhancement—quite the opposite. But we must find a way to achieve these enhancements without making future improvements of a more radical nature prohibitively expensive. I think that the key to unlocking the long-term sustainability of intellectual tool enhancement to develop a unified and responsive theory/practice funding model that can exercise leadership on the scale of decades.

    A call to action for a sustainable theory/practice spiral [013O]

    I am calling for the endowment and funding of independent research institutions on a permanent or decades-long basis, whose mission is not bound to a specific tool (e.g. Lean or Coq or Forester) but rather to a set of scientific principles and society-level goals to be achieved on a generational timescale.

    It may seem as though open-ended endowments of this kind are a pipedream, but I would draw your attention to the example of the Hoskinson Center for Formal Mathematics at Carnegie Mellon University established in 2021 by a gift from billionaire Charles Hoskinson; although the Center is mainly focused on Lean, I see no reason why institutions of this nature could not be endowed on a permanent basis with a broader technical approach.

    For future endowments, it will be important to place an emphasis on the funding of permanent staff over the funding of research students and postdocs—whose near-term career needs are often in deep and irreconcilable conflict with the mission of an institution that aims to make generational social impact. If you have resources that could be brought to bear on such an ambitious project, or are connected with someone who does, please get in touch with me (js2878@cl.cam.ac.uk). It is time for us to build and sustain the scaffolding for the next three centuries of Science.

    Acknowledgments [013P]

    My sincere thanks to Johan Commelin for his comments and encouragement.

    Backlinks

      We must fund intellectual infrastructure for the long term › Problems with the bimodal theory/practice cycle [013M]

      The bimodal “practice—then theory—then practice” model presupposed by the dichotomy between traditional research grants and focused research organisations and other short-term “moon-shots” neglects the dialectical interplay between theory and practice, in ways that can have real consequences for human intellectual advancement. Indeed, it seems to me that the model of dividing funding between traditional research grants and FROs is based on the idea that progress occurs in a two step cycle:

      1. First the “real science” reaches the point where it is strong enough that it could be applied in a practical way, but this application would be impossible to achieve within the research grant funding model.
      2. So an FRO is spun up to pick up where the science left off, and develop the application to the point that it can be practically adopted in institutions and industry.
      3. (Repeat!)

      I do not think that the cycle above can lead to sustainable intellectual infrastructure, which requires (1) a more responsive interplay between theory and practice, and (2) long-term continuity of lessons and advances that cannot be achieved on the current model of “once or twice per decade post-mortems” in the form of successive research grant and FRO proposals.