Lambda the Ultimate

From ICFP '06, the 1st informal Workshop on Mechanizing Metatheory comes Nick Benton's "Machine Obstructed Proof: How many months can it take to verify 30 assembly instructions?". It is a one page paper, but seems deserving of some notice.

Nick Benton offers a critique of Coq from the standpoint of an inexperienced user, although I am not sure I would really categorize Benton as "inexperienced". Some interesting quotes:

• "...I have rarely felt as stupid and frustrated as I did during my first few weeks using Coq."
• "Tactical theorem proving is like an extreme form of aspect-oriented programming. This is not A Good Thing...."
• "Just having intermediate stages of the work in a computerized form...proved a major benefit."
• "Automated proving is not just a slightly more fussy version of paper proving and neither...is it really like programming."
• "...but the payoff really came the second time I used Coq: I was able to prove some elementary but delicate results...in just a day or so."

[On edit: moved to a story from a forum post. Sorry. - TM]

This looks very interesting:

http://homepage.mac.com/luke_e/Menu8.html

(Luke also posted an announcement to the Haskell mailing list)