[POPLmark] Comparison of certified code transformations for functional languages?
Adam Chlipala
adamc at cs.berkeley.edu
Sat May 12 17:29:10 EDT 2007
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.
More information about the Poplmark
mailing list