Dal Teorema al Codice: introduzione ai proof assistants per la certificazione del software

Le attività di certificazione, e in particolare quelle legate al software, rivestono un ruolo sempre più centrale nella società contemporanea. La questione del software certificato è però tutt’altro che banale: essa è profondamente connessa al tema della formalizzazione delle prove matematiche. Negli ultimi vent’anni sono stati sviluppati numerosi strumenti che, basandosi su logiche di ordine superiore particolarmente sofisticate, permettono di formalizzare dimostrazioni e produrre certificati software. Tra questi, i più affermati sono i cosiddetti Assistenti di Dimostrazione (Proof Assistants), come Coq, Isabelle e il più recente Lean di Microsoft. Sebbene tali strumenti siano generalmente utilizzati da esperti, questo minicorso offre agli studenti l’opportunità di muovere i primi passi nel mondo della certificazione del software attraverso un’interfaccia semplice e intuitiva. Astraendo dai dettagli tecnici più complessi, gli studenti potranno familiarizzare con alcuni dei principi fondamentali della certificazione e comprenderne il valore pratico. Il corso è stato erogato in lingua italiana, e si è svolto, in presenza, dal 19/11/2025 al 05/12/2025, per una durata totale di sei (6) ore. La prova finale (senza voto) consiste nella formalizzazione, attraverso uno strumento software online, di una dimostrazione per induzione strutturale su tipi di dato algebrico, come liste o alberi binari. Le competenze acquisite al termine del corso sono: formalizzazione di dimostrazioni e certificazione di software attraverso Assistenti di Dimostrazione.