The Coq mailing list

[Andrew Pennebaker <andrew.pennebaker AT gmail.com>]

That's really funny! :)

I'll do that, then.

Cheers,

Andrew Pennebaker

www.yellosoft.us

On Wed, Nov 2, 2011 at 5:46 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

Andrew Pennebaker wrote:

Sorry, I didn't realize how important the question was to you. I tend to skim tutorials and try to code on my own afterwards, skimming more deeply for specific areas of interest.

I started reading Chapter 1, skimming less over the start and more over the end, when I realized Coq was being compared to other verifiers like HOL, which I am also not familiar with, so the comparisons would be largely meaningless.

In Chapter 2, I was amazed that the tutorial jumps right into constructing a compiler for a stack language. The note about coqdoc / prettyprinting was very important; I would have been lost for how to type the code into Coq. On one hand, the prettyprinting is helpful, because the concision allows more information to be shown at once, but on the other, it's frustrating to learn two syntaxes in parallel when one, what you actually type into Coq, would have sufficed. The problem itself necessitates a parallel syntax: raw stack language expressions and compiled stack code. And then there's the parallel syntax of conceptual inductive proofs and inductive Coq proofs--I'm not even strong on hand inductive proofs. At that point, I started to get lost.

Chapter 2 is quite atypical.  It is, indeed, a demo, included as motivation, while all the later chapters are more traditional bottom-up presentations.  In effect, you stopped before reaching the part of the book that teaches how to use Coq!  So, I suggest continuing from Chapter 3, and trusting that the author of whatever source you're reading has chosen an appropriate order of presentation.  If at some point in reading, you haven't yet seen how to do something, be patient. :)