Alla scoperta dei proof assistant con Agda

Trascrizione codice: https://dpdmancul.gitlab.io/agda-examples/transcript.html Appunti (in inglese): https://dpdmancul.gitlab.io/agda-examples/ Un viaggio alla scoperta dei proof assistant, fra matematica, logica , filosofia e informatica. 0:00 Introduzione 6:40 Agda 8:33 Numeri naturali 19:20 Funzioni (somma) 26:40 Dimostrazioni 44:45 Logica 58:25 Principio del terzo escluso e monadi di continuazione 1:08:10 Sillogismi 1:17:20 Liste 1:28:40 Correttezza programmi 1:35:01 Intelligenza artificiale nei proof assistant 1:37:00 Oltre Agda: Idris2 e Isabelle 1:38:50 Dimostrare correttezza algoritmi vs codice 1:42:05 Monadi (promise, future, task)