The Coq mailing list

[Ron <iampure AT gmail.com>]

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.