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

22 hours 30 min ago

3 days 6 hours ago

3 days 9 hours ago

4 days 4 hours ago

4 days 11 hours ago

4 days 15 hours ago

4 days 15 hours ago

4 days 18 hours ago

5 days 9 hours ago

5 days 13 hours ago