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 2011-09-17 13:38 | LtU Forum | previous forum topic | next forum topic | other blogs | 10319 reads
|
Browse archives
Active forum topics |
Recent comments
22 weeks 6 days ago
22 weeks 6 days ago
22 weeks 6 days ago
45 weeks 19 hours ago
49 weeks 2 days ago
50 weeks 6 days ago
50 weeks 6 days ago
1 year 1 week ago
1 year 6 weeks ago
1 year 6 weeks ago