> Also, since they're provably correct the "maintenance" metaphor is no longer applicable.

If you want your software to never change, then sure, a proof of correctness is enough. But I've yet to see a piece of software that is both relevant and never has to adapt to new requirements.