The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

On Feb 19, 2006, at 5:58 PM, Ron wrote:

> 2006/2/19, Adam Chlipala 
> <adamc AT cs.berkeley.edu>:
> > Ron wrote:
> >
> > > Now, it would be very interesting if someone would have  
> > > formalized all
> > > x86 instructions or similar. Did anyone do this?
> > I've formalized in Coq the parts of x86 that I've needed so far  
> > for the
> > tasks I've attempted.  There is the beginning of a re-usable  
> > library for
> > parsing machine code (with OCaml) and proving things about the  
> > resulting
> > ASTs (with Coq) here:
> >     http://cvs.sourceforge.net/viewcvs.py/proofos/asm/
> Ok, that's very interesting. Do I understand correctly that you try to
> load a binary and then load that up in Coq somehow, with the theorem
> you want to prove about that program. And then a user could start
> proving something about this? I.e. this is different from all the "oh,
> we have this dependently typed language with programmers supplying all
> the proofs"-approach :)
>
> > I know that some other people have also created formalizations,  
> > but none
> > are really packaged for wide use.  I asked your exact question on  
> > this
> > list before beginning the above library and received no positive  
> > answers.
> Great initiative :)
> > > Or if not, what is
> > > the most complex program of which non-trivial statements have been
> > > proved?
> > If you count memory safety as non-trivial (and the proofs are quite
> > non-trivial!), then we can prove facts about arbitrarily complicated
> > programs; anything outputted by a certifying ML compiler, for  
> > instance,
> > in a format like typed assembly language.  If that's not non-trivial
> > enough for you, then probably the Certified Assembly Programming  
> > work at
> > Yale has dealt with the most interesting properties that I've seen.
> If you don't have this cool typed assembly language, but only a binary
> with x86, then that doesn't work, but if I understand correctly your
> "library" does not assume a typed assembly, right?
>
> > > And what software is used most is this context? Coq? With what
> > > libraries?
> > Anecdotally, I've heard of the most projects in this area that use  
> > Coq.
> Ok, then I am on the right track.
>
> P.S. Did you or anybody else use the book Coq'Art to become
> experienced with Coq? Can you recommend it? Amazon does not have
> reviews.

I have a copy of Coq'Art, and my opinion is that it is quite good.  I  
refer to it with some frequency.  I went into reading it after having  
worked with Coq for a couple of weeks; I think it was easier reading  
for that.  I think otherwise I would have done more re-reading and  
scratching my head.  That said, there are some of the more esoteric  
areas that Coq'Art doesn't cover.  For example, there is an important  
restriction on inductive definitions called some thing like the  
"positivity requirement" which I could not find in Coq'Art; I had to  
dig around in the documentation and finally read a journal paper  
before I found a satisfactory explanation of what this restriction is  
and why it exists.

Short version: it's good.  Get it if you plan to do any serious work  
with Coq.


Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
          -- TMBG