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 (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.)