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

4 hours 38 min ago

4 hours 51 min ago

5 hours 41 min ago

6 hours 15 min ago

7 hours 26 min ago

8 hours 35 min ago

13 hours 7 min ago

15 hours 17 min ago

1 day 4 hours ago

1 day 8 hours ago