The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

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

SF includes simple proofs in the first chapter.  They're proofs about little 
programs, so a bit of programming comes first.  But I expect readers with 
some functional programming background will get through that part (indeed, 
the whole chapter) in a few minutes.

> I'd definitely be interested in seeing the tools you use for SF

I'll email you off list.

   - Benjamin