[isabelle] Title of "Programming and Proving" [Re: ?spam? Re: Simpler theorem statements, and proofs for them]



2012-11-23 06:55 Tobias Nipkow:
Am 22/11/2012 17:15, schrieb Christoph LANGE:
BTW, about "Programming and Proving": I had noticed this manual when I got
started with Isabelle, but then didn't take a closer look, as I was misled by
the "Programming".  I thought it was some specific guide on verifying functional
programs.

In a way it is. It starts from a functional programming perspective. If you have
a suggestion for a better title, let me know.

OK, got the point.  Now I really can't imagine a better title.

But I could imagine a better _guidance_, both on the documentation website (http://isabelle.in.tum.de/documentation.html) and in the "doc/Contents" file of the Isabelle installation (at least I have /usr/share/doc/isabelle-2012/doc/Contents when installing from the Gentoo Linux package).

On the website, Prog&Prove is listed first, but under a section header "Miscellaneous tutorials". The section title could be changed to "Getting started", and each document link could be followed by a few words of explanation, e.g.:

Programming and Proving in Isabelle/HOL – Isabelle by example; read this first

Similarly, the doc/Contents file should not merely restate the _titles_ of the documents, but provide the same extra information.

Cheers,

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  2–5 April 2013, Exeter, UK.  Deadlines 10 Dec (stage 1), 14 Jan (st. 2)
  http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.