The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, September 24, 2011 07:38:45 AM Benjamin C. Pierce wrote:
> Hi Daniel,
> 
> Several of these topics are also covered in the Software Foundations
> textbook (http://www.cis.upenn.edu/~bcpierce/sf).
> 
> Would it make sense, for your intended audience, to take some initial
> prefix of SF as background and build the remainder of the tutorial as a
> "companion volume" that could be distributed together with SF?  We have
> already done this with some smaller companion contributions such as Arthur
> Chargueraud's two chapters on Coq automation and Andrew Tolmach's chapter
> on normalization.  In the long run, I would love to see SF turn into a
> collection of loosely integrated electronic textbooks on a range of topics
> (PL metatheory, formalized mathematics, verified compilation, verified
> algorithms, …).
> 
> Besides saving you some (hopefully substantial) work on explaining basic
> aspects of Coq, we can offer you some reasonably polished conventions and
> tools for organizing and (HTML-) typesetting your material, exercises with
> hidden solutions, terse variants for use in lectures, etc.  And everyone
> benefits from the synergy of one combined effort instead of two smaller
> ones.
> 
> If this might be of interest, let me know and we can discuss further.

I've been looking at this a bit.  I think for my intended audience, I'd 
prefer 
to start out right from the beginning with doing some simple proofs, whereas 
in SF it seems to have more of a focus on programming (starting out with how 
to define some simple types and functions on them, etc.).

I'd definitely be interested in seeing the tools you use for SF, though, and 
probably also in seeing the tools Adam used to produce CPDT.  One thing that 
I'm planning to do is to go through certain developments the way somebody 
might actually develop them, complete with false starts.  For example: "Oh, I 
need to prove this intermediate result?  That seems like something which 
could 
be useful more generally.  Let me go back and prove that as a general lemma, 
then return to what I was working on before."  Or, "Hmm, this destruct or 
induction didn't leave me with a context that lets me proceed.  Let me undo 
that, and try inversion instead of destruct, or revert some hypotheses before 
trying to use induction."  Is that sort of thing possible with the SF 
templates?  I know in CPDT, Adam uses "Undo." or "Abort." where this sort of 
situation comes up.  I'm more used to using Coqide than Proof General, 
though, 
so I'd really like to be able to say "OK, so let's rewind above the current 
incomplete proof, add such and such, then execute until the bottom again."  
And then maybe provide example scripts that reflect the final state.  But I'm 
open to using Adam's style with Proof General if being able to step through 
precanned files is important, as opposed to having to type things in from a 
copy of the tutorial.
-- 
Daniel