Programare funcțională verificată în Agda

Recenzii ale cititorilor

Recenzile cărții evidențiază accesibilitatea și abordarea practică a tipurilor dependente folosind Agda, subliniind caracterul său adecvat pentru începători, în ciuda unor deficiențe în ceea ce privește claritatea și organizarea. Deși mulți cititori o consideră excelentă pentru a învăța Agda și demonstrarea teoremelor, există critici privind structura, claritatea și prezentarea sa, în special în versiunea Kindle.

⬤ Introducere accesibilă la tipurile dependente în contexte practice folosind Agda.
⬤ Pregătește cititorii pentru materiale mai avansate privind teoria tipurilor și demonstrarea teoremelor.
⬤ Conține un număr bun de demonstrații simple și exemple practice.
⬤ Potrivit pentru cititori fără cunoștințe prealabile de logică sau de teoria tipurilor, ceea ce îi sporește audiența.

⬤ Lipsă de acoperire teoretică a tipurilor dependente.
⬤ Unele secțiuni nu pun accentul pe conceptele generale înainte de a intra în detalii.
⬤ Probleme de claritate în explicațiile și organizarea capitolelor; unele puncte sunt repetate excesiv, în timp ce altele sunt explicate inadecvat.
⬤ Versiunea Kindle are o prezentare slabă, cu o indentare inadecvată a paragrafelor și probleme de aliniere cu codul sursă.

(pe baza a 4 recenzii ale cititorilor)

Titlul original:

Verified Functional Programming in Agda

Conținutul cărții:

Agda este un limbaj de programare avansat bazat pe teoria tipurilor. Sistemul de tipuri al Agda este suficient de expresiv pentru a susține verificarea funcțională completă a programelor, în două stiluri.

În verificarea externă, scriem programe pur funcționale și apoi scriem dovezi ale proprietăților acestora. Dovezile sunt artefacte externe separate, folosind de obicei inducția structurală. În verificarea internă, specificăm proprietățile programelor prin tipuri bogate pentru programele în sine.

Acest lucru necesită adesea includerea de dovezi în interiorul codului, pentru a arăta verificatorului de tip că proprietățile specificate sunt valabile. Puterea de a dovedi proprietățile programelor în aceste două stiluri este un adaos profund la practica programării, oferind programatorilor puterea de a garanta absența erorilor și, astfel, de a îmbunătăți calitatea software-ului mai mult decât era posibil anterior. Programarea funcțională verificată în Agda este prima carte care oferă o expunere sistematică a verificării externe și interne în Agda, potrivită pentru studenții de licență de la Informatică.

Nu se presupune nicio familiaritate cu programarea funcțională sau cu probele verificate de calculator. Cartea începe cu o introducere în programarea funcțională prin exemple familiare precum booleenii, numerele naturale și listele, și tehnici de verificare externă. Verificarea internă este luată în considerare prin exemple de vectori, arbori de căutare binară și arbori Braun.

De asemenea, sunt incluse materiale mai avansate privind calculul la nivel de tip, raționamentul explicit privind terminarea și normalizarea prin evaluare. Cartea include, de asemenea, un studiu de caz de dimensiuni medii privind codarea și decodarea Huffman.