Coq Proof Assistant

From the homepage.

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

I studied basic symbolic logic to learn Coq, but its still very difficult. I still have no idea about correspondence between "A's type is B" and "A is a proof of B" (Curry–Howard correspondence).