[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Daniel C. Wang]

I think, you make some good points. I think you should think about  how 
you can turn your concerns into some micro-challenges.
There's no point to in doing a "real" proof which exercises many other 
issues besides the one you think are the real issues.
Once you've actually done a  formal proof for a real proof you always 
have a set of issues that made the proof more tedious than it needed to 
be. Distilling those issue into some micro-challenges I think gives you 
insight into the problem.

The first poplmark ought to have given people enough experience to 
develop a set of small challenges that highlight those issues.
I have my own set of pet problems. This one is one of them, because it 
is more tedious than it ought to be in at least one system I know about.

Dimitrios Vytiniotis wrote:
> Hi, here's a small Isabelle/HOL script:
>
>     www.cis.upenn.edu/~dimitriv/poplmark/DWang.thy
>
> I can't say I agree that this example is a good test, in my opinion
> *real* problematic examples, are those where the programmer ends up saying:
>
>  Good God! not a 100th auxiliary lemma about my Stupid binders!!! (1)
>
> and the particular example is way easier. With respect to integration of
> theories of let's say Naturals or co-algebraic types, I believe---but
> have not big experience---that all modern tools are quite good at that
> already, no? Who isn't?
>
> The real issue is of course that of extensibility of a representation
> technique when new types have to be added or new reasoning methods have
> to be used. A representation technique is no good when your 4-lemma
> paper proof has to involve 40 auxiliary formal proofs *each* time you
> want to use your representation. But evaluating that again requires many
> real-world examples as test-cases because for examples in the scale
> of the one Dan proposed we just can't say much (also read: I will never
> reach mental state (1) above).
>
> Best,
> -dimitris
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>