- <p class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-tinycals.png">
- <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
- </a>
- </span>
- The tactical language, part of the proof language, has
- step-by-step semantics, enabling inspection and replaying of deeply
- structured proof scripts. </p>
-
- <p>Matita is partially supported by the following Projects:
- <ul>
- <li><a href=http://www.cs.chalmers.se/Cs/Research/Logic/Types/>
- Types Project</a>
- <li><a href=http://www.mctafi.math.unipd.it/>McTafi</a></li>
- </ul>
+ <p>It embeds key computational constructs of functional programming languages:
+ functions can be defined by (well-founded) recursion, and are live entities that can be
+ tested and executed.</p>
+
+ <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
+ 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
+ <a href="http://cerco.cs.unibo.it/">CerCo<a> for the formal verification of a
+ complexity-preserving compiler from a large subset of C to a microcontroller
+ assembly of the kind traditionally used in embedded systems.