Lo scopo del corso è duplice. Da un lato, si vogliono illustrare le radici logiche dell'informatica, dall'altro si vogliono usare metodologie della logica, o meglio della teoria della dimostrazione, per la formalizzazione rigorosa della specifica di un programma e per porre le basi per la verifica automatica di proprietà di programmi. Si partirà dalla logica classica, poi si passerà alla logica intuizionista di cui si vedrà soprattutto l'aspetto costruttivo. Attraverso la decorazione delle dimostrazioni con un linguaggio tipo il lambda calcolo si vedrà quindi la connessione con i linguaggi di programmazione.