From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 3 Apr 2012 15:36:09 +0000 (+0000)
Subject: Minor changes
X-Git-Tag: make_still_working~1821
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f86d822d5d47b5b5b2f8940c5b90c1fcdc547420;p=helm.git

Minor changes
---

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 05ed186c0..5da934cdc 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -46,7 +46,7 @@
       <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 
diff --git a/helm/www/matita/matita_it.shtml b/helm/www/matita/matita_it.shtml
index 0d77ec373..04b43167c 100644
--- a/helm/www/matita/matita_it.shtml
+++ b/helm/www/matita/matita_it.shtml
@@ -38,15 +38,15 @@
       Matita si fonda su di un Sistema di <a href="http://en.wikipedia.org/wiki/Dependent_type">Tipi Dipendenti</a> noto con il nome di Calcolo delle
       Costruzioni Induttive.</p>
 
-      <p>Questo calcolo integra al proprio interno alcuni cosrtutti computazionali tipici dei linguaggi di programmazione funzionali: in particolare, si 
-     possono definire funzioni per ricorsione (ben fondata), la cui 
-    applizazione puo' essere effetivamente calcolata come per normali programmi.
+      <p>Questo calcolo integra al proprio interno alcuni costrutti computazionali 
+     tipici dei linguaggi di programmazione funzionali: in particolare, si 
+     possono definire funzioni per ricorsione (ben fondata), che possono essere
+     valutate e testate come dei normali programmi.
      </p>
 
       <p>Al tempo stesso, le dimostrazioni sono una parte integrale del
       formalismo, cosa che permette di ottenere, attraverso l'
-      <a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence">isomorfismo di Curry Howard </a>, una efficace integrazione tra specifica e
-      ragionamento: le prove sono oggetti di prima classe del linguaggio
+      <a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence">isomorfismo di Curry Howard </a>, una efficace integrazione tra specifica del comportamento, sua realizzazione implementativa e relativa verifica di correttezza: le prove sono oggetti di prima classe del linguaggio
       e possono essere trattati come dei normali tipi di dato, inducendo
       in modo naturale uno stile di programmazione simile al
       <a href="http://en.wikipedia.org/wiki/Proof-carrying_code">proof-carrying-code</a>, dove frammenti di software sono arricchiti con dimostrazioni di