Programmazione funzionale verificata in Agda

Recensioni dei lettori

Le recensioni del libro ne evidenziano l'accessibilità e l'approccio pratico ai tipi dipendenti utilizzando Agda, sottolineandone l'idoneità per i principianti nonostante alcune carenze in termini di chiarezza e organizzazione. Sebbene molti lettori lo trovino eccellente per l'apprendimento di Agda e della dimostrazione di teoremi, ci sono critiche riguardo alla sua struttura, chiarezza e presentazione, in particolare nella versione Kindle.

⬤ Introduzione accessibile ai tipi dipendenti in contesti pratici utilizzando Agda.
⬤ Prepara il lettore a materiale più avanzato sulla teoria dei tipi e sulla dimostrazione di teoremi.
⬤ Contiene un buon numero di prove semplici ed esempi pratici.
⬤ È adatto a lettori senza conoscenze preliminari di logica o teoria dei tipi, aumentando così la sua portata.

⬤ Manca la trattazione teorica dei tipi dipendenti.
⬤ Alcune sezioni non enfatizzano i concetti generali prima di immergersi nei dettagli.
⬤ Problemi di chiarezza nelle spiegazioni e nell'organizzazione dei capitoli; alcuni punti sono eccessivamente ripetuti mentre altri sono spiegati in modo inadeguato.
⬤ La versione Kindle è impaginata male, con un'indentazione dei paragrafi inadeguata e problemi di allineamento con il codice sorgente.

(basato su 4 recensioni dei lettori)

Titolo originale:

Verified Functional Programming in Agda

Contenuto del libro:

Agda è un linguaggio di programmazione avanzato basato sulla teoria dei tipi. Il sistema di tipi di Agda è abbastanza espressivo da supportare la verifica funzionale completa dei programmi, in due stili.

Nella verifica esterna, scriviamo programmi funzionali puri e poi scriviamo prove di proprietà su di essi. Le prove sono artefatti esterni separati, che in genere utilizzano l'induzione strutturale. Nella verifica interna, specifichiamo le proprietà dei programmi attraverso tipi ricchi per i programmi stessi.

Questo spesso richiede l'inclusione di prove all'interno del codice, per dimostrare al verificatore di tipo che le proprietà specificate sono valide. La possibilità di dimostrare le proprietà dei programmi in questi due stili rappresenta una profonda aggiunta alla pratica della programmazione, in quanto dà ai programmatori la possibilità di garantire l'assenza di bug e quindi di migliorare la qualità del software più di quanto fosse possibile in precedenza. Verified Functional Programming in Agda è il primo libro a fornire un'esposizione sistematica della verifica esterna e interna in Agda, adatta agli studenti universitari di Informatica.

Non si presuppone alcuna familiarità con la programmazione funzionale o con le prove verificate al computer. Il libro inizia con un'introduzione alla programmazione funzionale attraverso esempi familiari come booleani, numeri naturali e liste, e alle tecniche di verifica esterna. La verifica interna viene considerata attraverso gli esempi di vettori, alberi di ricerca binari e alberi di Braun.

Sono inclusi anche materiali più avanzati sul calcolo a livello di tipo, sul ragionamento esplicito sulla terminazione e sulla normalizzazione per valutazione. Il libro include anche un caso di studio di medie dimensioni sulla codifica e decodifica di Huffman.