Matita e' un tool sperimentale di supporto alla dimostrazione interattiva di teoremi, in via di sviluppo al Dipartimento di Scienze dell'Informazione della Universita' degli Studi di Bologna.

Un dimostratore interattivo e' uno strumento software di ausilio alla dimostrazione formale di teoremi attraverso la collaborazione tra l'uomo e la macchina. Fornisce un liguaggio formale in cui coesistono definizioni matematiche, algoritmi eseguibili, teoremi e relative dimostrazioni, ed un ambiente interattivo che tiene traccia dello stato corrente delle prove, e le aggiorna in funzione dei comandi (tattiche) impartiti dall'utente.

Matita si fonda su di un Sistema di Tipi Dipendenti noto con il nome di Calcolo delle Costruzioni Induttive.

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.

Al tempo stesso, le dimostrazioni sono una parte integrale del formalismo, cosa che permette di ottenere, attraverso l' isomorfismo di Curry Howard , 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 proof-carrying-code, dove frammenti di software sono arricchiti con dimostrazioni di alcune delle loro proprieta'.

Matita e' attualmente adottato nel Progetto Europeo CerCo (Certified Complexity) per la verifica formale della preservazione della complessita' durante la fase di compilazione da linguaggio C verso un linguaggio assembly tipico di microprocessori per sistemi embedded.