Zweryfikowane programowanie funkcjonalne w Agda

Opinie czytelników

Recenzje książki podkreślają jej przystępność i praktyczne podejście do typów zależnych przy użyciu Agdy, podkreślając jej przydatność dla początkujących pomimo pewnych niedociągnięć w jasności i organizacji. Podczas gdy wielu czytelników uważa ją za doskonałą do nauki Agdy i dowodzenia twierdzeń, pojawiają się krytyczne uwagi dotyczące jej struktury, przejrzystości i prezentacji, szczególnie w wersji Kindle.

⬤ Przystępne wprowadzenie do typów zależnych w praktycznych zastosowaniach Agdy.
⬤ Przygotowuje czytelników do bardziej zaawansowanego materiału na temat teorii typów i dowodzenia twierdzeń.
⬤ Zawiera dużą liczbę prostych dowodów i praktycznych przykładów.
⬤ Nadaje się dla czytelników bez wcześniejszej wiedzy z logiki lub teorii typów, zwiększając zasięg odbiorców.

⬤ Brakuje teoretycznego omówienia typów zależnych.
⬤ Niektóre sekcje nie kładą nacisku na ogólne koncepcje przed zagłębieniem się w szczegóły.
⬤ Problemy z przejrzystością w wyjaśnieniach i organizacji rozdziałów; niektóre punkty są nadmiernie powtarzane, podczas gdy inne są nieodpowiednio wyjaśnione.
⬤ Wersja na Kindle ma kiepski układ, z nieodpowiednimi wcięciami akapitów i problemami z wyrównaniem kodu źródłowego.

(na podstawie 4 opinii czytelników)

Oryginalny tytuł:

Verified Functional Programming in Agda

Zawartość książki:

Agda to zaawansowany język programowania oparty na teorii typów. System typów Agdy jest wystarczająco ekspresyjny, aby wspierać pełną funkcjonalną weryfikację programów, w dwóch stylach.

W weryfikacji zewnętrznej piszemy czyste programy funkcjonalne, a następnie piszemy dowody ich właściwości. Dowody są oddzielnymi zewnętrznymi artefaktami, zwykle wykorzystującymi indukcję strukturalną. W weryfikacji wewnętrznej określamy właściwości programów poprzez bogate typy dla samych programów.

Często wymaga to dołączenia dowodów wewnątrz kodu, aby pokazać modułowi sprawdzania typów, że określone właściwości mają zastosowanie. Możliwość udowadniania właściwości programów w tych dwóch stylach jest głębokim dodatkiem do praktyki programowania, dając programistom możliwość zagwarantowania braku błędów, a tym samym poprawy jakości oprogramowania w większym stopniu niż było to wcześniej możliwe. Verified Functional Programming in Agda to pierwsza książka, która zapewnia systematyczną ekspozycję zewnętrznej i wewnętrznej weryfikacji w Agda, odpowiednią dla studentów studiów licencjackich informatyki.

Nie zakłada się znajomości programowania funkcyjnego ani sprawdzanych komputerowo dowodów. Książka rozpoczyna się od wprowadzenia do programowania funkcyjnego poprzez znane przykłady, takie jak boole, liczby naturalne i listy, oraz techniki weryfikacji zewnętrznej. Weryfikacja wewnętrzna jest rozważana na przykładach wektorów, drzew wyszukiwania binarnego i drzew Brauna.

Bardziej zaawansowany materiał na temat obliczeń na poziomie typu, jawnego rozumowania o zakończeniu i normalizacji przez ocenę jest również zawarty. Książka zawiera również średniej wielkości studium przypadku dotyczące kodowania i dekodowania Huffmana.