cf. interactive discussion

Dear authors,

I am delighted to accept your manuscript, conditional to a few technical corrections / clarifications which are detailed below. Thank you for having considered Earth System Dynamics to publish your work, and I am certainly waiting for the continued developments of dependent-type programming applications of decision theory.

- p. 3, l.26 : p. 2 l. 21: use "\citep" (bracket references) where needed. Check manuscript throughout

- p. 11, l.29 : "But notice that, as discovered by Ionescu (2009) 30 in the context of vulnerability studies, measures that pick up the most (least) probable Val -value of a probability distribution do violate the monotonicity condition" -> If the Ionescu thesis available online? If not, you might need to give a bit more detail. I tried to find a counterexample (of most-probable Val violating monotonicity) and, at least in a few minutes, I couldn't find any. Is there any simple counterexample you could give?

- p. 4., l, 21: programmes machine checked to be correct. This seems to be a central notion, but the average reader will need to undrestand better in what sense the programme is checked to be 'correct'. What does 'correct' mean in this context?

- p. 4, l 18 : specificy the meaning of the \sqsubseteq symbol. I do not understand why in this case we can't simply use $\leq$ (see also p. 26 l. 13). Is this is a generalisaton of $\leq$ for arbitrary defined order relations?