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

[Adam Chlipala]

Karl Crary wrote:
> I know nothing at all about the development you're looking at, so I 
> can't give you an answer in any case.  However, your question about 
> "fairness" suggests that you're looking to draw some sort of 
> conclusion from these numbers, so I'm curious:  What sort of 
> conclusion are you looking to draw?  You're comparing lines of code in 
> proofs of different results in different systems.  It's hard for me to 
> see that the comparison could tell you much of anything.

I don't think that the fact that it's different systems should matter 
much, modulo standard concerns about measuring code size between 
languages.  The choice of system is as much open to debate as other 
elements of the formalization strategy.  If one system's implementations 
are systematically bulkier, then that suggests a useful conclusion about 
which system to use.

I don't deny that the theorems being proved are different, but they 
aren't enormously different.  Some quantitative comparison seems better 
than pure hand-waving.  It would naturally be better to have 
apples-to-apples comparisons, but the last time I tried to facilitate 
that by suggesting a compilation benchmark problem on this list, no one 
responded with alternate solutions. ;)