[POPLmark] Comparison of certified code transformations for functional languages?
adamc at cs.berkeley.edu
Sat May 12 17:19:34 EDT 2007
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. ;)
More information about the Poplmark