Re: [isabelle] Automation is awesome; one bibliography leads to another
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Automation is awesome; one bibliography leads to another
- From: gottfried.barrow at gmx.com
- Date: Fri, 01 Jun 2012 15:59:17 -0500
- In-reply-to: <35D863A5-A351-4E40-A8D5-DFC520C8D964@cam.ac.uk>
- References: <4FC6BFB2.firstname.lastname@example.org> <CAMej=27mXQQNYE8SLpOnPzpDKaprCs=XjinmQBPSSbx7F9breA@mail.gmail.com> <35D863A5-A351-4E40-A8D5-DFC520C8D964@cam.ac.uk>
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
Larry, Ramana, and Freek,
Thanks for the comments.
I can sort of see the value in only focusing on the high level concepts
of the statements of the theorem and lemmas.
I think Isabelle brings togrether a diverse group of people. There's
academics, the commercial world of software and hardware design, and the
world of research which ties them together. If I was getting paid
$80,000 a year to verify software design, my attitude would be "work as
fast as possible, and don't concern me with the details when not
necessary". As it is, I'm favoring the education end of the spectrum.
I'll switch gears when I get that $100,000 a year job offer.
This archive was generated by a fusion of
Pipermail (Mailman edition) and