If programs are proofs, then general programming languages correspond to trivialism.

It is not that difficult to write general-purpose functions in total languages like Coq. You just provide the functions with "fuel" to "burn" during computation. You don't have to express all features of interest in the type. But then you cannot rely on automation.

"Programs are proofs" slogan is interesting from yet another point of view. What are the theorems for which a complex program is the simplest proof? There can be multiple such "theorems" ("principal types" property doesn't hold in complex settings).