[POPLmark] Comparison of certified code transformations for functional languages?

[Adam Chlipala]

Julien Narboux wrote:
> - Minamide's version seems to try to mimic the paper proof (for instance 
> he derives an induction principle to have nice case names which reflect 
> the distinction between terms which are values or not).
>
> IMHO it is fair to say that yours is more automated, but I am not yet 
> convinced it is easier to understand.
>   

Yes, I think I probably used the wrong words for what I had in mind.  
I'm interested in engineering large certified compilers.  In a POPL 
paper, we may be interested in following all of the details of a proof, 
as this may expand our understanding of the problem in a useful way.  
For realistic programming languages, however, I don't expect that we 
want to examine much detail at all; there will just be too much of it.  
All that matters is that 1) the proof is correct, 2) we were able to 
write it cheaply, and 3) we are able to adapt it to changes in the 
theorem statement.  Standard "software engineering" issues come into 
points 2 and 3, but understanding a proof for its own sake doesn't 
factor in, for me.

So, I'll try rephrasing what kind of comparison I would like to have: I 
want quantitative measures of how quickly someone can perform a formal 
certification task using different approaches, and how much additional 
effort is required to adapt developments to changes in theorem 
statements.  Measuring code size doesn't say anything about these 
directly, but I think it's not controversial to say that there's a 
pretty strong relationship.