Re: [isabelle] Automation is awesome; one bibliography leads to another

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 MHonArc.