X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=5da934cdc8aa6661c76a4af35997b6fd49401713;hb=119da3f9ce130f7c4e8b23fcc491d221472ad657;hp=2bf6a2119984b97d5ed56ecf36d25fe60edae50a;hpb=727fa1f56c2e47203da5d232ad48b2fe02e63282;p=helm.git
diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 2bf6a2119..5da934cdc 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -1,68 +1,65 @@
-
-
- Matita home page
-
-
+
+ Matita (that means pencil in italian) is an experimental,
+ interactive theorem prover under development at the
+ Computer Science Department of the
+ University of Bologna.
+
-
+
+
+
+
+ An interactive prover is a software tool aiding the development of
+ formal proofs by man-machine collaboration. It provides a formal language
+ where mathematical definitions, executable algorithms and theorems cohexist,
+ and an interactive environment keeping the current status of the proof,
+ and updating it according to commands (usually called tactics) issued by the user.
+
+
+
+ Matita is based on a Dependent Type System known as the Calculus of Inductive Constructions.
-
-
+
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.
-
- - 1. Developers
- - 2. Documentation
- - 4. Download
-
-
-
-
+
At the same time, proofs are an integrated part of the formalism, allowing, via the
+ Curry Howard
+ isomorphism, a smooth interplay between
+ 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 proof-carrying-code,
+ where chunks of software
+ come equipped with proofs of (some of) their properties.
+
+
Matita is currently adopted in the European Union "Certified Complexity" Project
+ CerCo 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.
+
+
+
+
+
-
-