## User login## Navigation |
## Machine Obstructed ProofFrom 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] |
## Browse archives## Active forum topics |

## Recent comments

18 hours 54 min ago

19 hours 9 min ago

20 hours 2 min ago

20 hours 49 min ago

21 hours 17 min ago

21 hours 39 min ago

21 hours 57 min ago

22 hours 39 min ago

23 hours 1 min ago

23 hours 17 min ago