> It’s the only kind of program that can be actually reasoned about.

What do you mean? There are loads of formal reasoning tools that use dynamic allocation, e.g. Lean.