Avis des lecteurs
Résumé:Les critiques du livre soulignent son accessibilité et son approche pratique des types dépendants à l'aide d'Agda, en insistant sur le fait qu'il convient aux débutants malgré quelques lacunes en matière de clarté et d'organisation. Bien que de nombreux lecteurs le trouvent excellent pour l'apprentissage d'Agda et de la preuve de théorèmes, il y a des critiques concernant sa structure, sa clarté et sa présentation, en particulier dans la version Kindle.
Avantages:⬤ Introduction accessible aux types dépendants dans des contextes pratiques utilisant Agda.
⬤ Prépare les lecteurs à un matériel plus avancé sur la théorie des types et la preuve par le théorème.
⬤ Contient un bon nombre de preuves simples et d'exemples pratiques.
⬤ Convient aux lecteurs qui n'ont pas de connaissances préalables en logique ou en théorie des types, ce qui élargit son audience.
⬤ Manque de couverture théorique des types dépendants.
⬤ Certaines sections ne mettent pas l'accent sur les concepts généraux avant de plonger dans les détails.
⬤ Problèmes de clarté dans les explications et l'organisation des chapitres ; certains points sont trop répétés tandis que d'autres sont expliqués de manière inadéquate.
⬤ La version Kindle a une mauvaise mise en page, avec une indentation inadéquate des paragraphes et des problèmes d'alignement avec le code source.
(basé sur 4 avis de lecteurs)
Titre original :
Verified Functional Programming in Agda
Contenu du livre :
Agda est un langage de programmation avancé basé sur la théorie des types. Le système de types d'Agda est suffisamment expressif pour permettre une vérification fonctionnelle complète des programmes, dans deux styles.
Dans la vérification externe, nous écrivons des programmes fonctionnels purs, puis des preuves de leurs propriétés. Les preuves sont des artefacts externes distincts, utilisant typiquement l'induction structurelle. Dans la vérification interne, nous spécifions les propriétés des programmes par le biais de types riches pour les programmes eux-mêmes.
Cela nécessite souvent d'inclure des preuves à l'intérieur du code, pour montrer au vérificateur de type que les propriétés spécifiées sont valables. Le pouvoir de prouver les propriétés des programmes dans ces deux styles est un ajout profond à la pratique de la programmation, donnant aux programmeurs le pouvoir de garantir l'absence de bogues, et donc d'améliorer la qualité des logiciels plus qu'il n'était possible de le faire auparavant. La programmation fonctionnelle vérifiée en Agda est le premier livre à fournir une exposition systématique de la vérification externe et interne en Agda, adaptée aux étudiants de premier cycle en informatique.
Aucune familiarité avec la programmation fonctionnelle ou les preuves vérifiées par ordinateur n'est présupposée. Le livre commence par une introduction à la programmation fonctionnelle à travers des exemples familiers comme les booléens, les nombres naturels et les listes, et les techniques de vérification externe. La vérification interne est abordée à travers des exemples de vecteurs, d'arbres de recherche binaires et d'arbres de Braun.
Des éléments plus avancés sur le calcul au niveau du type, le raisonnement explicite sur la terminaison et la normalisation par évaluation sont également inclus. Le livre comprend également une étude de cas de taille moyenne sur le codage et le décodage de Huffman.
Autres informations sur le livre :
| ISBN : | 9781970001273 |
| Auteur : | |
| Éditeur : | |
| Langue : | anglais |
| Reliure : | Relié |
Achat:
Actuellement disponible, en stock.
