I would venture the proofs are not the real effort in CompCert.
The real effort is to formulate the various systems such that the
proofs become as simple as possible. So 15.77% is minuscule
compared to the total intellectual effort of this project. Your job
is not yet in danger (even in your retirement :-)
But, seriously, sometimes I am worried that too much automation
is a bad thing, because it can mask the flaws in what one is doing.
There are many examples in the study of logics, but let me use
programming instead. Start with your favorite terrible programming language
(Python happens to be a convenient target, or C++). Now, sure, you can
reduce the number of bugs with automatic program analysis, the smarter
the better. But you would nevertheless still be better off in a statically typed
functional language with a decent module system. You prop up something
that would be better left to wither and die.
- Frank