User loginNavigation 
Sample applications for programming languagesRecently 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:
By Jules Jacobs at 20110917 13:38  LtU Forum  previous forum topic  next forum topic  other blogs  7406 reads

Browse archivesActive forum topics 
Recent comments
1 hour 44 min ago
1 hour 47 min ago
2 hours 27 min ago
2 hours 46 min ago
11 hours 4 min ago
13 hours 8 min ago
14 hours 26 min ago
15 hours 12 min ago
15 hours 36 min ago
15 hours 45 min ago