This is likely true today but it's increasingly false. Massive efforts are already underway to develop tooling and methodology for this purpose. Once completed the applications developed with them will be significantly easier to produce. Also, since they're provably correct the "maintenance" metaphor is no longer applicable. What we need is provably correct code generation for the output of theorem provers like Coq. These tools generate a large portion of the proof automatically. Programs can be inferred directly from proofs using the Curry-Howard Correspondence. Interesting discussion here: http://www.mail-archive.com/sc-l@securecoding.org/msg01278.h...
> 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.
Agreed. When I said "maintenance" I was referring to the continuous post hoc work needed to uphold the original functionality as it encounters the full range of it's potential input.
