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



Am 23/11/2012 11:49, schrieb Christoph LANGE:
> 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

I think most of the titles are self-explanatory, and indicate that they are
special manuals. Except for the first two. But all of them come with an abstract
or intro, and prog-prove explains quite clearly what it is about (and mentions
that the second one is old fashioned). You might want to also have this abstract
on the web page, but that would require yet more mechanisms.

However, there is a small linguistic point, which you may or may not have
intended to make: "Miscellaneous" material usually comes at the end. These are
"Tutorials", no qualification. The next subsection isn't called "Miscellaneous
Reference Manuals" either, and the whole section is called "Tutorials and
manuals". Makarius, could you drop the "Miscellaneous", please?

Tobias


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





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