## 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

7 weeks 3 days ago

7 weeks 5 days ago

7 weeks 6 days ago

14 weeks 6 days ago

20 weeks 4 days ago

20 weeks 5 days ago

21 weeks 4 days ago

24 weeks 3 days ago

25 weeks 5 days ago

25 weeks 6 days ago