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

[Karl Crary]

Hi Adam,

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.

    -- Karl


Adam Chlipala wrote:
> I found this code online at
>     http://www.score.is.tsukuba.ac.jp/~minamide/verification.html
>
> It looks like the development is at least twice as long as mine 
> lines-of-code wise, at 632 vs. 238.  I wasn't sure at a glance how to 
> calculate a fair backwards slice of required developments, so I counted 
> Lt.thy and Plotkin.thy.  It uses a smaller (and untyped, as far as I can 
> tell) source language, omitting a base type and products.  The proofs 
> seem significantly more manual and hard to understand.  Perhaps an 
> Isabelle expert could tell me if I'm just being unfair here. :-)
>
>