Le cas de Coq est un peu particulier, parce qu'il s'agit en fait d'au moins deux langages différents, Gallina, le langage de preuve en tant que tel, et Ltac, un langage de métaprogrammation qui est à Gallina ce que PHP est à HTML. Autant Gallina est plutôt bien spécifié[1], autant Ltac est un bousin sans nom qui est la source d'un tas de problèmes, le genre de code qu'il suffit de regarder fixement pour faire péter un développement à l'autre bout de la planète. Ceci dit, il y a eu du progrès depuis et l'utilisation d'une infrastructure d'intégration continue un peu sérieuse permet de jauger la casse avant la publication d'une version.
En ce qui concerne Bedrock, je me permets quand même de juger que c'est un cas vraiment extrême. C'est un projet notablement connu pour avoir été implémenté par des gens qui sont des spécialistes internationaux de l'exploitation de bug à des fins particulièrement créatives. Personnellement, ma réaction naturelle serait de les secouer très fort jusqu'à ce qu'ils comprennent que ce qu'ils font donne des envies suicidaires et/ou meutrières à l'équipe de développement de Coq.
[1] Bon en fait, n'importe quel spécialiste de la théorie des types sait que c'est pas vrai non plus, mais au moins c'est un langage plutôt robuste en terme de compatibilité.
[^] # Re: Perl6
Posté par Perthmâd . En réponse au journal La recherche en langages de programmation au quotidien. Évalué à 3.
Le cas de Coq est un peu particulier, parce qu'il s'agit en fait d'au moins deux langages différents, Gallina, le langage de preuve en tant que tel, et Ltac, un langage de métaprogrammation qui est à Gallina ce que PHP est à HTML. Autant Gallina est plutôt bien spécifié[1], autant Ltac est un bousin sans nom qui est la source d'un tas de problèmes, le genre de code qu'il suffit de regarder fixement pour faire péter un développement à l'autre bout de la planète. Ceci dit, il y a eu du progrès depuis et l'utilisation d'une infrastructure d'intégration continue un peu sérieuse permet de jauger la casse avant la publication d'une version.
En ce qui concerne Bedrock, je me permets quand même de juger que c'est un cas vraiment extrême. C'est un projet notablement connu pour avoir été implémenté par des gens qui sont des spécialistes internationaux de l'exploitation de bug à des fins particulièrement créatives. Personnellement, ma réaction naturelle serait de les secouer très fort jusqu'à ce qu'ils comprennent que ce qu'ils font donne des envies suicidaires et/ou meutrières à l'équipe de développement de Coq.
[1] Bon en fait, n'importe quel spécialiste de la théorie des types sait que c'est pas vrai non plus, mais au moins c'est un langage plutôt robuste en terme de compatibilité.