X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=5da934cdc8aa6661c76a4af35997b6fd49401713;hb=74c7035b4dd6933bda4479816e51f5771ee1f572;hp=68ebc8ad2fc76b3f5dc9aca4c14e6efa2fc8f6d9;hpb=33f5240193f527ef11619d3ae89cdbf2bfcecb07;p=helm.git diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index 68ebc8ad2..5da934cdc 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -25,14 +25,9 @@ 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 @@ -51,18 +46,19 @@
At the same time, proofs are an integrated part of the formalism, allowing, via the Curry Howard isomorphism, 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 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 + 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.
+