The Coq mailing list

[Daniel Nagle <Daniel.Nagle AT ul.ie>]

To Whom it may Concern:
I am a student working on a project involving the construction and 
proving of theorems for use in software verification. Part of my brief 
is to learn what specific theorem provers are best at doing and why. Coq 
has been heartily recommended to me and I am wondering if someone could 
point out a good source of information to on the theorem prover that 
would perhaps help me answer the folloing questions.

What are the main advantages of Coq in comparison to other Theorem Provers?
What area's in Coq are weak in comparison to other theorem provers?
Is it possible to interface Coq directly with another program through 
other methods apart from pipes and standard I/O?

If you can help me with the above questions I posed I would be very 
grateful.

All the best,
Daniel Nagle.