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
come equipped with proofs of (some of) their properties.</p>
<p>Matita is currently adopted in the European Union "Certified Complexity" Project
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
come equipped with proofs of (some of) their properties.</p>
<p>Matita is currently adopted in the European Union "Certified Complexity" Project