Between his talk here at U of C and his invited talk at ICFP this year, Bob Harper has convinced me I ought to look into Twelf: even us "regular folks" who aren't interested making up logics and seeing what neat theorems a program can deduce unaided (ivory tower!) but instead just want to prove regular old theorems about properties of programming languages (practically blue-collar!) can derive benefit from it. So I went to the web site, downloaded and installed the software and started in on Andrew Appel's tutorial.

First impression: cool! I'm not at all skilled at it yet — I've been able to prove that

(Oh, and note to the myriad Twelf implementors that undoubtedly read this page regularly: the README doesn't tell you that if you've only got SML/NJ installed you've got to say

First impression: cool! I'm not at all skilled at it yet — I've been able to prove that

`(A or B) implies (B or A)`,`(A implies B implies C) implies ((A and B) implies C)`and similar teensy little logical theorems but nothing bigger. Nonetheless, when I'm writing theorems in Twelf I feel like I'm in a cool place where I'm doing programming (easy!) but the result is math (hard!). Of course that's not really fair, since the programming is very mathematical and the proofs very easy; we'll see how I feel when I get to the point where I'm using it to prove type-soundness theorems and the like.(Oh, and note to the myriad Twelf implementors that undoubtedly read this page regularly: the README doesn't tell you that if you've only got SML/NJ installed you've got to say

`./smlnj/install.sh`rather than`make`. I was about to give up when I noticed that`smlnj/`directory in the distribution archive.)
## 1 Comments:

There's a typo in the http://www.twelf.org/ redirect: www.cs.cmue.edu instead of www.cs.cmu.edu.

By Anonymous, at 15:35

Post a Comment

<< Home