semi off-topic: Prof. Pierce's research group created the Unison bi-directional file synchronizer and open-sourced it. It's a really useful tool that I use literally every single day to keep my files synchronized. Think of it as a predecessor to dropbox, without the UI polish ;)<p><a href="http://www.cis.upenn.edu/~bcpierce/unison/" rel="nofollow">http://www.cis.upenn.edu/~bcpierce/unison/</a>
The project he's working on, <a href="http://www.seas.upenn.edu/~harmony/" rel="nofollow">http://www.seas.upenn.edu/~harmony/</a>, is one I've been half-paying-attention to for a while.<p>In particular something like this will (I think) be a perfect substrate for refactoring parsers, semantic diff tools, and other neat stuff...
The author, Benjamin Pierce, also wrote the book <i>Types and Programming Languages</i>, among others.<p>His website: <a href="http://www.cis.upenn.edu/~bcpierce/" rel="nofollow">http://www.cis.upenn.edu/~bcpierce/</a>
<i>Do we want languages where a PhD is required to understand the library documentation?<p>two PhDs for Haskell</i><p>This presentation is so lighthearted... I realy like it.
What's a good introduction to contracts? I'd like to know how a basic contract system works and which extensions are there? What's the relation between contracts and assert?
With respect to very precise type systems, and coupling between program structure and types, one of the reason mathematics is so powerful is its flexibility<p>I actually have trouble with mathematics, because it is so flexible. For example, equality of sets A and B is typically shown by saying that every element of A is in B, and every element in B is in A. <i>Why on earth do they do that? Why not just say they're the same??!</i><p>One advantage is it gives you the flexibility to demonstrate the first limb using one technique, and the second limb with a completely unrelated approach. I saw one example of showing equivalence of language defined by a class of grammars, and a language defined by constraints over sequences. You could even use a constructive and a non-constructive proof for each half.<p>It's a way of subdividing that is decoupled.