This week I submitted a new research grant proposal to the Swedish Research Council (VR) under the Natural and Engineering Sciences call.

This project builds heavily on the foundations we’ve been laying over the last few years: our work on Optimization Under Uncertainty (OptUU) (see also my earlier blog post), dependently typed dimensional analysis (recently accepted for JFP publication), and domain-specific tensor languages (also available on arXiv). It tries to take a major step forward by scaling these algebraically-accountable architectures to high-stakes, continuous domains: specifically, climate policy exploration and fusion plasma disruption simulation.

The proposal outlines three interlocking Work Packages (WPs) aimed at taming the computational curse of dimensionality using functional programming. The work will be carried out in close collaboration with domain experts, including Nicola Botta at the Potsdam Institute for Climate Impact Research (PIK), and the Plasma Theory group here at Chalmers.

If granted, the project will fund a new PhD student position starting in 2027 to help build out these verified DSLs in Agda/Lean/Haskell.

Here is the abstract from the proposal:

Abstract: In high-stakes domains like climate policy and fusion energy, decisions require balancing conflicting objectives under deep uncertainty. Because empirical trial-and-error is often practically impossible or highly risky, we cannot rely on ad hoc modeling; we need software that is mathematically correct by construction. The aim of this project is to develop a formally verified software architecture capable of computing multi-objective optimal control policies while taming the computational curse of dimensionality.

To achieve this, the research combines functional programming with domain expertise. First, we create domain-specific languages that allow researchers to formally describe complex decision problems and uncertainty. Second, we shrink the mathematical search space by embedding physical constraints and structural symmetries—such as dimensional analysis—directly into the code logic. Finally, we scale these rigorous methods to handle real-world simulations, translating our verified models into fast, efficient solvers and safe AI approximations.

By bridging the gap between computer science and complex system control, the project provides domain experts with trustworthy, machine-checkable tools and supports the transition to decarbonized economies with robust methods for accountable decision-making under uncertainty.

It will take until late autumn before we know if it gets funded, but please do get in touch if you find the topic interesting!

If you are interested in the technical details and methodology, you can read the full grant proposal here (PDF).