<p>At the same time, proofs are an integrated part of the formalism, allowing, via the
<a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence">Curry Howard
isomorphism</a>, a smooth interplay between
- specification and reasoning: proofs are objects of the language, and
+ specification, implementation and verification: proofs are objects of the language, and
can be treated as normal data, naturally leading to a programming style
akin to <a href="http://en.wikipedia.org/wiki/Proof-carrying_code">proof-carrying-code</a>,
where chunks of software