The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Ron wrote:

> 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 :)
>  
That's right.  Coq is really just such a dependently typed language, 
with the extra facilities for interactive programming/proving.

> 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?
>  
The types in typed assembly language are just proof hints.  TAL-based 
approaches are quite compatible with producing standard x86 binaries.

There is no idea of assembly-level types in the library I linked.

> 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 found it to be a very worthwhile book to read.