Lambda the Ultimate

Recently there has been some interest in the role formal proof and experimental/statistical evidence to show claims of usefulness in programming language papers. On the one hand, formal proofs often prove properties that are widely believed to be correlated with usefulness (such as type system soundness proofs). Experimental evidence is hard to come by, sometimes unreasonably so for papers introducing something new, especially if the something under study has a long learning curve. On the other hand, the end users of PLT efforts are humans (programmers). Humans are complex and we cannot hope for formal proof that something is actually useful.

This got me thinking about why the usefulness of things developed in papers often seems doubtful, despite formal proofs. Type system papers have lots of formal proofs that prove useful properties like soundness. FRP papers have proofs or derivations that an implementation implements a formal model. Papers introducing new programming constructs have proofs. Why is it that after reading such papers it's unclear that the results are actually useful? Because for every type system that is sound and useful, there are hundreds that are sound and not useful. A proof that a (e.g. FRP) system implementation implements a formal model correctly gives confidence in that fact, but not in that the formal model is actually useful. That there are proofs about a programming language construct does not at all imply that the construct is useful.

What would, along with the proofs, give more confidence in the usefulness without requiring as much effort as statistical experiments with users? One possibility is a collection of sample applications. Papers often have a small 5 line toy motivating example but rarely go beyond that. For example the Coherence stuff has a small example of tasks with start length and end. While a system to execute callbacks in a deterministic way could be useful, such a example shows neither the importance of the problem nor the usefulness of the solution beyond reasonable doubt. This was also mentioned on the author's blog. If there was a library of sample applications to go along with the paper, that would. Note that I'm not saying that this is a bad paper at all, just that the level of examples is the same as most other papers.

My question is threefold:

1. Do you think it is useful having a collection of sample applications of the stuff developed in the paper, perhaps in an appendix or on the paper's website?
2. Which existing papers already had this?
3. What are good example applications for each different domain? For example an email client or a todo list application for UI papers such as Coherence or FRP, and perhaps a Javascript parser for papers investigating new parser technology papers such as Yacc is dead and OMeta.