I see a lot of mention if "dafny" here, is this a language that's getting traction? I'm surprised there's not any examples on their website of real companies using it for real problems.

This looks very interesting area.

Thanks Gwern that seems pretty similar to what I had in mind.

I guess I was thinking that making it precise would be either something like

Only do an action if the probability of success of given the action has been done is 95% or greater and don't do an action if the probability of success doing nothing is 95%.

or,

Make the Utility be 1 if at a defined point the probability of success is 95% or greater and 0 otherwise and just maximise Expected Utility.

I'm not sure how the first proposal is going to come up against either of the problems you mention. Though it does seem to need a definition of inaction and presumably it could fall prey to the 5 and 10 problem or similar.

I guess there might be a general problem with this sort approach in that it won't try to do low impact actions that move from a 50% probability to a 55% probability.

Thanks I didn't have the copy of the book on hand as I was listening on audible.

I assume this won't work, just because the whole thing is a hard problem so a throwaway thought about a solution in a popular press book is unlikely to solve this. I was mainly interested in either why it won't work or why it's hard to make this precise.