Not knocking this, just saying that it is easy to claim improvements if you know there are improvements to be had.

I will quibble a little with their characterization of proofs as being more computationally impractical.

Proof verification is cheap. On a good day it is as cheap as type checking. Type checking being a kind of proof verification. That said writing proofs can be tricky.

I am still figuring out what writing proofs requires. Anything beyond what your type system can express currently requires a different set of tools (Rocq, Lean, etc) than writing asserts and ordinary programs. Plus writing proofs tends to have lots of mundane details that can be tedious to write.

So while I agree proofs seem impractical. I won't agree the reason is computational cost.