Fonctions fortement typés (strongly-specified) en Coq

Discussions autour de cette fonctionnalité de Coq

L'auteur de ce sujet a trouvé une solution à son problème.
Auteur du sujet

Bonjour à tous.

Récemment, j'ai écris un petit article sur les fonctions fortement typés en Coq. Je me suis dit que ça pourrait être intéressant d'en parler1.

Si vous avez des remarques sur l'article en lui-même, je suis à la recherche de feedback. Mais j'aimerai aussi avoir votre avis sur cette fonctionnalité de Coq, qui compte parmi mes préférées du bousin.


  1. Et comme on m'a encouragé à créer un nouveau sujet, le voici :). 

Édité par lethom

Auteur du sujet

Pourquoi pas, après tout. J'y avais pensé, mais ça demanderait un peu de travail. En l'état, l'article n'est pas forcément super pédagogique et s'adresse à « ceux qui connaissent déjà ». Je ne sais pas à quel point il faudrait le retravailler pour qu'il cadre bien à ZdS (et il faudrait lui rajouter une conclusion huhu).

En l'état, l'article n'est pas forcément super pédagogique et s'adresse à « ceux qui connaissent déjà »

Je ne pense pas que ça soit très grave. Il faut arrêter l'auto-censure sous prétexte que l'on a peur de ne pas être pédagogue (ou que l'on ne veut carrément pas l'être). Les articles techniques/avancés ont aussi leur place sur le site. Si vraiment ça intéresse les débutants curieux mais que ceux-ci se plaignent de ne rien comprendre, au moins on saura que ça vaut la peine d'écrire un document introductif…

+1 -0
Vous devez être connecté pour pouvoir poster un message.
Connexion

Pas encore inscrit ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte