Taking good decisions at a given point in time requires estimating the consequences of such decisions at later times. In most situations, these consequences are uncertain and taking good decisions requires weighting the odds and the chances of the options at stake.

The math needed for making rational decisions under uncertainty is well understood since about the middle of the last century.

And yet policy advice in matters of climate policy typically relies on the assumption that the evolution of societies, of their economies and hence of the anthropogenic forcing on the climate system can be predicted with certainty.

The possibility that a financial crisis, a pandemic or a war suddenly takes center stage and delays the implementation of measures to avoid unmanageable consequences of climate change is not factored in.

The math that allows to account for uncertainties in climate decisions rigorously is also the key for quantifying how much these decisions do actually matter. This is, in turn, a pre-condition for talking about responsibility and responsibility attribution: nobody shall be held responsible for taking (or for failing to take) actions that do not matter.

But which climate decisions do really matter? Simply accounting for the fact that measures to avoid unmanageable impacts of climate change are often implemented with delays, brings new results to the table.

Among others, it speaks for earlier, more precautionary climate policies, as one would expect. But it also shows that deciding to de-carbonize as soon as possible still pays off even as the chances that decisions are actually implemented become very low. This is, perhaps, more surprising: a "moral" approach - doing the right thing even though the probability of success becomes increasingly small - is rational over a wide range of uncertainties.

Are these findings correct? This question is the "elephant in the room" whenever scientists come up with results that have been obtained by running computer programs.

We can check the methods and the models but which guarantees do we have that the computer programs that run those models are correct? Programs can be tested and careful testing can sometimes show the presence of errors. But testing is not enough to show the absence of programming errors.

The paper is an advance to more rigorous practices. The results that are shown have been obtained with verified programs. We have applied an implementation of Type Theory to write programs that are machine-checked to be correct.

This is the highest level of correctness that computer science can provide today. So far, verified programming has only been adopted in applications that are considered to be too critical (to be allowed) to fail. For example, in security applications.

Thus, this work is also a first application of Type Theory to climate policy research. We hope that our results will inspire other scientist to study and apply similar methods: it's a fascinating journey and it turns out that Type Theory helps both ensuring that the math is done rightly and, perhaps more importantly, understanding what is the right math to do.