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

Discussions autour de cette fonctionnalité de Coq

a marqué ce sujet comme résolu.

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 :). ↩

+0 -0

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).

+0 -0

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
Connectez-vous pour pouvoir poster un message.
Connexion

Pas encore membre ?

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