This seems like a misunderstanding / not my intent. (Could you maybe quote the part that gave you this impression?)
I believe Dusan was trying to say that davidad’s agenda limits the planner AI to only writing provable mathematical solutions. To expand, I believe that compared to what you briefly describe, the idea in davidad’s agenda is that you don’t try to build a planner that’s definitely inner aligned, you simply have a formal verification system that ~guarantees what effects a plan will and won’t have if implemented.
I believe Dusan was trying to say that davidad’s agenda limits the planner AI to only writing provable mathematical solutions. To expand, I believe that compared to what you briefly describe, the idea in davidad’s agenda is that you don’t try to build a planner that’s definitely inner aligned, you simply have a formal verification system that ~guarantees what effects a plan will and won’t have if implemented.